Step | Hyp | Ref
| Expression |
1 | | vex 3451 |
. . . . . 6
⊢ 𝑧 ∈ V |
2 | | neeq1 3003 |
. . . . . . 7
⊢ (𝑢 = 𝑧 → (𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅)) |
3 | | eqeq1 2737 |
. . . . . . . 8
⊢ (𝑢 = 𝑧 → (𝑢 = ({𝑡} × 𝑡) ↔ 𝑧 = ({𝑡} × 𝑡))) |
4 | 3 | rexbidv 3172 |
. . . . . . 7
⊢ (𝑢 = 𝑧 → (∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡) ↔ ∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡))) |
5 | 2, 4 | anbi12d 632 |
. . . . . 6
⊢ (𝑢 = 𝑧 → ((𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡)))) |
6 | 1, 5 | elab 3634 |
. . . . 5
⊢ (𝑧 ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡))) |
7 | 6 | simplbi 499 |
. . . 4
⊢ (𝑧 ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} → 𝑧 ≠ ∅) |
8 | | dfac5lem.1 |
. . . 4
⊢ 𝐴 = {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} |
9 | 7, 8 | eleq2s 2852 |
. . 3
⊢ (𝑧 ∈ 𝐴 → 𝑧 ≠ ∅) |
10 | 9 | rgen 3063 |
. 2
⊢
∀𝑧 ∈
𝐴 𝑧 ≠ ∅ |
11 | | df-an 398 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) ↔ ¬ (𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤)) |
12 | 1, 5, 8 | elab2 3638 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝐴 ↔ (𝑧 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡))) |
13 | 12 | simprbi 498 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝐴 → ∃𝑡 ∈ ℎ 𝑧 = ({𝑡} × 𝑡)) |
14 | | vex 3451 |
. . . . . . . . . . 11
⊢ 𝑤 ∈ V |
15 | | neeq1 3003 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑤 → (𝑢 ≠ ∅ ↔ 𝑤 ≠ ∅)) |
16 | | eqeq1 2737 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑤 → (𝑢 = ({𝑡} × 𝑡) ↔ 𝑤 = ({𝑡} × 𝑡))) |
17 | 16 | rexbidv 3172 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑤 → (∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡) ↔ ∃𝑡 ∈ ℎ 𝑤 = ({𝑡} × 𝑡))) |
18 | 15, 17 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑤 → ((𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑤 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑤 = ({𝑡} × 𝑡)))) |
19 | 14, 18, 8 | elab2 3638 |
. . . . . . . . . 10
⊢ (𝑤 ∈ 𝐴 ↔ (𝑤 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑤 = ({𝑡} × 𝑡))) |
20 | 19 | simprbi 498 |
. . . . . . . . 9
⊢ (𝑤 ∈ 𝐴 → ∃𝑡 ∈ ℎ 𝑤 = ({𝑡} × 𝑡)) |
21 | | sneq 4600 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑔 → {𝑡} = {𝑔}) |
22 | 21 | xpeq1d 5666 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑔 → ({𝑡} × 𝑡) = ({𝑔} × 𝑡)) |
23 | | xpeq2 5658 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑔 → ({𝑔} × 𝑡) = ({𝑔} × 𝑔)) |
24 | 22, 23 | eqtrd 2773 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑔 → ({𝑡} × 𝑡) = ({𝑔} × 𝑔)) |
25 | 24 | eqeq2d 2744 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑔 → (𝑤 = ({𝑡} × 𝑡) ↔ 𝑤 = ({𝑔} × 𝑔))) |
26 | 25 | cbvrexvw 3225 |
. . . . . . . . 9
⊢
(∃𝑡 ∈
ℎ 𝑤 = ({𝑡} × 𝑡) ↔ ∃𝑔 ∈ ℎ 𝑤 = ({𝑔} × 𝑔)) |
27 | 20, 26 | sylib 217 |
. . . . . . . 8
⊢ (𝑤 ∈ 𝐴 → ∃𝑔 ∈ ℎ 𝑤 = ({𝑔} × 𝑔)) |
28 | | eleq2 2823 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = ({𝑡} × 𝑡) → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ ({𝑡} × 𝑡))) |
29 | | elxp 5660 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ({𝑡} × 𝑡) ↔ ∃𝑢∃𝑣(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡))) |
30 | | excom 2163 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑢∃𝑣(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ↔ ∃𝑣∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡))) |
31 | 29, 30 | bitri 275 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ({𝑡} × 𝑡) ↔ ∃𝑣∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡))) |
32 | 28, 31 | bitrdi 287 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = ({𝑡} × 𝑡) → (𝑥 ∈ 𝑧 ↔ ∃𝑣∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)))) |
33 | | eleq2 2823 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = ({𝑔} × 𝑔) → (𝑥 ∈ 𝑤 ↔ 𝑥 ∈ ({𝑔} × 𝑔))) |
34 | | elxp 5660 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ({𝑔} × 𝑔) ↔ ∃𝑢∃𝑦(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))) |
35 | | excom 2163 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑢∃𝑦(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)) ↔ ∃𝑦∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))) |
36 | 34, 35 | bitri 275 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ({𝑔} × 𝑔) ↔ ∃𝑦∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))) |
37 | 33, 36 | bitrdi 287 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = ({𝑔} × 𝑔) → (𝑥 ∈ 𝑤 ↔ ∃𝑦∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)))) |
38 | 32, 37 | bi2anan9 638 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) ↔ (∃𝑣∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑦∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))))) |
39 | | exdistrv 1960 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑣∃𝑦(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))) ↔ (∃𝑣∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑦∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)))) |
40 | 38, 39 | bitr4di 289 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) ↔ ∃𝑣∃𝑦(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))))) |
41 | | velsn 4606 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 ∈ {𝑡} ↔ 𝑢 = 𝑡) |
42 | | opeq1 4834 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 = 𝑡 → ⟨𝑢, 𝑣⟩ = ⟨𝑡, 𝑣⟩) |
43 | 42 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 = 𝑡 → (𝑥 = ⟨𝑢, 𝑣⟩ ↔ 𝑥 = ⟨𝑡, 𝑣⟩)) |
44 | 43 | biimpac 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 = 𝑡) → 𝑥 = ⟨𝑡, 𝑣⟩) |
45 | 41, 44 | sylan2b 595 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ 𝑢 ∈ {𝑡}) → 𝑥 = ⟨𝑡, 𝑣⟩) |
46 | 45 | adantrr 716 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) → 𝑥 = ⟨𝑡, 𝑣⟩) |
47 | 46 | exlimiv 1934 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) → 𝑥 = ⟨𝑡, 𝑣⟩) |
48 | | velsn 4606 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 ∈ {𝑔} ↔ 𝑢 = 𝑔) |
49 | | opeq1 4834 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 = 𝑔 → ⟨𝑢, 𝑦⟩ = ⟨𝑔, 𝑦⟩) |
50 | 49 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 = 𝑔 → (𝑥 = ⟨𝑢, 𝑦⟩ ↔ 𝑥 = ⟨𝑔, 𝑦⟩)) |
51 | 50 | biimpac 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ 𝑢 = 𝑔) → 𝑥 = ⟨𝑔, 𝑦⟩) |
52 | 48, 51 | sylan2b 595 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ 𝑢 ∈ {𝑔}) → 𝑥 = ⟨𝑔, 𝑦⟩) |
53 | 52 | adantrr 716 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)) → 𝑥 = ⟨𝑔, 𝑦⟩) |
54 | 53 | exlimiv 1934 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔)) → 𝑥 = ⟨𝑔, 𝑦⟩) |
55 | 47, 54 | sylan9req 2794 |
. . . . . . . . . . . . . . . . 17
⊢
((∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))) → ⟨𝑡, 𝑣⟩ = ⟨𝑔, 𝑦⟩) |
56 | | vex 3451 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑡 ∈ V |
57 | | vex 3451 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑣 ∈ V |
58 | 56, 57 | opth1 5436 |
. . . . . . . . . . . . . . . . 17
⊢
(⟨𝑡, 𝑣⟩ = ⟨𝑔, 𝑦⟩ → 𝑡 = 𝑔) |
59 | 55, 58 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))) → 𝑡 = 𝑔) |
60 | 59 | exlimivv 1936 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑣∃𝑦(∃𝑢(𝑥 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ {𝑡} ∧ 𝑣 ∈ 𝑡)) ∧ ∃𝑢(𝑥 = ⟨𝑢, 𝑦⟩ ∧ (𝑢 ∈ {𝑔} ∧ 𝑦 ∈ 𝑔))) → 𝑡 = 𝑔) |
61 | 40, 60 | syl6bi 253 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑡 = 𝑔)) |
62 | 61, 24 | syl6 35 |
. . . . . . . . . . . . 13
⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → ({𝑡} × 𝑡) = ({𝑔} × 𝑔))) |
63 | | eqeq12 2750 |
. . . . . . . . . . . . 13
⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → (𝑧 = 𝑤 ↔ ({𝑡} × 𝑡) = ({𝑔} × 𝑔))) |
64 | 62, 63 | sylibrd 259 |
. . . . . . . . . . . 12
⊢ ((𝑧 = ({𝑡} × 𝑡) ∧ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤)) |
65 | 64 | ex 414 |
. . . . . . . . . . 11
⊢ (𝑧 = ({𝑡} × 𝑡) → (𝑤 = ({𝑔} × 𝑔) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤))) |
66 | 65 | rexlimivw 3145 |
. . . . . . . . . 10
⊢
(∃𝑡 ∈
ℎ 𝑧 = ({𝑡} × 𝑡) → (𝑤 = ({𝑔} × 𝑔) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤))) |
67 | 66 | rexlimdvw 3154 |
. . . . . . . . 9
⊢
(∃𝑡 ∈
ℎ 𝑧 = ({𝑡} × 𝑡) → (∃𝑔 ∈ ℎ 𝑤 = ({𝑔} × 𝑔) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤))) |
68 | 67 | imp 408 |
. . . . . . . 8
⊢
((∃𝑡 ∈
ℎ 𝑧 = ({𝑡} × 𝑡) ∧ ∃𝑔 ∈ ℎ 𝑤 = ({𝑔} × 𝑔)) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤)) |
69 | 13, 27, 68 | syl2an 597 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → ((𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤)) |
70 | 11, 69 | biimtrrid 242 |
. . . . . 6
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (¬ (𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤) → 𝑧 = 𝑤)) |
71 | 70 | necon1ad 2957 |
. . . . 5
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (𝑧 ≠ 𝑤 → (𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤))) |
72 | 71 | alrimdv 1933 |
. . . 4
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (𝑧 ≠ 𝑤 → ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤))) |
73 | | disj1 4414 |
. . . 4
⊢ ((𝑧 ∩ 𝑤) = ∅ ↔ ∀𝑥(𝑥 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑤)) |
74 | 72, 73 | syl6ibr 252 |
. . 3
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) → (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) |
75 | 74 | rgen2 3191 |
. 2
⊢
∀𝑧 ∈
𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) |
76 | | dfac5lem.3 |
. . 3
⊢ (𝜑 ↔ ∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))) |
77 | | vex 3451 |
. . . . . . . 8
⊢ ℎ ∈ V |
78 | | vuniex 7680 |
. . . . . . . 8
⊢ ∪ ℎ
∈ V |
79 | 77, 78 | xpex 7691 |
. . . . . . 7
⊢ (ℎ × ∪ ℎ)
∈ V |
80 | 79 | pwex 5339 |
. . . . . 6
⊢ 𝒫
(ℎ × ∪ ℎ)
∈ V |
81 | | snssi 4772 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ ℎ → {𝑡} ⊆ ℎ) |
82 | | elssuni 4902 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ ℎ → 𝑡 ⊆ ∪ ℎ) |
83 | | xpss12 5652 |
. . . . . . . . . . . 12
⊢ (({𝑡} ⊆ ℎ ∧ 𝑡 ⊆ ∪ ℎ) → ({𝑡} × 𝑡) ⊆ (ℎ × ∪ ℎ)) |
84 | 81, 82, 83 | syl2anc 585 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ ℎ → ({𝑡} × 𝑡) ⊆ (ℎ × ∪ ℎ)) |
85 | | vsnex 5390 |
. . . . . . . . . . . . 13
⊢ {𝑡} ∈ V |
86 | 85, 56 | xpex 7691 |
. . . . . . . . . . . 12
⊢ ({𝑡} × 𝑡) ∈ V |
87 | 86 | elpw 4568 |
. . . . . . . . . . 11
⊢ (({𝑡} × 𝑡) ∈ 𝒫 (ℎ × ∪ ℎ) ↔ ({𝑡} × 𝑡) ⊆ (ℎ × ∪ ℎ)) |
88 | 84, 87 | sylibr 233 |
. . . . . . . . . 10
⊢ (𝑡 ∈ ℎ → ({𝑡} × 𝑡) ∈ 𝒫 (ℎ × ∪ ℎ)) |
89 | | eleq1 2822 |
. . . . . . . . . 10
⊢ (𝑢 = ({𝑡} × 𝑡) → (𝑢 ∈ 𝒫 (ℎ × ∪ ℎ) ↔ ({𝑡} × 𝑡) ∈ 𝒫 (ℎ × ∪ ℎ))) |
90 | 88, 89 | syl5ibrcom 247 |
. . . . . . . . 9
⊢ (𝑡 ∈ ℎ → (𝑢 = ({𝑡} × 𝑡) → 𝑢 ∈ 𝒫 (ℎ × ∪ ℎ))) |
91 | 90 | rexlimiv 3142 |
. . . . . . . 8
⊢
(∃𝑡 ∈
ℎ 𝑢 = ({𝑡} × 𝑡) → 𝑢 ∈ 𝒫 (ℎ × ∪ ℎ)) |
92 | 91 | adantl 483 |
. . . . . . 7
⊢ ((𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)) → 𝑢 ∈ 𝒫 (ℎ × ∪ ℎ)) |
93 | 92 | abssi 4031 |
. . . . . 6
⊢ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ⊆ 𝒫 (ℎ × ∪ ℎ) |
94 | 80, 93 | ssexi 5283 |
. . . . 5
⊢ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ∈ V |
95 | 8, 94 | eqeltri 2830 |
. . . 4
⊢ 𝐴 ∈ V |
96 | | raleq 3308 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ↔ ∀𝑧 ∈ 𝐴 𝑧 ≠ ∅)) |
97 | | raleq 3308 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) |
98 | 97 | raleqbi1dv 3306 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅) ↔ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅))) |
99 | 96, 98 | anbi12d 632 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) ↔ (∀𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)))) |
100 | | raleq 3308 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))) |
101 | 100 | exbidv 1925 |
. . . . 5
⊢ (𝑥 = 𝐴 → (∃𝑦∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦) ↔ ∃𝑦∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))) |
102 | 99, 101 | imbi12d 345 |
. . . 4
⊢ (𝑥 = 𝐴 → (((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) ↔ ((∀𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)))) |
103 | 95, 102 | spcv 3566 |
. . 3
⊢
(∀𝑥((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) → ((∀𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))) |
104 | 76, 103 | sylbi 216 |
. 2
⊢ (𝜑 → ((∀𝑧 ∈ 𝐴 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦))) |
105 | 10, 75, 104 | mp2ani 697 |
1
⊢ (𝜑 → ∃𝑦∀𝑧 ∈ 𝐴 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) |