Step | Hyp | Ref
| Expression |
1 | | eleq1 2097 |
. . . 4
⊢ (x = 𝑎 → (x ∈ A ↔ 𝑎 ∈ A)) |
2 | 1 | cbvexv 1792 |
. . 3
⊢ (∃x x ∈ A ↔ ∃𝑎 𝑎 ∈ A) |
3 | | eleq1 2097 |
. . . 4
⊢ (𝑎 = y → (𝑎 ∈ A ↔ y ∈ A)) |
4 | 3 | cbvexv 1792 |
. . 3
⊢ (∃𝑎 𝑎 ∈ A ↔ ∃y y ∈ A) |
5 | 2, 4 | bitri 173 |
. 2
⊢ (∃x x ∈ A ↔ ∃y y ∈ A) |
6 | | r19.2m 3303 |
. . . . 5
⊢ ((∃x x ∈ A ∧ ∀x ∈ A 𝑅 Er B) → ∃x ∈ A 𝑅 Er B) |
7 | | errel 6051 |
. . . . . . 7
⊢ (𝑅 Er B → Rel 𝑅) |
8 | | df-rel 4295 |
. . . . . . 7
⊢ (Rel
𝑅 ↔ 𝑅 ⊆ (V × V)) |
9 | 7, 8 | sylib 127 |
. . . . . 6
⊢ (𝑅 Er B → 𝑅 ⊆ (V × V)) |
10 | 9 | reximi 2410 |
. . . . 5
⊢ (∃x ∈ A 𝑅 Er B → ∃x ∈ A 𝑅 ⊆ (V ×
V)) |
11 | | iinss 3699 |
. . . . 5
⊢ (∃x ∈ A 𝑅 ⊆ (V × V) →
∩ x ∈ A 𝑅 ⊆ (V ×
V)) |
12 | 6, 10, 11 | 3syl 17 |
. . . 4
⊢ ((∃x x ∈ A ∧ ∀x ∈ A 𝑅 Er B) → ∩
x ∈
A 𝑅 ⊆ (V × V)) |
13 | | df-rel 4295 |
. . . 4
⊢ (Rel
∩ x ∈ A 𝑅 ↔ ∩ x ∈ A 𝑅 ⊆ (V ×
V)) |
14 | 12, 13 | sylibr 137 |
. . 3
⊢ ((∃x x ∈ A ∧ ∀x ∈ A 𝑅 Er B) → Rel ∩
x ∈
A 𝑅) |
15 | | id 19 |
. . . . . . . . . 10
⊢ (𝑅 Er B → 𝑅 Er B) |
16 | 15 | ersymb 6056 |
. . . . . . . . 9
⊢ (𝑅 Er B → (u𝑅v ↔ v𝑅u)) |
17 | 16 | biimpd 132 |
. . . . . . . 8
⊢ (𝑅 Er B → (u𝑅v → v𝑅u)) |
18 | | df-br 3756 |
. . . . . . . 8
⊢ (u𝑅v ↔
〈u, v〉 ∈ 𝑅) |
19 | | df-br 3756 |
. . . . . . . 8
⊢ (v𝑅u ↔
〈v, u〉 ∈ 𝑅) |
20 | 17, 18, 19 | 3imtr3g 193 |
. . . . . . 7
⊢ (𝑅 Er B → (〈u, v〉 ∈ 𝑅 → 〈v, u〉 ∈ 𝑅)) |
21 | 20 | ral2imi 2379 |
. . . . . 6
⊢ (∀x ∈ A 𝑅 Er B → (∀x ∈ A
〈u, v〉 ∈ 𝑅 → ∀x ∈ A
〈v, u〉 ∈ 𝑅)) |
22 | 21 | adantl 262 |
. . . . 5
⊢ ((∃x x ∈ A ∧ ∀x ∈ A 𝑅 Er B) → (∀x ∈ A
〈u, v〉 ∈ 𝑅 → ∀x ∈ A
〈v, u〉 ∈ 𝑅)) |
23 | | df-br 3756 |
. . . . . 6
⊢ (u∩ x ∈ A 𝑅v ↔
〈u, v〉 ∈ ∩ x ∈ A 𝑅) |
24 | | vex 2554 |
. . . . . . . 8
⊢ u ∈
V |
25 | | vex 2554 |
. . . . . . . 8
⊢ v ∈
V |
26 | 24, 25 | opex 3957 |
. . . . . . 7
⊢
〈u, v〉 ∈
V |
27 | | eliin 3653 |
. . . . . . 7
⊢
(〈u, v〉 ∈ V →
(〈u, v〉 ∈ ∩ x ∈ A 𝑅 ↔ ∀x ∈ A
〈u, v〉 ∈ 𝑅)) |
28 | 26, 27 | ax-mp 7 |
. . . . . 6
⊢
(〈u, v〉 ∈ ∩ x ∈ A 𝑅 ↔ ∀x ∈ A
〈u, v〉 ∈ 𝑅) |
29 | 23, 28 | bitri 173 |
. . . . 5
⊢ (u∩ x ∈ A 𝑅v ↔
∀x
∈ A
〈u, v〉 ∈ 𝑅) |
30 | | df-br 3756 |
. . . . . 6
⊢ (v∩ x ∈ A 𝑅u ↔
〈v, u〉 ∈ ∩ x ∈ A 𝑅) |
31 | 25, 24 | opex 3957 |
. . . . . . 7
⊢
〈v, u〉 ∈
V |
32 | | eliin 3653 |
. . . . . . 7
⊢
(〈v, u〉 ∈ V →
(〈v, u〉 ∈ ∩ x ∈ A 𝑅 ↔ ∀x ∈ A
〈v, u〉 ∈ 𝑅)) |
33 | 31, 32 | ax-mp 7 |
. . . . . 6
⊢
(〈v, u〉 ∈ ∩ x ∈ A 𝑅 ↔ ∀x ∈ A
〈v, u〉 ∈ 𝑅) |
34 | 30, 33 | bitri 173 |
. . . . 5
⊢ (v∩ x ∈ A 𝑅u ↔
∀x
∈ A
〈v, u〉 ∈ 𝑅) |
35 | 22, 29, 34 | 3imtr4g 194 |
. . . 4
⊢ ((∃x x ∈ A ∧ ∀x ∈ A 𝑅 Er B) → (u∩ x ∈ A 𝑅v →
v∩
x ∈
A 𝑅u)) |
36 | 35 | imp 115 |
. . 3
⊢ (((∃x x ∈ A ∧ ∀x ∈ A 𝑅 Er B) ∧ u∩ x ∈ A 𝑅v)
→ v∩
x ∈
A 𝑅u) |
37 | | r19.26 2435 |
. . . . . 6
⊢ (∀x ∈ A
(〈u, v〉 ∈ 𝑅 ∧ 〈v,
w〉 ∈
𝑅) ↔ (∀x ∈ A
〈u, v〉 ∈ 𝑅 ∧ ∀x ∈ A 〈v,
w〉 ∈
𝑅)) |
38 | 15 | ertr 6057 |
. . . . . . . . 9
⊢ (𝑅 Er B → ((u𝑅v ∧ v𝑅w) → u𝑅w)) |
39 | | df-br 3756 |
. . . . . . . . . 10
⊢ (v𝑅w ↔
〈v, w〉 ∈ 𝑅) |
40 | 18, 39 | anbi12i 433 |
. . . . . . . . 9
⊢
((u𝑅v ∧ v𝑅w) ↔ (〈u, v〉 ∈ 𝑅 ∧
〈v, w〉 ∈ 𝑅)) |
41 | | df-br 3756 |
. . . . . . . . 9
⊢ (u𝑅w ↔
〈u, w〉 ∈ 𝑅) |
42 | 38, 40, 41 | 3imtr3g 193 |
. . . . . . . 8
⊢ (𝑅 Er B → ((〈u, v〉 ∈ 𝑅 ∧
〈v, w〉 ∈ 𝑅) → 〈u, w〉 ∈ 𝑅)) |
43 | 42 | ral2imi 2379 |
. . . . . . 7
⊢ (∀x ∈ A 𝑅 Er B → (∀x ∈ A
(〈u, v〉 ∈ 𝑅 ∧ 〈v,
w〉 ∈
𝑅) → ∀x ∈ A
〈u, w〉 ∈ 𝑅)) |
44 | 43 | adantl 262 |
. . . . . 6
⊢ ((∃x x ∈ A ∧ ∀x ∈ A 𝑅 Er B) → (∀x ∈ A
(〈u, v〉 ∈ 𝑅 ∧ 〈v,
w〉 ∈
𝑅) → ∀x ∈ A
〈u, w〉 ∈ 𝑅)) |
45 | 37, 44 | syl5bir 142 |
. . . . 5
⊢ ((∃x x ∈ A ∧ ∀x ∈ A 𝑅 Er B) → ((∀x ∈ A
〈u, v〉 ∈ 𝑅 ∧ ∀x ∈ A 〈v,
w〉 ∈
𝑅) → ∀x ∈ A
〈u, w〉 ∈ 𝑅)) |
46 | | df-br 3756 |
. . . . . . 7
⊢ (v∩ x ∈ A 𝑅w ↔
〈v, w〉 ∈ ∩ x ∈ A 𝑅) |
47 | | vex 2554 |
. . . . . . . . 9
⊢ w ∈
V |
48 | 25, 47 | opex 3957 |
. . . . . . . 8
⊢
〈v, w〉 ∈
V |
49 | | eliin 3653 |
. . . . . . . 8
⊢
(〈v, w〉 ∈ V →
(〈v, w〉 ∈ ∩ x ∈ A 𝑅 ↔ ∀x ∈ A
〈v, w〉 ∈ 𝑅)) |
50 | 48, 49 | ax-mp 7 |
. . . . . . 7
⊢
(〈v, w〉 ∈ ∩ x ∈ A 𝑅 ↔ ∀x ∈ A
〈v, w〉 ∈ 𝑅) |
51 | 46, 50 | bitri 173 |
. . . . . 6
⊢ (v∩ x ∈ A 𝑅w ↔
∀x
∈ A
〈v, w〉 ∈ 𝑅) |
52 | 29, 51 | anbi12i 433 |
. . . . 5
⊢
((u∩ x ∈ A 𝑅v ∧ v∩ x ∈ A 𝑅w)
↔ (∀x ∈ A 〈u,
v〉 ∈
𝑅 ∧ ∀x ∈ A 〈v,
w〉 ∈
𝑅)) |
53 | | df-br 3756 |
. . . . . 6
⊢ (u∩ x ∈ A 𝑅w ↔
〈u, w〉 ∈ ∩ x ∈ A 𝑅) |
54 | 24, 47 | opex 3957 |
. . . . . . 7
⊢
〈u, w〉 ∈
V |
55 | | eliin 3653 |
. . . . . . 7
⊢
(〈u, w〉 ∈ V →
(〈u, w〉 ∈ ∩ x ∈ A 𝑅 ↔ ∀x ∈ A
〈u, w〉 ∈ 𝑅)) |
56 | 54, 55 | ax-mp 7 |
. . . . . 6
⊢
(〈u, w〉 ∈ ∩ x ∈ A 𝑅 ↔ ∀x ∈ A
〈u, w〉 ∈ 𝑅) |
57 | 53, 56 | bitri 173 |
. . . . 5
⊢ (u∩ x ∈ A 𝑅w ↔
∀x
∈ A
〈u, w〉 ∈ 𝑅) |
58 | 45, 52, 57 | 3imtr4g 194 |
. . . 4
⊢ ((∃x x ∈ A ∧ ∀x ∈ A 𝑅 Er B) → ((u∩ x ∈ A 𝑅v ∧ v∩ x ∈ A 𝑅w) → u∩ x ∈ A 𝑅w)) |
59 | 58 | imp 115 |
. . 3
⊢ (((∃x x ∈ A ∧ ∀x ∈ A 𝑅 Er B) ∧ (u∩ x ∈ A 𝑅v ∧ v∩ x ∈ A 𝑅w)) → u∩ x ∈ A 𝑅w) |
60 | | simpl 102 |
. . . . . . . . . . 11
⊢ ((𝑅 Er B ∧ u ∈ B) → 𝑅 Er B) |
61 | | simpr 103 |
. . . . . . . . . . 11
⊢ ((𝑅 Er B ∧ u ∈ B) → u
∈ B) |
62 | 60, 61 | erref 6062 |
. . . . . . . . . 10
⊢ ((𝑅 Er B ∧ u ∈ B) → u𝑅u) |
63 | | df-br 3756 |
. . . . . . . . . 10
⊢ (u𝑅u ↔
〈u, u〉 ∈ 𝑅) |
64 | 62, 63 | sylib 127 |
. . . . . . . . 9
⊢ ((𝑅 Er B ∧ u ∈ B) → 〈u, u〉 ∈ 𝑅) |
65 | 64 | expcom 109 |
. . . . . . . 8
⊢ (u ∈ B → (𝑅 Er B
→ 〈u, u〉 ∈ 𝑅)) |
66 | 65 | ralimdv 2382 |
. . . . . . 7
⊢ (u ∈ B → (∀x ∈ A 𝑅 Er B → ∀x ∈ A
〈u, u〉 ∈ 𝑅)) |
67 | 66 | com12 27 |
. . . . . 6
⊢ (∀x ∈ A 𝑅 Er B → (u
∈ B
→ ∀x ∈ A 〈u,
u〉 ∈
𝑅)) |
68 | 67 | adantl 262 |
. . . . 5
⊢ ((∃x x ∈ A ∧ ∀x ∈ A 𝑅 Er B) → (u
∈ B
→ ∀x ∈ A 〈u,
u〉 ∈
𝑅)) |
69 | | r19.26 2435 |
. . . . . . 7
⊢ (∀x ∈ A (𝑅 Er B ∧ 〈u, u〉 ∈ 𝑅) ↔ (∀x ∈ A 𝑅 Er B ∧ ∀x ∈ A
〈u, u〉 ∈ 𝑅)) |
70 | | r19.2m 3303 |
. . . . . . . . 9
⊢ ((∃x x ∈ A ∧ ∀x ∈ A (𝑅 Er B ∧ 〈u, u〉 ∈ 𝑅)) → ∃x ∈ A (𝑅 Er B ∧ 〈u, u〉 ∈ 𝑅)) |
71 | 24, 24 | opeldm 4481 |
. . . . . . . . . . 11
⊢
(〈u, u〉 ∈ 𝑅 → u ∈ dom 𝑅) |
72 | | erdm 6052 |
. . . . . . . . . . . . 13
⊢ (𝑅 Er B → dom 𝑅 = B) |
73 | 72 | eleq2d 2104 |
. . . . . . . . . . . 12
⊢ (𝑅 Er B → (u
∈ dom 𝑅 ↔ u ∈ B)) |
74 | 73 | biimpa 280 |
. . . . . . . . . . 11
⊢ ((𝑅 Er B ∧ u ∈ dom 𝑅) → u ∈ B) |
75 | 71, 74 | sylan2 270 |
. . . . . . . . . 10
⊢ ((𝑅 Er B ∧ 〈u, u〉 ∈ 𝑅) → u ∈ B) |
76 | 75 | rexlimivw 2423 |
. . . . . . . . 9
⊢ (∃x ∈ A (𝑅 Er B ∧ 〈u, u〉 ∈ 𝑅) → u ∈ B) |
77 | 70, 76 | syl 14 |
. . . . . . . 8
⊢ ((∃x x ∈ A ∧ ∀x ∈ A (𝑅 Er B ∧ 〈u, u〉 ∈ 𝑅)) → u ∈ B) |
78 | 77 | ex 108 |
. . . . . . 7
⊢ (∃x x ∈ A → (∀x ∈ A (𝑅 Er B ∧ 〈u, u〉 ∈ 𝑅) → u ∈ B)) |
79 | 69, 78 | syl5bir 142 |
. . . . . 6
⊢ (∃x x ∈ A → ((∀x ∈ A 𝑅 Er B ∧ ∀x ∈ A
〈u, u〉 ∈ 𝑅) → u ∈ B)) |
80 | 79 | expdimp 246 |
. . . . 5
⊢ ((∃x x ∈ A ∧ ∀x ∈ A 𝑅 Er B) → (∀x ∈ A
〈u, u〉 ∈ 𝑅 → u ∈ B)) |
81 | 68, 80 | impbid 120 |
. . . 4
⊢ ((∃x x ∈ A ∧ ∀x ∈ A 𝑅 Er B) → (u
∈ B
↔ ∀x ∈ A 〈u,
u〉 ∈
𝑅)) |
82 | | df-br 3756 |
. . . . 5
⊢ (u∩ x ∈ A 𝑅u ↔
〈u, u〉 ∈ ∩ x ∈ A 𝑅) |
83 | 24, 24 | opex 3957 |
. . . . . 6
⊢
〈u, u〉 ∈
V |
84 | | eliin 3653 |
. . . . . 6
⊢
(〈u, u〉 ∈ V →
(〈u, u〉 ∈ ∩ x ∈ A 𝑅 ↔ ∀x ∈ A
〈u, u〉 ∈ 𝑅)) |
85 | 83, 84 | ax-mp 7 |
. . . . 5
⊢
(〈u, u〉 ∈ ∩ x ∈ A 𝑅 ↔ ∀x ∈ A
〈u, u〉 ∈ 𝑅) |
86 | 82, 85 | bitri 173 |
. . . 4
⊢ (u∩ x ∈ A 𝑅u ↔
∀x
∈ A
〈u, u〉 ∈ 𝑅) |
87 | 81, 86 | syl6bbr 187 |
. . 3
⊢ ((∃x x ∈ A ∧ ∀x ∈ A 𝑅 Er B) → (u
∈ B
↔ u∩
x ∈
A 𝑅u)) |
88 | 14, 36, 59, 87 | iserd 6068 |
. 2
⊢ ((∃x x ∈ A ∧ ∀x ∈ A 𝑅 Er B) → ∩
x ∈
A 𝑅 Er B) |
89 | 5, 88 | sylanbr 269 |
1
⊢ ((∃y y ∈ A ∧ ∀x ∈ A 𝑅 Er B) → ∩
x ∈
A 𝑅 Er B) |