Step | Hyp | Ref
| Expression |
1 | | 1oex 8238 |
. . . . . . 7
⊢
1o ∈ V |
2 | 1 | ensn1 8719 |
. . . . . 6
⊢
{1o} ≈ 1o |
3 | 2 | ensymi 8703 |
. . . . 5
⊢
1o ≈ {1o} |
4 | | entr 8705 |
. . . . 5
⊢ ((𝐵 ≈ 1o ∧
1o ≈ {1o}) → 𝐵 ≈ {1o}) |
5 | 3, 4 | mpan2 691 |
. . . 4
⊢ (𝐵 ≈ 1o →
𝐵 ≈
{1o}) |
6 | | 1on 8232 |
. . . . . . . 8
⊢
1o ∈ On |
7 | 6 | onirri 6340 |
. . . . . . 7
⊢ ¬
1o ∈ 1o |
8 | | disjsn 4643 |
. . . . . . 7
⊢
((1o ∩ {1o}) = ∅ ↔ ¬
1o ∈ 1o) |
9 | 7, 8 | mpbir 234 |
. . . . . 6
⊢
(1o ∩ {1o}) = ∅ |
10 | | unen 8748 |
. . . . . 6
⊢ (((𝐴 ≈ 1o ∧
𝐵 ≈ {1o})
∧ ((𝐴 ∩ 𝐵) = ∅ ∧ (1o
∩ {1o}) = ∅)) → (𝐴 ∪ 𝐵) ≈ (1o ∪
{1o})) |
11 | 9, 10 | mpanr2 704 |
. . . . 5
⊢ (((𝐴 ≈ 1o ∧
𝐵 ≈ {1o})
∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∪ 𝐵) ≈ (1o ∪
{1o})) |
12 | 11 | ex 416 |
. . . 4
⊢ ((𝐴 ≈ 1o ∧
𝐵 ≈ {1o})
→ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ∪ 𝐵) ≈ (1o ∪
{1o}))) |
13 | 5, 12 | sylan2 596 |
. . 3
⊢ ((𝐴 ≈ 1o ∧
𝐵 ≈ 1o)
→ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ∪ 𝐵) ≈ (1o ∪
{1o}))) |
14 | | df-2o 8226 |
. . . . 5
⊢
2o = suc 1o |
15 | | df-suc 6239 |
. . . . 5
⊢ suc
1o = (1o ∪ {1o}) |
16 | 14, 15 | eqtri 2767 |
. . . 4
⊢
2o = (1o ∪ {1o}) |
17 | 16 | breq2i 5077 |
. . 3
⊢ ((𝐴 ∪ 𝐵) ≈ 2o ↔ (𝐴 ∪ 𝐵) ≈ (1o ∪
{1o})) |
18 | 13, 17 | syl6ibr 255 |
. 2
⊢ ((𝐴 ≈ 1o ∧
𝐵 ≈ 1o)
→ ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ∪ 𝐵) ≈ 2o)) |
19 | | en1 8723 |
. . 3
⊢ (𝐴 ≈ 1o ↔
∃𝑥 𝐴 = {𝑥}) |
20 | | en1 8723 |
. . 3
⊢ (𝐵 ≈ 1o ↔
∃𝑦 𝐵 = {𝑦}) |
21 | | sneq 4567 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦}) |
22 | 21 | uneq2d 4093 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ({𝑥} ∪ {𝑥}) = ({𝑥} ∪ {𝑦})) |
23 | | unidm 4082 |
. . . . . . . . . . . . . 14
⊢ ({𝑥} ∪ {𝑥}) = {𝑥} |
24 | 22, 23 | eqtr3di 2795 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → ({𝑥} ∪ {𝑦}) = {𝑥}) |
25 | | vex 3426 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
26 | 25 | ensn1 8719 |
. . . . . . . . . . . . . 14
⊢ {𝑥} ≈
1o |
27 | | 1sdom2 8904 |
. . . . . . . . . . . . . 14
⊢
1o ≺ 2o |
28 | | ensdomtr 8807 |
. . . . . . . . . . . . . 14
⊢ (({𝑥} ≈ 1o ∧
1o ≺ 2o) → {𝑥} ≺ 2o) |
29 | 26, 27, 28 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ {𝑥} ≺
2o |
30 | 24, 29 | eqbrtrdi 5108 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ({𝑥} ∪ {𝑦}) ≺ 2o) |
31 | | sdomnen 8682 |
. . . . . . . . . . . 12
⊢ (({𝑥} ∪ {𝑦}) ≺ 2o → ¬ ({𝑥} ∪ {𝑦}) ≈ 2o) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ¬ ({𝑥} ∪ {𝑦}) ≈ 2o) |
33 | 32 | necon2ai 2972 |
. . . . . . . . . 10
⊢ (({𝑥} ∪ {𝑦}) ≈ 2o → 𝑥 ≠ 𝑦) |
34 | | disjsn2 4644 |
. . . . . . . . . 10
⊢ (𝑥 ≠ 𝑦 → ({𝑥} ∩ {𝑦}) = ∅) |
35 | 33, 34 | syl 17 |
. . . . . . . . 9
⊢ (({𝑥} ∪ {𝑦}) ≈ 2o → ({𝑥} ∩ {𝑦}) = ∅) |
36 | 35 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → (({𝑥} ∪ {𝑦}) ≈ 2o → ({𝑥} ∩ {𝑦}) = ∅)) |
37 | | uneq12 4088 |
. . . . . . . . 9
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → (𝐴 ∪ 𝐵) = ({𝑥} ∪ {𝑦})) |
38 | 37 | breq1d 5079 |
. . . . . . . 8
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → ((𝐴 ∪ 𝐵) ≈ 2o ↔ ({𝑥} ∪ {𝑦}) ≈ 2o)) |
39 | | ineq12 4138 |
. . . . . . . . 9
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → (𝐴 ∩ 𝐵) = ({𝑥} ∩ {𝑦})) |
40 | 39 | eqeq1d 2741 |
. . . . . . . 8
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → ((𝐴 ∩ 𝐵) = ∅ ↔ ({𝑥} ∩ {𝑦}) = ∅)) |
41 | 36, 38, 40 | 3imtr4d 297 |
. . . . . . 7
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → ((𝐴 ∪ 𝐵) ≈ 2o → (𝐴 ∩ 𝐵) = ∅)) |
42 | 41 | ex 416 |
. . . . . 6
⊢ (𝐴 = {𝑥} → (𝐵 = {𝑦} → ((𝐴 ∪ 𝐵) ≈ 2o → (𝐴 ∩ 𝐵) = ∅))) |
43 | 42 | exlimdv 1941 |
. . . . 5
⊢ (𝐴 = {𝑥} → (∃𝑦 𝐵 = {𝑦} → ((𝐴 ∪ 𝐵) ≈ 2o → (𝐴 ∩ 𝐵) = ∅))) |
44 | 43 | exlimiv 1938 |
. . . 4
⊢
(∃𝑥 𝐴 = {𝑥} → (∃𝑦 𝐵 = {𝑦} → ((𝐴 ∪ 𝐵) ≈ 2o → (𝐴 ∩ 𝐵) = ∅))) |
45 | 44 | imp 410 |
. . 3
⊢
((∃𝑥 𝐴 = {𝑥} ∧ ∃𝑦 𝐵 = {𝑦}) → ((𝐴 ∪ 𝐵) ≈ 2o → (𝐴 ∩ 𝐵) = ∅)) |
46 | 19, 20, 45 | syl2anb 601 |
. 2
⊢ ((𝐴 ≈ 1o ∧
𝐵 ≈ 1o)
→ ((𝐴 ∪ 𝐵) ≈ 2o →
(𝐴 ∩ 𝐵) = ∅)) |
47 | 18, 46 | impbid 215 |
1
⊢ ((𝐴 ≈ 1o ∧
𝐵 ≈ 1o)
→ ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐴 ∪ 𝐵) ≈ 2o)) |