Step | Hyp | Ref
| Expression |
1 | | eleq1w 2236 |
. . . 4
⊢ (𝑥 = 𝑎 → (𝑥 ∈ 𝐴 ↔ 𝑎 ∈ 𝐴)) |
2 | 1 | cbvexv 1916 |
. . 3
⊢
(∃𝑥 𝑥 ∈ 𝐴 ↔ ∃𝑎 𝑎 ∈ 𝐴) |
3 | | eleq1w 2236 |
. . . 4
⊢ (𝑎 = 𝑦 → (𝑎 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
4 | 3 | cbvexv 1916 |
. . 3
⊢
(∃𝑎 𝑎 ∈ 𝐴 ↔ ∃𝑦 𝑦 ∈ 𝐴) |
5 | 2, 4 | bitri 184 |
. 2
⊢
(∃𝑥 𝑥 ∈ 𝐴 ↔ ∃𝑦 𝑦 ∈ 𝐴) |
6 | | r19.2m 3507 |
. . . . 5
⊢
((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → ∃𝑥 ∈ 𝐴 𝑅 Er 𝐵) |
7 | | errel 6534 |
. . . . . . 7
⊢ (𝑅 Er 𝐵 → Rel 𝑅) |
8 | | df-rel 4627 |
. . . . . . 7
⊢ (Rel
𝑅 ↔ 𝑅 ⊆ (V × V)) |
9 | 7, 8 | sylib 122 |
. . . . . 6
⊢ (𝑅 Er 𝐵 → 𝑅 ⊆ (V × V)) |
10 | 9 | reximi 2572 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 𝑅 Er 𝐵 → ∃𝑥 ∈ 𝐴 𝑅 ⊆ (V × V)) |
11 | | iinss 3933 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 𝑅 ⊆ (V × V) → ∩ 𝑥 ∈ 𝐴 𝑅 ⊆ (V × V)) |
12 | 6, 10, 11 | 3syl 17 |
. . . 4
⊢
((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → ∩
𝑥 ∈ 𝐴 𝑅 ⊆ (V × V)) |
13 | | df-rel 4627 |
. . . 4
⊢ (Rel
∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∩
𝑥 ∈ 𝐴 𝑅 ⊆ (V × V)) |
14 | 12, 13 | sylibr 134 |
. . 3
⊢
((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → Rel ∩ 𝑥 ∈ 𝐴 𝑅) |
15 | | id 19 |
. . . . . . . . . 10
⊢ (𝑅 Er 𝐵 → 𝑅 Er 𝐵) |
16 | 15 | ersymb 6539 |
. . . . . . . . 9
⊢ (𝑅 Er 𝐵 → (𝑢𝑅𝑣 ↔ 𝑣𝑅𝑢)) |
17 | 16 | biimpd 144 |
. . . . . . . 8
⊢ (𝑅 Er 𝐵 → (𝑢𝑅𝑣 → 𝑣𝑅𝑢)) |
18 | | df-br 3999 |
. . . . . . . 8
⊢ (𝑢𝑅𝑣 ↔ 〈𝑢, 𝑣〉 ∈ 𝑅) |
19 | | df-br 3999 |
. . . . . . . 8
⊢ (𝑣𝑅𝑢 ↔ 〈𝑣, 𝑢〉 ∈ 𝑅) |
20 | 17, 18, 19 | 3imtr3g 204 |
. . . . . . 7
⊢ (𝑅 Er 𝐵 → (〈𝑢, 𝑣〉 ∈ 𝑅 → 〈𝑣, 𝑢〉 ∈ 𝑅)) |
21 | 20 | ral2imi 2540 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 𝑅 Er 𝐵 → (∀𝑥 ∈ 𝐴 〈𝑢, 𝑣〉 ∈ 𝑅 → ∀𝑥 ∈ 𝐴 〈𝑣, 𝑢〉 ∈ 𝑅)) |
22 | 21 | adantl 277 |
. . . . 5
⊢
((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → (∀𝑥 ∈ 𝐴 〈𝑢, 𝑣〉 ∈ 𝑅 → ∀𝑥 ∈ 𝐴 〈𝑣, 𝑢〉 ∈ 𝑅)) |
23 | | df-br 3999 |
. . . . . 6
⊢ (𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑣 ↔ 〈𝑢, 𝑣〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅) |
24 | | vex 2738 |
. . . . . . . 8
⊢ 𝑢 ∈ V |
25 | | vex 2738 |
. . . . . . . 8
⊢ 𝑣 ∈ V |
26 | 24, 25 | opex 4223 |
. . . . . . 7
⊢
〈𝑢, 𝑣〉 ∈ V |
27 | | eliin 3887 |
. . . . . . 7
⊢
(〈𝑢, 𝑣〉 ∈ V →
(〈𝑢, 𝑣〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀𝑥 ∈ 𝐴 〈𝑢, 𝑣〉 ∈ 𝑅)) |
28 | 26, 27 | ax-mp 5 |
. . . . . 6
⊢
(〈𝑢, 𝑣〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀𝑥 ∈ 𝐴 〈𝑢, 𝑣〉 ∈ 𝑅) |
29 | 23, 28 | bitri 184 |
. . . . 5
⊢ (𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑣 ↔ ∀𝑥 ∈ 𝐴 〈𝑢, 𝑣〉 ∈ 𝑅) |
30 | | df-br 3999 |
. . . . . 6
⊢ (𝑣∩ 𝑥 ∈ 𝐴 𝑅𝑢 ↔ 〈𝑣, 𝑢〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅) |
31 | 25, 24 | opex 4223 |
. . . . . . 7
⊢
〈𝑣, 𝑢〉 ∈ V |
32 | | eliin 3887 |
. . . . . . 7
⊢
(〈𝑣, 𝑢〉 ∈ V →
(〈𝑣, 𝑢〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀𝑥 ∈ 𝐴 〈𝑣, 𝑢〉 ∈ 𝑅)) |
33 | 31, 32 | ax-mp 5 |
. . . . . 6
⊢
(〈𝑣, 𝑢〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀𝑥 ∈ 𝐴 〈𝑣, 𝑢〉 ∈ 𝑅) |
34 | 30, 33 | bitri 184 |
. . . . 5
⊢ (𝑣∩ 𝑥 ∈ 𝐴 𝑅𝑢 ↔ ∀𝑥 ∈ 𝐴 〈𝑣, 𝑢〉 ∈ 𝑅) |
35 | 22, 29, 34 | 3imtr4g 205 |
. . . 4
⊢
((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → (𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑣 → 𝑣∩ 𝑥 ∈ 𝐴 𝑅𝑢)) |
36 | 35 | imp 124 |
. . 3
⊢
(((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) ∧ 𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑣) → 𝑣∩ 𝑥 ∈ 𝐴 𝑅𝑢) |
37 | | r19.26 2601 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 (〈𝑢, 𝑣〉 ∈ 𝑅 ∧ 〈𝑣, 𝑤〉 ∈ 𝑅) ↔ (∀𝑥 ∈ 𝐴 〈𝑢, 𝑣〉 ∈ 𝑅 ∧ ∀𝑥 ∈ 𝐴 〈𝑣, 𝑤〉 ∈ 𝑅)) |
38 | 15 | ertr 6540 |
. . . . . . . . 9
⊢ (𝑅 Er 𝐵 → ((𝑢𝑅𝑣 ∧ 𝑣𝑅𝑤) → 𝑢𝑅𝑤)) |
39 | | df-br 3999 |
. . . . . . . . . 10
⊢ (𝑣𝑅𝑤 ↔ 〈𝑣, 𝑤〉 ∈ 𝑅) |
40 | 18, 39 | anbi12i 460 |
. . . . . . . . 9
⊢ ((𝑢𝑅𝑣 ∧ 𝑣𝑅𝑤) ↔ (〈𝑢, 𝑣〉 ∈ 𝑅 ∧ 〈𝑣, 𝑤〉 ∈ 𝑅)) |
41 | | df-br 3999 |
. . . . . . . . 9
⊢ (𝑢𝑅𝑤 ↔ 〈𝑢, 𝑤〉 ∈ 𝑅) |
42 | 38, 40, 41 | 3imtr3g 204 |
. . . . . . . 8
⊢ (𝑅 Er 𝐵 → ((〈𝑢, 𝑣〉 ∈ 𝑅 ∧ 〈𝑣, 𝑤〉 ∈ 𝑅) → 〈𝑢, 𝑤〉 ∈ 𝑅)) |
43 | 42 | ral2imi 2540 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 𝑅 Er 𝐵 → (∀𝑥 ∈ 𝐴 (〈𝑢, 𝑣〉 ∈ 𝑅 ∧ 〈𝑣, 𝑤〉 ∈ 𝑅) → ∀𝑥 ∈ 𝐴 〈𝑢, 𝑤〉 ∈ 𝑅)) |
44 | 43 | adantl 277 |
. . . . . 6
⊢
((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → (∀𝑥 ∈ 𝐴 (〈𝑢, 𝑣〉 ∈ 𝑅 ∧ 〈𝑣, 𝑤〉 ∈ 𝑅) → ∀𝑥 ∈ 𝐴 〈𝑢, 𝑤〉 ∈ 𝑅)) |
45 | 37, 44 | syl5bir 153 |
. . . . 5
⊢
((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → ((∀𝑥 ∈ 𝐴 〈𝑢, 𝑣〉 ∈ 𝑅 ∧ ∀𝑥 ∈ 𝐴 〈𝑣, 𝑤〉 ∈ 𝑅) → ∀𝑥 ∈ 𝐴 〈𝑢, 𝑤〉 ∈ 𝑅)) |
46 | | df-br 3999 |
. . . . . . 7
⊢ (𝑣∩ 𝑥 ∈ 𝐴 𝑅𝑤 ↔ 〈𝑣, 𝑤〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅) |
47 | | vex 2738 |
. . . . . . . . 9
⊢ 𝑤 ∈ V |
48 | 25, 47 | opex 4223 |
. . . . . . . 8
⊢
〈𝑣, 𝑤〉 ∈ V |
49 | | eliin 3887 |
. . . . . . . 8
⊢
(〈𝑣, 𝑤〉 ∈ V →
(〈𝑣, 𝑤〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀𝑥 ∈ 𝐴 〈𝑣, 𝑤〉 ∈ 𝑅)) |
50 | 48, 49 | ax-mp 5 |
. . . . . . 7
⊢
(〈𝑣, 𝑤〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀𝑥 ∈ 𝐴 〈𝑣, 𝑤〉 ∈ 𝑅) |
51 | 46, 50 | bitri 184 |
. . . . . 6
⊢ (𝑣∩ 𝑥 ∈ 𝐴 𝑅𝑤 ↔ ∀𝑥 ∈ 𝐴 〈𝑣, 𝑤〉 ∈ 𝑅) |
52 | 29, 51 | anbi12i 460 |
. . . . 5
⊢ ((𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑣 ∧ 𝑣∩ 𝑥 ∈ 𝐴 𝑅𝑤) ↔ (∀𝑥 ∈ 𝐴 〈𝑢, 𝑣〉 ∈ 𝑅 ∧ ∀𝑥 ∈ 𝐴 〈𝑣, 𝑤〉 ∈ 𝑅)) |
53 | | df-br 3999 |
. . . . . 6
⊢ (𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑤 ↔ 〈𝑢, 𝑤〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅) |
54 | 24, 47 | opex 4223 |
. . . . . . 7
⊢
〈𝑢, 𝑤〉 ∈ V |
55 | | eliin 3887 |
. . . . . . 7
⊢
(〈𝑢, 𝑤〉 ∈ V →
(〈𝑢, 𝑤〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀𝑥 ∈ 𝐴 〈𝑢, 𝑤〉 ∈ 𝑅)) |
56 | 54, 55 | ax-mp 5 |
. . . . . 6
⊢
(〈𝑢, 𝑤〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀𝑥 ∈ 𝐴 〈𝑢, 𝑤〉 ∈ 𝑅) |
57 | 53, 56 | bitri 184 |
. . . . 5
⊢ (𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑤 ↔ ∀𝑥 ∈ 𝐴 〈𝑢, 𝑤〉 ∈ 𝑅) |
58 | 45, 52, 57 | 3imtr4g 205 |
. . . 4
⊢
((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → ((𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑣 ∧ 𝑣∩ 𝑥 ∈ 𝐴 𝑅𝑤) → 𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑤)) |
59 | 58 | imp 124 |
. . 3
⊢
(((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) ∧ (𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑣 ∧ 𝑣∩ 𝑥 ∈ 𝐴 𝑅𝑤)) → 𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑤) |
60 | | simpl 109 |
. . . . . . . . . . 11
⊢ ((𝑅 Er 𝐵 ∧ 𝑢 ∈ 𝐵) → 𝑅 Er 𝐵) |
61 | | simpr 110 |
. . . . . . . . . . 11
⊢ ((𝑅 Er 𝐵 ∧ 𝑢 ∈ 𝐵) → 𝑢 ∈ 𝐵) |
62 | 60, 61 | erref 6545 |
. . . . . . . . . 10
⊢ ((𝑅 Er 𝐵 ∧ 𝑢 ∈ 𝐵) → 𝑢𝑅𝑢) |
63 | | df-br 3999 |
. . . . . . . . . 10
⊢ (𝑢𝑅𝑢 ↔ 〈𝑢, 𝑢〉 ∈ 𝑅) |
64 | 62, 63 | sylib 122 |
. . . . . . . . 9
⊢ ((𝑅 Er 𝐵 ∧ 𝑢 ∈ 𝐵) → 〈𝑢, 𝑢〉 ∈ 𝑅) |
65 | 64 | expcom 116 |
. . . . . . . 8
⊢ (𝑢 ∈ 𝐵 → (𝑅 Er 𝐵 → 〈𝑢, 𝑢〉 ∈ 𝑅)) |
66 | 65 | ralimdv 2543 |
. . . . . . 7
⊢ (𝑢 ∈ 𝐵 → (∀𝑥 ∈ 𝐴 𝑅 Er 𝐵 → ∀𝑥 ∈ 𝐴 〈𝑢, 𝑢〉 ∈ 𝑅)) |
67 | 66 | com12 30 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 𝑅 Er 𝐵 → (𝑢 ∈ 𝐵 → ∀𝑥 ∈ 𝐴 〈𝑢, 𝑢〉 ∈ 𝑅)) |
68 | 67 | adantl 277 |
. . . . 5
⊢
((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → (𝑢 ∈ 𝐵 → ∀𝑥 ∈ 𝐴 〈𝑢, 𝑢〉 ∈ 𝑅)) |
69 | | r19.26 2601 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 (𝑅 Er 𝐵 ∧ 〈𝑢, 𝑢〉 ∈ 𝑅) ↔ (∀𝑥 ∈ 𝐴 𝑅 Er 𝐵 ∧ ∀𝑥 ∈ 𝐴 〈𝑢, 𝑢〉 ∈ 𝑅)) |
70 | | r19.2m 3507 |
. . . . . . . . 9
⊢
((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑅 Er 𝐵 ∧ 〈𝑢, 𝑢〉 ∈ 𝑅)) → ∃𝑥 ∈ 𝐴 (𝑅 Er 𝐵 ∧ 〈𝑢, 𝑢〉 ∈ 𝑅)) |
71 | 24, 24 | opeldm 4823 |
. . . . . . . . . . 11
⊢
(〈𝑢, 𝑢〉 ∈ 𝑅 → 𝑢 ∈ dom 𝑅) |
72 | | erdm 6535 |
. . . . . . . . . . . . 13
⊢ (𝑅 Er 𝐵 → dom 𝑅 = 𝐵) |
73 | 72 | eleq2d 2245 |
. . . . . . . . . . . 12
⊢ (𝑅 Er 𝐵 → (𝑢 ∈ dom 𝑅 ↔ 𝑢 ∈ 𝐵)) |
74 | 73 | biimpa 296 |
. . . . . . . . . . 11
⊢ ((𝑅 Er 𝐵 ∧ 𝑢 ∈ dom 𝑅) → 𝑢 ∈ 𝐵) |
75 | 71, 74 | sylan2 286 |
. . . . . . . . . 10
⊢ ((𝑅 Er 𝐵 ∧ 〈𝑢, 𝑢〉 ∈ 𝑅) → 𝑢 ∈ 𝐵) |
76 | 75 | rexlimivw 2588 |
. . . . . . . . 9
⊢
(∃𝑥 ∈
𝐴 (𝑅 Er 𝐵 ∧ 〈𝑢, 𝑢〉 ∈ 𝑅) → 𝑢 ∈ 𝐵) |
77 | 70, 76 | syl 14 |
. . . . . . . 8
⊢
((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑅 Er 𝐵 ∧ 〈𝑢, 𝑢〉 ∈ 𝑅)) → 𝑢 ∈ 𝐵) |
78 | 77 | ex 115 |
. . . . . . 7
⊢
(∃𝑥 𝑥 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 (𝑅 Er 𝐵 ∧ 〈𝑢, 𝑢〉 ∈ 𝑅) → 𝑢 ∈ 𝐵)) |
79 | 69, 78 | syl5bir 153 |
. . . . . 6
⊢
(∃𝑥 𝑥 ∈ 𝐴 → ((∀𝑥 ∈ 𝐴 𝑅 Er 𝐵 ∧ ∀𝑥 ∈ 𝐴 〈𝑢, 𝑢〉 ∈ 𝑅) → 𝑢 ∈ 𝐵)) |
80 | 79 | expdimp 259 |
. . . . 5
⊢
((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → (∀𝑥 ∈ 𝐴 〈𝑢, 𝑢〉 ∈ 𝑅 → 𝑢 ∈ 𝐵)) |
81 | 68, 80 | impbid 129 |
. . . 4
⊢
((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → (𝑢 ∈ 𝐵 ↔ ∀𝑥 ∈ 𝐴 〈𝑢, 𝑢〉 ∈ 𝑅)) |
82 | | df-br 3999 |
. . . . 5
⊢ (𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑢 ↔ 〈𝑢, 𝑢〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅) |
83 | 24, 24 | opex 4223 |
. . . . . 6
⊢
〈𝑢, 𝑢〉 ∈ V |
84 | | eliin 3887 |
. . . . . 6
⊢
(〈𝑢, 𝑢〉 ∈ V →
(〈𝑢, 𝑢〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀𝑥 ∈ 𝐴 〈𝑢, 𝑢〉 ∈ 𝑅)) |
85 | 83, 84 | ax-mp 5 |
. . . . 5
⊢
(〈𝑢, 𝑢〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀𝑥 ∈ 𝐴 〈𝑢, 𝑢〉 ∈ 𝑅) |
86 | 82, 85 | bitri 184 |
. . . 4
⊢ (𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑢 ↔ ∀𝑥 ∈ 𝐴 〈𝑢, 𝑢〉 ∈ 𝑅) |
87 | 81, 86 | bitr4di 198 |
. . 3
⊢
((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → (𝑢 ∈ 𝐵 ↔ 𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑢)) |
88 | 14, 36, 59, 87 | iserd 6551 |
. 2
⊢
((∃𝑥 𝑥 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → ∩
𝑥 ∈ 𝐴 𝑅 Er 𝐵) |
89 | 5, 88 | sylanbr 285 |
1
⊢
((∃𝑦 𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → ∩
𝑥 ∈ 𝐴 𝑅 Er 𝐵) |