| Step | Hyp | Ref
| Expression |
| 1 | | vex 3484 |
. . . . . 6
⊢ 𝑧 ∈ V |
| 2 | | neeq1 3003 |
. . . . . . 7
⊢ (𝑢 = 𝑧 → (𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅)) |
| 3 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑢 = 𝑧 → (𝑢 = ({𝑡} × 𝑡) ↔ 𝑧 = ({𝑡} × 𝑡))) |
| 4 | 3 | rexbidv 3179 |
. . . . . . 7
⊢ (𝑢 = 𝑧 → (∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡) ↔ ∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡))) |
| 5 | 2, 4 | anbi12d 632 |
. . . . . 6
⊢ (𝑢 = 𝑧 → ((𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡)))) |
| 6 | 1, 5 | elab 3679 |
. . . . 5
⊢ (𝑧 ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡))) |
| 7 | 6 | simplbi 497 |
. . . 4
⊢ (𝑧 ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} → 𝑧 ≠ ∅) |
| 8 | | dfac5lem.1 |
. . . 4
⊢ 𝐴 = {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} |
| 9 | 7, 8 | eleq2s 2859 |
. . 3
⊢ (𝑧 ∈ 𝐴 → 𝑧 ≠ ∅) |
| 10 | 9 | rgen 3063 |
. 2
⊢
∀𝑧 ∈
𝐴 𝑧 ≠ ∅ |
| 11 | | df-an 396 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) ↔ ¬ (𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤)) |
| 12 | 1, 5, 8 | elab2 3682 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝐴 ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡))) |
| 13 | 12 | simprbi 496 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝐴 → ∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡)) |
| 14 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑤 ∈ V |
| 15 | | neeq1 3003 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑤 → (𝑢 ≠ ∅ ↔ 𝑤 ≠ ∅)) |
| 16 | | eqeq1 2741 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑤 → (𝑢 = ({𝑡} × 𝑡) ↔ 𝑤 = ({𝑡} × 𝑡))) |
| 17 | 16 | rexbidv 3179 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑤 → (∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡) ↔ ∃𝑡 ∈ ℎ 𝑤 = ({𝑡} × 𝑡))) |
| 18 | 15, 17 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑤 → ((𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑤 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑤 = ({𝑡} × 𝑡)))) |
| 19 | 14, 18, 8 | elab2 3682 |
. . . . . . . . . 10
⊢ (𝑤 ∈ 𝐴 ↔ (𝑤 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑤 = ({𝑡} × 𝑡))) |
| 20 | 19 | simprbi 496 |
. . . . . . . . 9
⊢ (𝑤 ∈ 𝐴 → ∃𝑡 ∈ ℎ 𝑤 = ({𝑡} × 𝑡)) |
| 21 | | sneq 4636 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑔 → {𝑡} = {𝑔}) |
| 22 | 21 | xpeq1d 5714 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑔 → ({𝑡} × 𝑡) = ({𝑔} × 𝑡)) |
| 23 | | xpeq2 5706 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑔 → ({𝑔} × 𝑡) = ({𝑔} × 𝑔)) |
| 24 | 22, 23 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑔 → ({𝑡} × 𝑡) = ({𝑔} × 𝑔)) |
| 25 | 24 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑔 → (𝑤 = ({𝑡} × 𝑡) ↔ 𝑤 = ({𝑔} × 𝑔))) |
| 26 | 25 | cbvrexvw 3238 |
. . . . . . . . 9
⊢
(∃𝑡 ∈
ℎ 𝑤 = ({𝑡} × 𝑡) ↔ ∃𝑔 ∈ ℎ 𝑤 = ({𝑔} × 𝑔)) |
| 27 | 20, 26 | sylib 218 |
. . . . . . . 8
⊢ (𝑤 ∈ 𝐴 → ∃𝑔 ∈ ℎ 𝑤 = ({𝑔} × 𝑔)) |
| 28 | | eleq2 2830 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = ({𝑡} × 𝑡) → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ ({𝑡} × 𝑡))) |
| 29 | | elxp 5708 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ({𝑡} × 𝑡) ↔ ∃𝑢∃𝑣(𝑥 = 〈𝑢, 𝑣〉 ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡))) |
| 30 | | opeq1 4873 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 = 𝑠 → 〈𝑢, 𝑣〉 = 〈𝑠, 𝑣〉) |
| 31 | 30 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 = 𝑠 → (𝑥 = 〈𝑢, 𝑣〉 ↔ 𝑥 = 〈𝑠, 𝑣〉)) |
| 32 | | eleq1w 2824 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 = 𝑠 → (𝑢 ∈ {𝑡} ↔ 𝑠 ∈ {𝑡})) |
| 33 | 32 | anbi1d 631 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 = 𝑠 → ((𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡) ↔ (𝑠 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡))) |
| 34 | 31, 33 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 = 𝑠 → ((𝑥 = 〈𝑢, 𝑣〉 ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ↔ (𝑥 = 〈𝑠, 𝑣〉 ∧ (𝑠 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)))) |
| 35 | 34 | excomimw 2043 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑢∃𝑣(𝑥 = 〈𝑢, 𝑣〉 ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) → ∃𝑣∃𝑢(𝑥 = 〈𝑢, 𝑣〉 ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡))) |
| 36 | 29, 35 | sylbi 217 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ({𝑡} × 𝑡) → ∃𝑣∃𝑢(𝑥 = 〈𝑢, 𝑣〉 ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡))) |
| 37 | 28, 36 | biimtrdi 253 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = ({𝑡} × 𝑡) → (𝑥 ∈ 𝑧 → ∃𝑣∃𝑢(𝑥 = 〈𝑢, 𝑣〉 ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)))) |
| 38 | | eleq2 2830 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = ({𝑔} × 𝑔) → (𝑥 ∈ 𝑤 ↔ 𝑥 ∈ ({𝑔} × 𝑔))) |
| 39 | | elxp 5708 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ({𝑔} × 𝑔) ↔ ∃𝑢∃𝑦(𝑥 = 〈𝑢, 𝑦〉 ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))) |
| 40 | | opeq1 4873 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 = 𝑠 → 〈𝑢, 𝑦〉 = 〈𝑠, 𝑦〉) |
| 41 | 40 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 = 𝑠 → (𝑥 = 〈𝑢, 𝑦〉 ↔ 𝑥 = 〈𝑠, 𝑦〉)) |
| 42 | | eleq1w 2824 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 = 𝑠 → (𝑢 ∈ {𝑔} ↔ 𝑠 ∈ {𝑔})) |
| 43 | 42 | anbi1d 631 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 = 𝑠 → ((𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔) ↔ (𝑠 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))) |
| 44 | 41, 43 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 = 𝑠 → ((𝑥 = 〈𝑢, 𝑦〉 ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)) ↔ (𝑥 = 〈𝑠, 𝑦〉 ∧ (𝑠 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)))) |
| 45 | 44 | excomimw 2043 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑢∃𝑦(𝑥 = 〈𝑢, 𝑦〉 ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)) → ∃𝑦∃𝑢(𝑥 = 〈𝑢, 𝑦〉 ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))) |
| 46 | 39, 45 | sylbi 217 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ({𝑔} × 𝑔) → ∃𝑦∃𝑢(𝑥 = 〈𝑢, 𝑦〉 ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))) |
| 47 | 38, 46 | biimtrdi 253 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = ({𝑔} × 𝑔) → (𝑥 ∈ 𝑤 → ∃𝑦∃𝑢(𝑥 = 〈𝑢, 𝑦〉 ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)))) |
| 48 | 37, 47 | im2anan9 620 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → (∃𝑣∃𝑢(𝑥 = 〈𝑢, 𝑣〉 ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑦∃𝑢(𝑥 = 〈𝑢, 𝑦〉 ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))))) |
| 49 | | exdistrv 1955 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑣∃𝑦(∃𝑢(𝑥 = 〈𝑢, 𝑣〉 ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑢(𝑥 = 〈𝑢, 𝑦〉 ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))) ↔ (∃𝑣∃𝑢(𝑥 = 〈𝑢, 𝑣〉 ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑦∃𝑢(𝑥 = 〈𝑢, 𝑦〉 ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)))) |
| 50 | 48, 49 | imbitrrdi 252 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → ∃𝑣∃𝑦(∃𝑢(𝑥 = 〈𝑢, 𝑣〉 ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑢(𝑥 = 〈𝑢, 𝑦〉 ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))))) |
| 51 | | velsn 4642 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 ∈ {𝑡} ↔ 𝑢 = 𝑡) |
| 52 | | opeq1 4873 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 = 𝑡 → 〈𝑢, 𝑣〉 = 〈𝑡, 𝑣〉) |
| 53 | 52 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 = 𝑡 → (𝑥 = 〈𝑢, 𝑣〉 ↔ 𝑥 = 〈𝑡, 𝑣〉)) |
| 54 | 53 | biimpac 478 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 = 〈𝑢, 𝑣〉 ∧ 𝑢 = 𝑡) → 𝑥 = 〈𝑡, 𝑣〉) |
| 55 | 51, 54 | sylan2b 594 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = 〈𝑢, 𝑣〉 ∧ 𝑢 ∈ {𝑡}) → 𝑥 = 〈𝑡, 𝑣〉) |
| 56 | 55 | adantrr 717 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = 〈𝑢, 𝑣〉 ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) → 𝑥 = 〈𝑡, 𝑣〉) |
| 57 | 56 | exlimiv 1930 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑢(𝑥 = 〈𝑢, 𝑣〉 ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) → 𝑥 = 〈𝑡, 𝑣〉) |
| 58 | | velsn 4642 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 ∈ {𝑔} ↔ 𝑢 = 𝑔) |
| 59 | | opeq1 4873 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 = 𝑔 → 〈𝑢, 𝑦〉 = 〈𝑔, 𝑦〉) |
| 60 | 59 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 = 𝑔 → (𝑥 = 〈𝑢, 𝑦〉 ↔ 𝑥 = 〈𝑔, 𝑦〉)) |
| 61 | 60 | biimpac 478 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 = 〈𝑢, 𝑦〉 ∧ 𝑢 = 𝑔) → 𝑥 = 〈𝑔, 𝑦〉) |
| 62 | 58, 61 | sylan2b 594 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = 〈𝑢, 𝑦〉 ∧ 𝑢 ∈ {𝑔}) → 𝑥 = 〈𝑔, 𝑦〉) |
| 63 | 62 | adantrr 717 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = 〈𝑢, 𝑦〉 ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)) → 𝑥 = 〈𝑔, 𝑦〉) |
| 64 | 63 | exlimiv 1930 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑢(𝑥 = 〈𝑢, 𝑦〉 ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)) → 𝑥 = 〈𝑔, 𝑦〉) |
| 65 | 57, 64 | sylan9req 2798 |
. . . . . . . . . . . . . . . . 17
⊢
((∃𝑢(𝑥 = 〈𝑢, 𝑣〉 ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑢(𝑥 = 〈𝑢, 𝑦〉 ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))) → 〈𝑡, 𝑣〉 = 〈𝑔, 𝑦〉) |
| 66 | | vex 3484 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑡 ∈ V |
| 67 | | vex 3484 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑣 ∈ V |
| 68 | 66, 67 | opth1 5480 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑡, 𝑣〉 = 〈𝑔, 𝑦〉 → 𝑡 = 𝑔) |
| 69 | 65, 68 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((∃𝑢(𝑥 = 〈𝑢, 𝑣〉 ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑢(𝑥 = 〈𝑢, 𝑦〉 ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))) → 𝑡 = 𝑔) |
| 70 | 69 | exlimivv 1932 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑣∃𝑦(∃𝑢(𝑥 = 〈𝑢, 𝑣〉 ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑢(𝑥 = 〈𝑢, 𝑦〉 ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))) → 𝑡 = 𝑔) |
| 71 | 50, 70 | syl6 35 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑡 = 𝑔)) |
| 72 | 71, 24 | syl6 35 |
. . . . . . . . . . . . 13
⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → ({𝑡} × 𝑡) = ({𝑔} × 𝑔))) |
| 73 | | eqeq12 2754 |
. . . . . . . . . . . . 13
⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → (𝑧 = 𝑤 ↔ ({𝑡} × 𝑡) = ({𝑔} × 𝑔))) |
| 74 | 72, 73 | sylibrd 259 |
. . . . . . . . . . . 12
⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤)) |
| 75 | 74 | ex 412 |
. . . . . . . . . . 11
⊢ (𝑧 = ({𝑡} × 𝑡) → (𝑤 = ({𝑔} × 𝑔) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤))) |
| 76 | 75 | rexlimivw 3151 |
. . . . . . . . . 10
⊢
(∃𝑡 ∈
ℎ 𝑧 = ({𝑡} × 𝑡) → (𝑤 = ({𝑔} × 𝑔) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤))) |
| 77 | 76 | rexlimdvw 3160 |
. . . . . . . . 9
⊢
(∃𝑡 ∈
ℎ 𝑧 = ({𝑡} × 𝑡) → (∃𝑔 ∈ ℎ 𝑤 = ({𝑔} × 𝑔) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤))) |
| 78 | 77 | imp 406 |
. . . . . . . 8
⊢
((∃𝑡 ∈
ℎ 𝑧 = ({𝑡} × 𝑡) ∧ ∃𝑔 ∈ ℎ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤)) |
| 79 | 13, 27, 78 | syl2an 596 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤)) |
| 80 | 11, 79 | biimtrrid 243 |
. . . . . 6
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (¬ (𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤)) |
| 81 | 80 | necon1ad 2957 |
. . . . 5
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (𝑧 ≠ 𝑤 → (𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤))) |
| 82 | 81 | alrimdv 1929 |
. . . 4
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (𝑧 ≠ 𝑤 → ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤))) |
| 83 | | disj1 4452 |
. . . 4
⊢ ((𝑧 ∩ 𝑤) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤)) |
| 84 | 82, 83 | imbitrrdi 252 |
. . 3
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) |
| 85 | 84 | rgen2 3199 |
. 2
⊢
∀𝑧 ∈
𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) |
| 86 | | dfac5lem.2 |
. . 3
⊢ (𝜑 ↔ ∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))) |
| 87 | | vex 3484 |
. . . . . . . 8
⊢ ℎ ∈ V |
| 88 | | vuniex 7759 |
. . . . . . . 8
⊢ ∪ ℎ
∈ V |
| 89 | 87, 88 | xpex 7773 |
. . . . . . 7
⊢ (ℎ × ∪ ℎ)
∈ V |
| 90 | 89 | pwex 5380 |
. . . . . 6
⊢ 𝒫
(ℎ × ∪ ℎ)
∈ V |
| 91 | | snssi 4808 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ ℎ → {𝑡} ⊆ ℎ) |
| 92 | | elssuni 4937 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ ℎ → 𝑡 ⊆ ∪ ℎ) |
| 93 | | xpss12 5700 |
. . . . . . . . . . . 12
⊢ (({𝑡} ⊆ ℎ ∧ 𝑡 ⊆ ∪ ℎ) → ({𝑡} × 𝑡) ⊆ (ℎ × ∪ ℎ)) |
| 94 | 91, 92, 93 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ ℎ → ({𝑡} × 𝑡) ⊆ (ℎ × ∪ ℎ)) |
| 95 | | vsnex 5434 |
. . . . . . . . . . . . 13
⊢ {𝑡} ∈ V |
| 96 | 95, 66 | xpex 7773 |
. . . . . . . . . . . 12
⊢ ({𝑡} × 𝑡) ∈ V |
| 97 | 96 | elpw 4604 |
. . . . . . . . . . 11
⊢ (({𝑡} × 𝑡) ∈ 𝒫 (ℎ × ∪ ℎ) ↔ ({𝑡} × 𝑡) ⊆ (ℎ × ∪ ℎ)) |
| 98 | 94, 97 | sylibr 234 |
. . . . . . . . . 10
⊢ (𝑡 ∈ ℎ → ({𝑡} × 𝑡) ∈ 𝒫 (ℎ × ∪ ℎ)) |
| 99 | | eleq1 2829 |
. . . . . . . . . 10
⊢ (𝑢 = ({𝑡} × 𝑡) → (𝑢 ∈ 𝒫 (ℎ × ∪ ℎ) ↔ ({𝑡} × 𝑡) ∈ 𝒫 (ℎ × ∪ ℎ))) |
| 100 | 98, 99 | syl5ibrcom 247 |
. . . . . . . . 9
⊢ (𝑡 ∈ ℎ → (𝑢 = ({𝑡} × 𝑡) → 𝑢 ∈ 𝒫 (ℎ × ∪ ℎ))) |
| 101 | 100 | rexlimiv 3148 |
. . . . . . . 8
⊢
(∃𝑡 ∈
ℎ 𝑢 = ({𝑡} × 𝑡) → 𝑢 ∈ 𝒫 (ℎ × ∪ ℎ)) |
| 102 | 101 | adantl 481 |
. . . . . . 7
⊢ ((𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)) → 𝑢 ∈ 𝒫 (ℎ × ∪ ℎ)) |
| 103 | 102 | abssi 4070 |
. . . . . 6
⊢ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ⊆ 𝒫 (ℎ × ∪ ℎ) |
| 104 | 90, 103 | ssexi 5322 |
. . . . 5
⊢ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ∈ V |
| 105 | 8, 104 | eqeltri 2837 |
. . . 4
⊢ 𝐴 ∈ V |
| 106 | | raleq 3323 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ↔ ∀𝑧 ∈ 𝐴 𝑧 ≠ ∅)) |
| 107 | | raleq 3323 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) |
| 108 | 107 | raleqbi1dv 3338 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) |
| 109 | 106, 108 | anbi12d 632 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) ↔ (∀𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)))) |
| 110 | | raleq 3323 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))) |
| 111 | 110 | exbidv 1921 |
. . . . 5
⊢ (𝑥 = 𝐴 → (∃𝑦∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∃𝑦∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))) |
| 112 | 109, 111 | imbi12d 344 |
. . . 4
⊢ (𝑥 = 𝐴 → (((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) ↔ ((∀𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)))) |
| 113 | 105, 112 | spcv 3605 |
. . 3
⊢
(∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) → ((∀𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))) |
| 114 | 86, 113 | sylbi 217 |
. 2
⊢ (𝜑 → ((∀𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))) |
| 115 | 10, 85, 114 | mp2ani 698 |
1
⊢ (𝜑 → ∃𝑦∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) |