Proof of Theorem dfac5lem2
Step | Hyp | Ref
| Expression |
1 | | dfac5lem.1 |
. . . 4
⊢ 𝐴 = {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} |
2 | 1 | unieqi 4804 |
. . 3
⊢ ∪ 𝐴 =
∪ {𝑢 ∣ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} |
3 | 2 | eleq2i 2842 |
. 2
⊢
(〈𝑤, 𝑔〉 ∈ ∪ 𝐴
↔ 〈𝑤, 𝑔〉 ∈ ∪ {𝑢
∣ (𝑢 ≠ ∅
∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))}) |
4 | | eluniab 4806 |
. . 3
⊢
(〈𝑤, 𝑔〉 ∈ ∪ {𝑢
∣ (𝑢 ≠ ∅
∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ↔ ∃𝑢(〈𝑤, 𝑔〉 ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)))) |
5 | | r19.42v 3266 |
. . . . 5
⊢
(∃𝑡 ∈
ℎ ((〈𝑤, 𝑔〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ((〈𝑤, 𝑔〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))) |
6 | | anass 473 |
. . . . 5
⊢
(((〈𝑤, 𝑔〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)) ↔ (〈𝑤, 𝑔〉 ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡)))) |
7 | 5, 6 | bitr2i 279 |
. . . 4
⊢
((〈𝑤, 𝑔〉 ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑡 ∈ ℎ ((〈𝑤, 𝑔〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) |
8 | 7 | exbii 1850 |
. . 3
⊢
(∃𝑢(〈𝑤, 𝑔〉 ∈ 𝑢 ∧ (𝑢 ≠ ∅ ∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑢∃𝑡 ∈ ℎ ((〈𝑤, 𝑔〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) |
9 | | rexcom4 3175 |
. . . 4
⊢
(∃𝑡 ∈
ℎ ∃𝑢((〈𝑤, 𝑔〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑢∃𝑡 ∈ ℎ ((〈𝑤, 𝑔〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) |
10 | | df-rex 3074 |
. . . 4
⊢
(∃𝑡 ∈
ℎ ∃𝑢((〈𝑤, 𝑔〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((〈𝑤, 𝑔〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))) |
11 | 9, 10 | bitr3i 280 |
. . 3
⊢
(∃𝑢∃𝑡 ∈ ℎ ((〈𝑤, 𝑔〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((〈𝑤, 𝑔〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))) |
12 | 4, 8, 11 | 3bitri 301 |
. 2
⊢
(〈𝑤, 𝑔〉 ∈ ∪ {𝑢
∣ (𝑢 ≠ ∅
∧ ∃𝑡 ∈ ℎ 𝑢 = ({𝑡} × 𝑡))} ↔ ∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((〈𝑤, 𝑔〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)))) |
13 | | ancom 465 |
. . . . . . . . 9
⊢
(((〈𝑤, 𝑔〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ (〈𝑤, 𝑔〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅))) |
14 | | ne0i 4229 |
. . . . . . . . . . 11
⊢
(〈𝑤, 𝑔〉 ∈ 𝑢 → 𝑢 ≠ ∅) |
15 | 14 | pm4.71i 564 |
. . . . . . . . . 10
⊢
(〈𝑤, 𝑔〉 ∈ 𝑢 ↔ (〈𝑤, 𝑔〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅)) |
16 | 15 | anbi2i 626 |
. . . . . . . . 9
⊢ ((𝑢 = ({𝑡} × 𝑡) ∧ 〈𝑤, 𝑔〉 ∈ 𝑢) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ (〈𝑤, 𝑔〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅))) |
17 | 13, 16 | bitr4i 281 |
. . . . . . . 8
⊢
(((〈𝑤, 𝑔〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ (𝑢 = ({𝑡} × 𝑡) ∧ 〈𝑤, 𝑔〉 ∈ 𝑢)) |
18 | 17 | exbii 1850 |
. . . . . . 7
⊢
(∃𝑢((〈𝑤, 𝑔〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ ∃𝑢(𝑢 = ({𝑡} × 𝑡) ∧ 〈𝑤, 𝑔〉 ∈ 𝑢)) |
19 | | snex 5293 |
. . . . . . . . 9
⊢ {𝑡} ∈ V |
20 | | vex 3411 |
. . . . . . . . 9
⊢ 𝑡 ∈ V |
21 | 19, 20 | xpex 7467 |
. . . . . . . 8
⊢ ({𝑡} × 𝑡) ∈ V |
22 | | eleq2 2839 |
. . . . . . . 8
⊢ (𝑢 = ({𝑡} × 𝑡) → (〈𝑤, 𝑔〉 ∈ 𝑢 ↔ 〈𝑤, 𝑔〉 ∈ ({𝑡} × 𝑡))) |
23 | 21, 22 | ceqsexv 3457 |
. . . . . . 7
⊢
(∃𝑢(𝑢 = ({𝑡} × 𝑡) ∧ 〈𝑤, 𝑔〉 ∈ 𝑢) ↔ 〈𝑤, 𝑔〉 ∈ ({𝑡} × 𝑡)) |
24 | 18, 23 | bitri 278 |
. . . . . 6
⊢
(∃𝑢((〈𝑤, 𝑔〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡)) ↔ 〈𝑤, 𝑔〉 ∈ ({𝑡} × 𝑡)) |
25 | 24 | anbi2i 626 |
. . . . 5
⊢ ((𝑡 ∈ ℎ ∧ ∃𝑢((〈𝑤, 𝑔〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑡 ∈ ℎ ∧ 〈𝑤, 𝑔〉 ∈ ({𝑡} × 𝑡))) |
26 | | opelxp 5553 |
. . . . . . 7
⊢
(〈𝑤, 𝑔〉 ∈ ({𝑡} × 𝑡) ↔ (𝑤 ∈ {𝑡} ∧ 𝑔 ∈ 𝑡)) |
27 | | velsn 4531 |
. . . . . . . . 9
⊢ (𝑤 ∈ {𝑡} ↔ 𝑤 = 𝑡) |
28 | | equcom 2026 |
. . . . . . . . 9
⊢ (𝑤 = 𝑡 ↔ 𝑡 = 𝑤) |
29 | 27, 28 | bitri 278 |
. . . . . . . 8
⊢ (𝑤 ∈ {𝑡} ↔ 𝑡 = 𝑤) |
30 | 29 | anbi1i 627 |
. . . . . . 7
⊢ ((𝑤 ∈ {𝑡} ∧ 𝑔 ∈ 𝑡) ↔ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡)) |
31 | 26, 30 | bitri 278 |
. . . . . 6
⊢
(〈𝑤, 𝑔〉 ∈ ({𝑡} × 𝑡) ↔ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡)) |
32 | 31 | anbi2i 626 |
. . . . 5
⊢ ((𝑡 ∈ ℎ ∧ 〈𝑤, 𝑔〉 ∈ ({𝑡} × 𝑡)) ↔ (𝑡 ∈ ℎ ∧ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡))) |
33 | | an12 645 |
. . . . 5
⊢ ((𝑡 ∈ ℎ ∧ (𝑡 = 𝑤 ∧ 𝑔 ∈ 𝑡)) ↔ (𝑡 = 𝑤 ∧ (𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡))) |
34 | 25, 32, 33 | 3bitri 301 |
. . . 4
⊢ ((𝑡 ∈ ℎ ∧ ∃𝑢((〈𝑤, 𝑔〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑡 = 𝑤 ∧ (𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡))) |
35 | 34 | exbii 1850 |
. . 3
⊢
(∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((〈𝑤, 𝑔〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ ∃𝑡(𝑡 = 𝑤 ∧ (𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡))) |
36 | | vex 3411 |
. . . 4
⊢ 𝑤 ∈ V |
37 | | elequ1 2119 |
. . . . 5
⊢ (𝑡 = 𝑤 → (𝑡 ∈ ℎ ↔ 𝑤 ∈ ℎ)) |
38 | | eleq2 2839 |
. . . . 5
⊢ (𝑡 = 𝑤 → (𝑔 ∈ 𝑡 ↔ 𝑔 ∈ 𝑤)) |
39 | 37, 38 | anbi12d 634 |
. . . 4
⊢ (𝑡 = 𝑤 → ((𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡) ↔ (𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤))) |
40 | 36, 39 | ceqsexv 3457 |
. . 3
⊢
(∃𝑡(𝑡 = 𝑤 ∧ (𝑡 ∈ ℎ ∧ 𝑔 ∈ 𝑡)) ↔ (𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤)) |
41 | 35, 40 | bitri 278 |
. 2
⊢
(∃𝑡(𝑡 ∈ ℎ ∧ ∃𝑢((〈𝑤, 𝑔〉 ∈ 𝑢 ∧ 𝑢 ≠ ∅) ∧ 𝑢 = ({𝑡} × 𝑡))) ↔ (𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤)) |
42 | 3, 12, 41 | 3bitri 301 |
1
⊢
(〈𝑤, 𝑔〉 ∈ ∪ 𝐴
↔ (𝑤 ∈ ℎ ∧ 𝑔 ∈ 𝑤)) |