Step | Hyp | Ref
| Expression |
1 | | inss2 3152 |
. . . 4
⊢ (𝑅 ∩ (B × B))
⊆ (B × B) |
2 | | relxp 4390 |
. . . 4
⊢ Rel
(B × B) |
3 | | relss 4370 |
. . . 4
⊢ ((𝑅 ∩ (B × B))
⊆ (B × B) → (Rel (B × B)
→ Rel (𝑅 ∩
(B × B)))) |
4 | 1, 2, 3 | mp2 16 |
. . 3
⊢ Rel
(𝑅 ∩ (B × B)) |
5 | 4 | a1i 9 |
. 2
⊢ (φ → Rel (𝑅 ∩ (B × B))) |
6 | | simpr 103 |
. . . . 5
⊢ ((φ ∧ x(𝑅 ∩ (B × B))y) →
x(𝑅 ∩ (B × B))y) |
7 | | brinxp2 4350 |
. . . . 5
⊢ (x(𝑅 ∩ (B × B))y ↔
(x ∈
B ∧
y ∈
B ∧
x𝑅y)) |
8 | 6, 7 | sylib 127 |
. . . 4
⊢ ((φ ∧ x(𝑅 ∩ (B × B))y) →
(x ∈
B ∧
y ∈
B ∧
x𝑅y)) |
9 | 8 | simp2d 916 |
. . 3
⊢ ((φ ∧ x(𝑅 ∩ (B × B))y) →
y ∈
B) |
10 | 8 | simp1d 915 |
. . 3
⊢ ((φ ∧ x(𝑅 ∩ (B × B))y) →
x ∈
B) |
11 | | erinxp.r |
. . . . 5
⊢ (φ → 𝑅 Er A) |
12 | 11 | adantr 261 |
. . . 4
⊢ ((φ ∧ x(𝑅 ∩ (B × B))y) →
𝑅 Er A) |
13 | 8 | simp3d 917 |
. . . 4
⊢ ((φ ∧ x(𝑅 ∩ (B × B))y) →
x𝑅y) |
14 | 12, 13 | ersym 6054 |
. . 3
⊢ ((φ ∧ x(𝑅 ∩ (B × B))y) →
y𝑅x) |
15 | | brinxp2 4350 |
. . 3
⊢ (y(𝑅 ∩ (B × B))x ↔
(y ∈
B ∧
x ∈
B ∧
y𝑅x)) |
16 | 9, 10, 14, 15 | syl3anbrc 1087 |
. 2
⊢ ((φ ∧ x(𝑅 ∩ (B × B))y) →
y(𝑅 ∩ (B × B))x) |
17 | 10 | adantrr 448 |
. . 3
⊢ ((φ ∧
(x(𝑅 ∩ (B × B))y ∧ y(𝑅 ∩ (B × B))z)) →
x ∈
B) |
18 | | simprr 484 |
. . . . 5
⊢ ((φ ∧
(x(𝑅 ∩ (B × B))y ∧ y(𝑅 ∩ (B × B))z)) →
y(𝑅 ∩ (B × B))z) |
19 | | brinxp2 4350 |
. . . . 5
⊢ (y(𝑅 ∩ (B × B))z ↔
(y ∈
B ∧
z ∈
B ∧
y𝑅z)) |
20 | 18, 19 | sylib 127 |
. . . 4
⊢ ((φ ∧
(x(𝑅 ∩ (B × B))y ∧ y(𝑅 ∩ (B × B))z)) →
(y ∈
B ∧
z ∈
B ∧
y𝑅z)) |
21 | 20 | simp2d 916 |
. . 3
⊢ ((φ ∧
(x(𝑅 ∩ (B × B))y ∧ y(𝑅 ∩ (B × B))z)) →
z ∈
B) |
22 | 11 | adantr 261 |
. . . 4
⊢ ((φ ∧
(x(𝑅 ∩ (B × B))y ∧ y(𝑅 ∩ (B × B))z)) →
𝑅 Er A) |
23 | 13 | adantrr 448 |
. . . 4
⊢ ((φ ∧
(x(𝑅 ∩ (B × B))y ∧ y(𝑅 ∩ (B × B))z)) →
x𝑅y) |
24 | 20 | simp3d 917 |
. . . 4
⊢ ((φ ∧
(x(𝑅 ∩ (B × B))y ∧ y(𝑅 ∩ (B × B))z)) →
y𝑅z) |
25 | 22, 23, 24 | ertrd 6058 |
. . 3
⊢ ((φ ∧
(x(𝑅 ∩ (B × B))y ∧ y(𝑅 ∩ (B × B))z)) →
x𝑅z) |
26 | | brinxp2 4350 |
. . 3
⊢ (x(𝑅 ∩ (B × B))z ↔
(x ∈
B ∧
z ∈
B ∧
x𝑅z)) |
27 | 17, 21, 25, 26 | syl3anbrc 1087 |
. 2
⊢ ((φ ∧
(x(𝑅 ∩ (B × B))y ∧ y(𝑅 ∩ (B × B))z)) →
x(𝑅 ∩ (B × B))z) |
28 | 11 | adantr 261 |
. . . . . 6
⊢ ((φ ∧ x ∈ B) → 𝑅 Er A) |
29 | | erinxp.a |
. . . . . . 7
⊢ (φ → B ⊆ A) |
30 | 29 | sselda 2939 |
. . . . . 6
⊢ ((φ ∧ x ∈ B) → x
∈ A) |
31 | 28, 30 | erref 6062 |
. . . . 5
⊢ ((φ ∧ x ∈ B) → x𝑅x) |
32 | 31 | ex 108 |
. . . 4
⊢ (φ → (x ∈ B → x𝑅x)) |
33 | 32 | pm4.71rd 374 |
. . 3
⊢ (φ → (x ∈ B ↔ (x𝑅x ∧ x ∈ B))) |
34 | | brin 3802 |
. . . 4
⊢ (x(𝑅 ∩ (B × B))x ↔
(x𝑅x ∧ x(B × B)x)) |
35 | | brxp 4318 |
. . . . . 6
⊢ (x(B ×
B)x
↔ (x ∈ B ∧ x ∈ B)) |
36 | | anidm 376 |
. . . . . 6
⊢
((x ∈ B ∧ x ∈ B) ↔
x ∈
B) |
37 | 35, 36 | bitri 173 |
. . . . 5
⊢ (x(B ×
B)x
↔ x ∈ B) |
38 | 37 | anbi2i 430 |
. . . 4
⊢
((x𝑅x ∧ x(B × B)x) ↔
(x𝑅x ∧ x ∈ B)) |
39 | 34, 38 | bitri 173 |
. . 3
⊢ (x(𝑅 ∩ (B × B))x ↔
(x𝑅x ∧ x ∈ B)) |
40 | 33, 39 | syl6bbr 187 |
. 2
⊢ (φ → (x ∈ B ↔ x(𝑅 ∩ (B × B))x)) |
41 | 5, 16, 27, 40 | iserd 6068 |
1
⊢ (φ → (𝑅 ∩ (B × B)) Er
B) |