Proof of Theorem efgrelexlema
Step | Hyp | Ref
| Expression |
1 | | efgrelexlem.1 |
. . 3
⊢ 𝐿 = {〈𝑖, 𝑗〉 ∣ ∃𝑐 ∈ (◡𝑆 “ {𝑖})∃𝑑 ∈ (◡𝑆 “ {𝑗})(𝑐‘0) = (𝑑‘0)} |
2 | 1 | bropaex12 5607 |
. 2
⊢ (𝐴𝐿𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
3 | | n0i 4220 |
. . . . . 6
⊢ (𝑎 ∈ (◡𝑆 “ {𝐴}) → ¬ (◡𝑆 “ {𝐴}) = ∅) |
4 | | snprc 4605 |
. . . . . . . 8
⊢ (¬
𝐴 ∈ V ↔ {𝐴} = ∅) |
5 | | imaeq2 5893 |
. . . . . . . 8
⊢ ({𝐴} = ∅ → (◡𝑆 “ {𝐴}) = (◡𝑆 “ ∅)) |
6 | 4, 5 | sylbi 220 |
. . . . . . 7
⊢ (¬
𝐴 ∈ V → (◡𝑆 “ {𝐴}) = (◡𝑆 “ ∅)) |
7 | | ima0 5913 |
. . . . . . 7
⊢ (◡𝑆 “ ∅) = ∅ |
8 | 6, 7 | eqtrdi 2789 |
. . . . . 6
⊢ (¬
𝐴 ∈ V → (◡𝑆 “ {𝐴}) = ∅) |
9 | 3, 8 | nsyl2 143 |
. . . . 5
⊢ (𝑎 ∈ (◡𝑆 “ {𝐴}) → 𝐴 ∈ V) |
10 | | n0i 4220 |
. . . . . 6
⊢ (𝑏 ∈ (◡𝑆 “ {𝐵}) → ¬ (◡𝑆 “ {𝐵}) = ∅) |
11 | | snprc 4605 |
. . . . . . . 8
⊢ (¬
𝐵 ∈ V ↔ {𝐵} = ∅) |
12 | | imaeq2 5893 |
. . . . . . . 8
⊢ ({𝐵} = ∅ → (◡𝑆 “ {𝐵}) = (◡𝑆 “ ∅)) |
13 | 11, 12 | sylbi 220 |
. . . . . . 7
⊢ (¬
𝐵 ∈ V → (◡𝑆 “ {𝐵}) = (◡𝑆 “ ∅)) |
14 | 13, 7 | eqtrdi 2789 |
. . . . . 6
⊢ (¬
𝐵 ∈ V → (◡𝑆 “ {𝐵}) = ∅) |
15 | 10, 14 | nsyl2 143 |
. . . . 5
⊢ (𝑏 ∈ (◡𝑆 “ {𝐵}) → 𝐵 ∈ V) |
16 | 9, 15 | anim12i 616 |
. . . 4
⊢ ((𝑎 ∈ (◡𝑆 “ {𝐴}) ∧ 𝑏 ∈ (◡𝑆 “ {𝐵})) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
17 | 16 | a1d 25 |
. . 3
⊢ ((𝑎 ∈ (◡𝑆 “ {𝐴}) ∧ 𝑏 ∈ (◡𝑆 “ {𝐵})) → ((𝑎‘0) = (𝑏‘0) → (𝐴 ∈ V ∧ 𝐵 ∈ V))) |
18 | 17 | rexlimivv 3201 |
. 2
⊢
(∃𝑎 ∈
(◡𝑆 “ {𝐴})∃𝑏 ∈ (◡𝑆 “ {𝐵})(𝑎‘0) = (𝑏‘0) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
19 | | fveq1 6667 |
. . . . . 6
⊢ (𝑐 = 𝑎 → (𝑐‘0) = (𝑎‘0)) |
20 | 19 | eqeq1d 2740 |
. . . . 5
⊢ (𝑐 = 𝑎 → ((𝑐‘0) = (𝑑‘0) ↔ (𝑎‘0) = (𝑑‘0))) |
21 | | fveq1 6667 |
. . . . . 6
⊢ (𝑑 = 𝑏 → (𝑑‘0) = (𝑏‘0)) |
22 | 21 | eqeq2d 2749 |
. . . . 5
⊢ (𝑑 = 𝑏 → ((𝑎‘0) = (𝑑‘0) ↔ (𝑎‘0) = (𝑏‘0))) |
23 | 20, 22 | cbvrex2vw 3362 |
. . . 4
⊢
(∃𝑐 ∈
(◡𝑆 “ {𝑖})∃𝑑 ∈ (◡𝑆 “ {𝑗})(𝑐‘0) = (𝑑‘0) ↔ ∃𝑎 ∈ (◡𝑆 “ {𝑖})∃𝑏 ∈ (◡𝑆 “ {𝑗})(𝑎‘0) = (𝑏‘0)) |
24 | | sneq 4523 |
. . . . . 6
⊢ (𝑖 = 𝐴 → {𝑖} = {𝐴}) |
25 | 24 | imaeq2d 5897 |
. . . . 5
⊢ (𝑖 = 𝐴 → (◡𝑆 “ {𝑖}) = (◡𝑆 “ {𝐴})) |
26 | 25 | rexeqdv 3316 |
. . . 4
⊢ (𝑖 = 𝐴 → (∃𝑎 ∈ (◡𝑆 “ {𝑖})∃𝑏 ∈ (◡𝑆 “ {𝑗})(𝑎‘0) = (𝑏‘0) ↔ ∃𝑎 ∈ (◡𝑆 “ {𝐴})∃𝑏 ∈ (◡𝑆 “ {𝑗})(𝑎‘0) = (𝑏‘0))) |
27 | 23, 26 | syl5bb 286 |
. . 3
⊢ (𝑖 = 𝐴 → (∃𝑐 ∈ (◡𝑆 “ {𝑖})∃𝑑 ∈ (◡𝑆 “ {𝑗})(𝑐‘0) = (𝑑‘0) ↔ ∃𝑎 ∈ (◡𝑆 “ {𝐴})∃𝑏 ∈ (◡𝑆 “ {𝑗})(𝑎‘0) = (𝑏‘0))) |
28 | | sneq 4523 |
. . . . . 6
⊢ (𝑗 = 𝐵 → {𝑗} = {𝐵}) |
29 | 28 | imaeq2d 5897 |
. . . . 5
⊢ (𝑗 = 𝐵 → (◡𝑆 “ {𝑗}) = (◡𝑆 “ {𝐵})) |
30 | 29 | rexeqdv 3316 |
. . . 4
⊢ (𝑗 = 𝐵 → (∃𝑏 ∈ (◡𝑆 “ {𝑗})(𝑎‘0) = (𝑏‘0) ↔ ∃𝑏 ∈ (◡𝑆 “ {𝐵})(𝑎‘0) = (𝑏‘0))) |
31 | 30 | rexbidv 3206 |
. . 3
⊢ (𝑗 = 𝐵 → (∃𝑎 ∈ (◡𝑆 “ {𝐴})∃𝑏 ∈ (◡𝑆 “ {𝑗})(𝑎‘0) = (𝑏‘0) ↔ ∃𝑎 ∈ (◡𝑆 “ {𝐴})∃𝑏 ∈ (◡𝑆 “ {𝐵})(𝑎‘0) = (𝑏‘0))) |
32 | 27, 31, 1 | brabg 5391 |
. 2
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐿𝐵 ↔ ∃𝑎 ∈ (◡𝑆 “ {𝐴})∃𝑏 ∈ (◡𝑆 “ {𝐵})(𝑎‘0) = (𝑏‘0))) |
33 | 2, 18, 32 | pm5.21nii 383 |
1
⊢ (𝐴𝐿𝐵 ↔ ∃𝑎 ∈ (◡𝑆 “ {𝐴})∃𝑏 ∈ (◡𝑆 “ {𝐵})(𝑎‘0) = (𝑏‘0)) |