Step | Hyp | Ref
| Expression |
1 | | 1on 7567 |
. . . . . . . 8
⊢
1𝑜 ∈ On |
2 | 1 | elexi 3213 |
. . . . . . 7
⊢
1𝑜 ∈ V |
3 | 2 | ensn1 8020 |
. . . . . 6
⊢
{1𝑜} ≈ 1𝑜 |
4 | 3 | ensymi 8006 |
. . . . 5
⊢
1𝑜 ≈ {1𝑜} |
5 | | entr 8008 |
. . . . 5
⊢ ((𝐵 ≈ 1𝑜
∧ 1𝑜 ≈ {1𝑜}) → 𝐵 ≈
{1𝑜}) |
6 | 4, 5 | mpan2 707 |
. . . 4
⊢ (𝐵 ≈ 1𝑜
→ 𝐵 ≈
{1𝑜}) |
7 | 1 | onirri 5834 |
. . . . . . 7
⊢ ¬
1𝑜 ∈ 1𝑜 |
8 | | disjsn 4246 |
. . . . . . 7
⊢
((1𝑜 ∩ {1𝑜}) = ∅ ↔
¬ 1𝑜 ∈ 1𝑜) |
9 | 7, 8 | mpbir 221 |
. . . . . 6
⊢
(1𝑜 ∩ {1𝑜}) =
∅ |
10 | | unen 8040 |
. . . . . 6
⊢ (((𝐴 ≈ 1𝑜
∧ 𝐵 ≈
{1𝑜}) ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ (1𝑜
∩ {1𝑜}) = ∅)) → (𝐴 ∪ 𝐵) ≈ (1𝑜 ∪
{1𝑜})) |
11 | 9, 10 | mpanr2 720 |
. . . . 5
⊢ (((𝐴 ≈ 1𝑜
∧ 𝐵 ≈
{1𝑜}) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∪ 𝐵) ≈ (1𝑜 ∪
{1𝑜})) |
12 | 11 | ex 450 |
. . . 4
⊢ ((𝐴 ≈ 1𝑜
∧ 𝐵 ≈
{1𝑜}) → ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ∪ 𝐵) ≈ (1𝑜 ∪
{1𝑜}))) |
13 | 6, 12 | sylan2 491 |
. . 3
⊢ ((𝐴 ≈ 1𝑜
∧ 𝐵 ≈
1𝑜) → ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ∪ 𝐵) ≈ (1𝑜 ∪
{1𝑜}))) |
14 | | df-2o 7561 |
. . . . 5
⊢
2𝑜 = suc 1𝑜 |
15 | | df-suc 5729 |
. . . . 5
⊢ suc
1𝑜 = (1𝑜 ∪
{1𝑜}) |
16 | 14, 15 | eqtri 2644 |
. . . 4
⊢
2𝑜 = (1𝑜 ∪
{1𝑜}) |
17 | 16 | breq2i 4661 |
. . 3
⊢ ((𝐴 ∪ 𝐵) ≈ 2𝑜 ↔
(𝐴 ∪ 𝐵) ≈ (1𝑜 ∪
{1𝑜})) |
18 | 13, 17 | syl6ibr 242 |
. 2
⊢ ((𝐴 ≈ 1𝑜
∧ 𝐵 ≈
1𝑜) → ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ∪ 𝐵) ≈
2𝑜)) |
19 | | en1 8023 |
. . 3
⊢ (𝐴 ≈ 1𝑜
↔ ∃𝑥 𝐴 = {𝑥}) |
20 | | en1 8023 |
. . 3
⊢ (𝐵 ≈ 1𝑜
↔ ∃𝑦 𝐵 = {𝑦}) |
21 | | unidm 3756 |
. . . . . . . . . . . . . 14
⊢ ({𝑥} ∪ {𝑥}) = {𝑥} |
22 | | sneq 4187 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦}) |
23 | 22 | uneq2d 3767 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ({𝑥} ∪ {𝑥}) = ({𝑥} ∪ {𝑦})) |
24 | 21, 23 | syl5reqr 2671 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → ({𝑥} ∪ {𝑦}) = {𝑥}) |
25 | | vex 3203 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
26 | 25 | ensn1 8020 |
. . . . . . . . . . . . . 14
⊢ {𝑥} ≈
1𝑜 |
27 | | 1sdom2 8159 |
. . . . . . . . . . . . . 14
⊢
1𝑜 ≺ 2𝑜 |
28 | | ensdomtr 8096 |
. . . . . . . . . . . . . 14
⊢ (({𝑥} ≈ 1𝑜
∧ 1𝑜 ≺ 2𝑜) → {𝑥} ≺
2𝑜) |
29 | 26, 27, 28 | mp2an 708 |
. . . . . . . . . . . . 13
⊢ {𝑥} ≺
2𝑜 |
30 | 24, 29 | syl6eqbr 4692 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ({𝑥} ∪ {𝑦}) ≺
2𝑜) |
31 | | sdomnen 7984 |
. . . . . . . . . . . 12
⊢ (({𝑥} ∪ {𝑦}) ≺ 2𝑜 → ¬
({𝑥} ∪ {𝑦}) ≈
2𝑜) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ¬ ({𝑥} ∪ {𝑦}) ≈
2𝑜) |
33 | 32 | necon2ai 2823 |
. . . . . . . . . 10
⊢ (({𝑥} ∪ {𝑦}) ≈ 2𝑜 → 𝑥 ≠ 𝑦) |
34 | | disjsn2 4247 |
. . . . . . . . . 10
⊢ (𝑥 ≠ 𝑦 → ({𝑥} ∩ {𝑦}) = ∅) |
35 | 33, 34 | syl 17 |
. . . . . . . . 9
⊢ (({𝑥} ∪ {𝑦}) ≈ 2𝑜 →
({𝑥} ∩ {𝑦}) = ∅) |
36 | 35 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → (({𝑥} ∪ {𝑦}) ≈ 2𝑜 →
({𝑥} ∩ {𝑦}) = ∅)) |
37 | | uneq12 3762 |
. . . . . . . . 9
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → (𝐴 ∪ 𝐵) = ({𝑥} ∪ {𝑦})) |
38 | 37 | breq1d 4663 |
. . . . . . . 8
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → ((𝐴 ∪ 𝐵) ≈ 2𝑜 ↔
({𝑥} ∪ {𝑦}) ≈
2𝑜)) |
39 | | ineq12 3809 |
. . . . . . . . 9
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → (𝐴 ∩ 𝐵) = ({𝑥} ∩ {𝑦})) |
40 | 39 | eqeq1d 2624 |
. . . . . . . 8
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → ((𝐴 ∩ 𝐵) = ∅ ↔ ({𝑥} ∩ {𝑦}) = ∅)) |
41 | 36, 38, 40 | 3imtr4d 283 |
. . . . . . 7
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → ((𝐴 ∪ 𝐵) ≈ 2𝑜 →
(𝐴 ∩ 𝐵) = ∅)) |
42 | 41 | ex 450 |
. . . . . 6
⊢ (𝐴 = {𝑥} → (𝐵 = {𝑦} → ((𝐴 ∪ 𝐵) ≈ 2𝑜 →
(𝐴 ∩ 𝐵) = ∅))) |
43 | 42 | exlimdv 1861 |
. . . . 5
⊢ (𝐴 = {𝑥} → (∃𝑦 𝐵 = {𝑦} → ((𝐴 ∪ 𝐵) ≈ 2𝑜 →
(𝐴 ∩ 𝐵) = ∅))) |
44 | 43 | exlimiv 1858 |
. . . 4
⊢
(∃𝑥 𝐴 = {𝑥} → (∃𝑦 𝐵 = {𝑦} → ((𝐴 ∪ 𝐵) ≈ 2𝑜 →
(𝐴 ∩ 𝐵) = ∅))) |
45 | 44 | imp 445 |
. . 3
⊢
((∃𝑥 𝐴 = {𝑥} ∧ ∃𝑦 𝐵 = {𝑦}) → ((𝐴 ∪ 𝐵) ≈ 2𝑜 →
(𝐴 ∩ 𝐵) = ∅)) |
46 | 19, 20, 45 | syl2anb 496 |
. 2
⊢ ((𝐴 ≈ 1𝑜
∧ 𝐵 ≈
1𝑜) → ((𝐴 ∪ 𝐵) ≈ 2𝑜 →
(𝐴 ∩ 𝐵) = ∅)) |
47 | 18, 46 | impbid 202 |
1
⊢ ((𝐴 ≈ 1𝑜
∧ 𝐵 ≈
1𝑜) → ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐴 ∪ 𝐵) ≈
2𝑜)) |