Proof of Theorem dfac5lem3
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | vsnex 5433 | . . . 4
⊢ {𝑤} ∈ V | 
| 2 |  | vex 3483 | . . . 4
⊢ 𝑤 ∈ V | 
| 3 | 1, 2 | xpex 7774 | . . 3
⊢ ({𝑤} × 𝑤) ∈ V | 
| 4 |  | neeq1 3002 | . . . 4
⊢ (𝑢 = ({𝑤} × 𝑤) → (𝑢 ≠ ∅ ↔ ({𝑤} × 𝑤) ≠ ∅)) | 
| 5 |  | eqeq1 2740 | . . . . 5
⊢ (𝑢 = ({𝑤} × 𝑤) → (𝑢 = ({𝑡} × 𝑡) ↔ ({𝑤} × 𝑤) = ({𝑡} × 𝑡))) | 
| 6 | 5 | rexbidv 3178 | . . . 4
⊢ (𝑢 = ({𝑤} × 𝑤) → (∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡) ↔ ∃𝑡 ∈ ℎ ({𝑤} × 𝑤) = ({𝑡} × 𝑡))) | 
| 7 | 4, 6 | anbi12d 632 | . . 3
⊢ (𝑢 = ({𝑤} × 𝑤) → ((𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)) ↔ (({𝑤} × 𝑤) ≠ ∅ ∧ ∃𝑡 ∈ ℎ ({𝑤} × 𝑤) = ({𝑡} × 𝑡)))) | 
| 8 | 3, 7 | elab 3678 | . 2
⊢ (({𝑤} × 𝑤) ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ↔ (({𝑤} × 𝑤) ≠ ∅ ∧ ∃𝑡 ∈ ℎ ({𝑤} × 𝑤) = ({𝑡} × 𝑡))) | 
| 9 |  | dfac5lem.1 | . . 3
⊢ 𝐴 = {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} | 
| 10 | 9 | eleq2i 2832 | . 2
⊢ (({𝑤} × 𝑤) ∈ 𝐴 ↔ ({𝑤} × 𝑤) ∈ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))}) | 
| 11 |  | xpeq2 5705 | . . . . . 6
⊢ (𝑤 = ∅ → ({𝑤} × 𝑤) = ({𝑤} × ∅)) | 
| 12 |  | xp0 6177 | . . . . . 6
⊢ ({𝑤} × ∅) =
∅ | 
| 13 | 11, 12 | eqtrdi 2792 | . . . . 5
⊢ (𝑤 = ∅ → ({𝑤} × 𝑤) = ∅) | 
| 14 |  | rneq 5946 | . . . . . 6
⊢ (({𝑤} × 𝑤) = ∅ → ran ({𝑤} × 𝑤) = ran ∅) | 
| 15 | 2 | snnz 4775 | . . . . . . 7
⊢ {𝑤} ≠ ∅ | 
| 16 |  | rnxp 6189 | . . . . . . 7
⊢ ({𝑤} ≠ ∅ → ran
({𝑤} × 𝑤) = 𝑤) | 
| 17 | 15, 16 | ax-mp 5 | . . . . . 6
⊢ ran
({𝑤} × 𝑤) = 𝑤 | 
| 18 |  | rn0 5935 | . . . . . 6
⊢ ran
∅ = ∅ | 
| 19 | 14, 17, 18 | 3eqtr3g 2799 | . . . . 5
⊢ (({𝑤} × 𝑤) = ∅ → 𝑤 = ∅) | 
| 20 | 13, 19 | impbii 209 | . . . 4
⊢ (𝑤 = ∅ ↔ ({𝑤} × 𝑤) = ∅) | 
| 21 | 20 | necon3bii 2992 | . . 3
⊢ (𝑤 ≠ ∅ ↔ ({𝑤} × 𝑤) ≠ ∅) | 
| 22 |  | df-rex 3070 | . . . 4
⊢
(∃𝑡 ∈
ℎ ({𝑤} × 𝑤) = ({𝑡} × 𝑡) ↔ ∃𝑡(𝑡 ∈ ℎ ∧ ({𝑤} × 𝑤) = ({𝑡} × 𝑡))) | 
| 23 |  | rneq 5946 | . . . . . . . . 9
⊢ (({𝑤} × 𝑤) = ({𝑡} × 𝑡) → ran ({𝑤} × 𝑤) = ran ({𝑡} × 𝑡)) | 
| 24 |  | vex 3483 | . . . . . . . . . . 11
⊢ 𝑡 ∈ V | 
| 25 | 24 | snnz 4775 | . . . . . . . . . 10
⊢ {𝑡} ≠ ∅ | 
| 26 |  | rnxp 6189 | . . . . . . . . . 10
⊢ ({𝑡} ≠ ∅ → ran
({𝑡} × 𝑡) = 𝑡) | 
| 27 | 25, 26 | ax-mp 5 | . . . . . . . . 9
⊢ ran
({𝑡} × 𝑡) = 𝑡 | 
| 28 | 23, 17, 27 | 3eqtr3g 2799 | . . . . . . . 8
⊢ (({𝑤} × 𝑤) = ({𝑡} × 𝑡) → 𝑤 = 𝑡) | 
| 29 |  | sneq 4635 | . . . . . . . . . 10
⊢ (𝑤 = 𝑡 → {𝑤} = {𝑡}) | 
| 30 | 29 | xpeq1d 5713 | . . . . . . . . 9
⊢ (𝑤 = 𝑡 → ({𝑤} × 𝑤) = ({𝑡} × 𝑤)) | 
| 31 |  | xpeq2 5705 | . . . . . . . . 9
⊢ (𝑤 = 𝑡 → ({𝑡} × 𝑤) = ({𝑡} × 𝑡)) | 
| 32 | 30, 31 | eqtrd 2776 | . . . . . . . 8
⊢ (𝑤 = 𝑡 → ({𝑤} × 𝑤) = ({𝑡} × 𝑡)) | 
| 33 | 28, 32 | impbii 209 | . . . . . . 7
⊢ (({𝑤} × 𝑤) = ({𝑡} × 𝑡) ↔ 𝑤 = 𝑡) | 
| 34 |  | equcom 2016 | . . . . . . 7
⊢ (𝑤 = 𝑡 ↔ 𝑡 = 𝑤) | 
| 35 | 33, 34 | bitri 275 | . . . . . 6
⊢ (({𝑤} × 𝑤) = ({𝑡} × 𝑡) ↔ 𝑡 = 𝑤) | 
| 36 | 35 | anbi1ci 626 | . . . . 5
⊢ ((𝑡 ∈ ℎ ∧ ({𝑤} × 𝑤) = ({𝑡} × 𝑡)) ↔ (𝑡 = 𝑤 ∧ 𝑡 ∈ ℎ)) | 
| 37 | 36 | exbii 1847 | . . . 4
⊢
(∃𝑡(𝑡 ∈ ℎ ∧ ({𝑤} × 𝑤) = ({𝑡} × 𝑡)) ↔ ∃𝑡(𝑡 = 𝑤 ∧ 𝑡 ∈ ℎ)) | 
| 38 |  | elequ1 2114 | . . . . 5
⊢ (𝑡 = 𝑤 → (𝑡 ∈ ℎ ↔ 𝑤 ∈ ℎ)) | 
| 39 | 38 | equsexvw 2003 | . . . 4
⊢
(∃𝑡(𝑡 = 𝑤 ∧ 𝑡 ∈ ℎ) ↔ 𝑤 ∈ ℎ) | 
| 40 | 22, 37, 39 | 3bitrri 298 | . . 3
⊢ (𝑤 ∈ ℎ ↔ ∃𝑡 ∈ ℎ ({𝑤} × 𝑤) = ({𝑡} × 𝑡)) | 
| 41 | 21, 40 | anbi12i 628 | . 2
⊢ ((𝑤 ≠ ∅ ∧ 𝑤 ∈ ℎ) ↔ (({𝑤} × 𝑤) ≠ ∅ ∧ ∃𝑡 ∈ ℎ ({𝑤} × 𝑤) = ({𝑡} × 𝑡))) | 
| 42 | 8, 10, 41 | 3bitr4i 303 | 1
⊢ (({𝑤} × 𝑤) ∈ 𝐴 ↔ (𝑤 ≠ ∅ ∧ 𝑤 ∈ ℎ)) |