Proof of Theorem dfac5lem3
Step | Hyp | Ref
| Expression |
1 | | snex 5324 |
. . . 4
⊢ {𝑤} ∈ V |
2 | | vex 3412 |
. . . 4
⊢ 𝑤 ∈ V |
3 | 1, 2 | xpex 7538 |
. . 3
⊢ ({𝑤} × 𝑤) ∈ V |
4 | | neeq1 3003 |
. . . 4
⊢ (𝑢 = ({𝑤} × 𝑤) → (𝑢 ≠ ∅ ↔ ({𝑤} × 𝑤) ≠ ∅)) |
5 | | eqeq1 2741 |
. . . . 5
⊢ (𝑢 = ({𝑤} × 𝑤) → (𝑢 = ({𝑡} × 𝑡) ↔ ({𝑤} × 𝑤) = ({𝑡} × 𝑡))) |
6 | 5 | rexbidv 3216 |
. . . 4
⊢ (𝑢 = ({𝑤} × 𝑤) → (∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡) ↔ ∃𝑡 ∈ ℎ ({𝑤} × 𝑤) = ({𝑡} × 𝑡))) |
7 | 4, 6 | anbi12d 634 |
. . 3
⊢ (𝑢 = ({𝑤} × 𝑤) → ((𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)) ↔ (({𝑤} × 𝑤) ≠ ∅ ∧ ∃𝑡 ∈ ℎ ({𝑤} × 𝑤) = ({𝑡} × 𝑡)))) |
8 | 3, 7 | elab 3587 |
. 2
⊢ (({𝑤} × 𝑤) ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ↔ (({𝑤} × 𝑤) ≠ ∅ ∧ ∃𝑡 ∈ ℎ ({𝑤} × 𝑤) = ({𝑡} × 𝑡))) |
9 | | dfac5lem.1 |
. . 3
⊢ 𝐴 = {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} |
10 | 9 | eleq2i 2829 |
. 2
⊢ (({𝑤} × 𝑤) ∈ 𝐴 ↔ ({𝑤} × 𝑤) ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))}) |
11 | | xpeq2 5572 |
. . . . . 6
⊢ (𝑤 = ∅ → ({𝑤} × 𝑤) = ({𝑤} × ∅)) |
12 | | xp0 6021 |
. . . . . 6
⊢ ({𝑤} × ∅) =
∅ |
13 | 11, 12 | eqtrdi 2794 |
. . . . 5
⊢ (𝑤 = ∅ → ({𝑤} × 𝑤) = ∅) |
14 | | rneq 5805 |
. . . . . 6
⊢ (({𝑤} × 𝑤) = ∅ → ran ({𝑤} × 𝑤) = ran ∅) |
15 | 2 | snnz 4692 |
. . . . . . 7
⊢ {𝑤} ≠ ∅ |
16 | | rnxp 6033 |
. . . . . . 7
⊢ ({𝑤} ≠ ∅ → ran
({𝑤} × 𝑤) = 𝑤) |
17 | 15, 16 | ax-mp 5 |
. . . . . 6
⊢ ran
({𝑤} × 𝑤) = 𝑤 |
18 | | rn0 5795 |
. . . . . 6
⊢ ran
∅ = ∅ |
19 | 14, 17, 18 | 3eqtr3g 2801 |
. . . . 5
⊢ (({𝑤} × 𝑤) = ∅ → 𝑤 = ∅) |
20 | 13, 19 | impbii 212 |
. . . 4
⊢ (𝑤 = ∅ ↔ ({𝑤} × 𝑤) = ∅) |
21 | 20 | necon3bii 2993 |
. . 3
⊢ (𝑤 ≠ ∅ ↔ ({𝑤} × 𝑤) ≠ ∅) |
22 | | df-rex 3067 |
. . . 4
⊢
(∃𝑡 ∈
ℎ ({𝑤} × 𝑤) = ({𝑡} × 𝑡) ↔ ∃𝑡(𝑡 ∈ ℎ ∧ ({𝑤} × 𝑤) = ({𝑡} × 𝑡))) |
23 | | rneq 5805 |
. . . . . . . . 9
⊢ (({𝑤} × 𝑤) = ({𝑡} × 𝑡) → ran ({𝑤} × 𝑤) = ran ({𝑡} × 𝑡)) |
24 | | vex 3412 |
. . . . . . . . . . 11
⊢ 𝑡 ∈ V |
25 | 24 | snnz 4692 |
. . . . . . . . . 10
⊢ {𝑡} ≠ ∅ |
26 | | rnxp 6033 |
. . . . . . . . . 10
⊢ ({𝑡} ≠ ∅ → ran
({𝑡} × 𝑡) = 𝑡) |
27 | 25, 26 | ax-mp 5 |
. . . . . . . . 9
⊢ ran
({𝑡} × 𝑡) = 𝑡 |
28 | 23, 17, 27 | 3eqtr3g 2801 |
. . . . . . . 8
⊢ (({𝑤} × 𝑤) = ({𝑡} × 𝑡) → 𝑤 = 𝑡) |
29 | | sneq 4551 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑡 → {𝑤} = {𝑡}) |
30 | 29 | xpeq1d 5580 |
. . . . . . . . 9
⊢ (𝑤 = 𝑡 → ({𝑤} × 𝑤) = ({𝑡} × 𝑤)) |
31 | | xpeq2 5572 |
. . . . . . . . 9
⊢ (𝑤 = 𝑡 → ({𝑡} × 𝑤) = ({𝑡} × 𝑡)) |
32 | 30, 31 | eqtrd 2777 |
. . . . . . . 8
⊢ (𝑤 = 𝑡 → ({𝑤} × 𝑤) = ({𝑡} × 𝑡)) |
33 | 28, 32 | impbii 212 |
. . . . . . 7
⊢ (({𝑤} × 𝑤) = ({𝑡} × 𝑡) ↔ 𝑤 = 𝑡) |
34 | | equcom 2026 |
. . . . . . 7
⊢ (𝑤 = 𝑡 ↔ 𝑡 = 𝑤) |
35 | 33, 34 | bitri 278 |
. . . . . 6
⊢ (({𝑤} × 𝑤) = ({𝑡} × 𝑡) ↔ 𝑡 = 𝑤) |
36 | 35 | anbi1ci 629 |
. . . . 5
⊢ ((𝑡 ∈ ℎ ∧ ({𝑤} × 𝑤) = ({𝑡} × 𝑡)) ↔ (𝑡 = 𝑤 ∧ 𝑡 ∈ ℎ)) |
37 | 36 | exbii 1855 |
. . . 4
⊢
(∃𝑡(𝑡 ∈ ℎ ∧ ({𝑤} × 𝑤) = ({𝑡} × 𝑡)) ↔ ∃𝑡(𝑡 = 𝑤 ∧ 𝑡 ∈ ℎ)) |
38 | | elequ1 2117 |
. . . . 5
⊢ (𝑡 = 𝑤 → (𝑡 ∈ ℎ ↔ 𝑤 ∈ ℎ)) |
39 | 38 | equsexvw 2013 |
. . . 4
⊢
(∃𝑡(𝑡 = 𝑤 ∧ 𝑡 ∈ ℎ) ↔ 𝑤 ∈ ℎ) |
40 | 22, 37, 39 | 3bitrri 301 |
. . 3
⊢ (𝑤 ∈ ℎ ↔ ∃𝑡 ∈ ℎ ({𝑤} × 𝑤) = ({𝑡} × 𝑡)) |
41 | 21, 40 | anbi12i 630 |
. 2
⊢ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ ℎ) ↔ (({𝑤} × 𝑤) ≠ ∅ ∧ ∃𝑡 ∈ ℎ ({𝑤} × 𝑤) = ({𝑡} × 𝑡))) |
42 | 8, 10, 41 | 3bitr4i 306 |
1
⊢ (({𝑤} × 𝑤) ∈ 𝐴 ↔ (𝑤 ≠ ∅ ∧ 𝑤 ∈ ℎ)) |