Step | Hyp | Ref
| Expression |
1 | | 1on 6031 |
. . . . . . . 8
⊢
1𝑜 ∈ On |
2 | 1 | elexi 2611 |
. . . . . . 7
⊢
1𝑜 ∈ V |
3 | 2 | ensn1 6299 |
. . . . . 6
⊢
{1𝑜} ≈ 1𝑜 |
4 | 3 | ensymi 6285 |
. . . . 5
⊢
1𝑜 ≈ {1𝑜} |
5 | | entr 6287 |
. . . . 5
⊢ ((𝐵 ≈ 1𝑜
∧ 1𝑜 ≈ {1𝑜}) → 𝐵 ≈
{1𝑜}) |
6 | 4, 5 | mpan2 415 |
. . . 4
⊢ (𝐵 ≈ 1𝑜
→ 𝐵 ≈
{1𝑜}) |
7 | 1 | onirri 4286 |
. . . . . . 7
⊢ ¬
1𝑜 ∈ 1𝑜 |
8 | | disjsn 3454 |
. . . . . . 7
⊢
((1𝑜 ∩ {1𝑜}) = ∅ ↔
¬ 1𝑜 ∈ 1𝑜) |
9 | 7, 8 | mpbir 144 |
. . . . . 6
⊢
(1𝑜 ∩ {1𝑜}) =
∅ |
10 | | unen 6316 |
. . . . . 6
⊢ (((𝐴 ≈ 1𝑜
∧ 𝐵 ≈
{1𝑜}) ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ (1𝑜
∩ {1𝑜}) = ∅)) → (𝐴 ∪ 𝐵) ≈ (1𝑜 ∪
{1𝑜})) |
11 | 9, 10 | mpanr2 428 |
. . . . 5
⊢ (((𝐴 ≈ 1𝑜
∧ 𝐵 ≈
{1𝑜}) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐴 ∪ 𝐵) ≈ (1𝑜 ∪
{1𝑜})) |
12 | 11 | ex 113 |
. . . 4
⊢ ((𝐴 ≈ 1𝑜
∧ 𝐵 ≈
{1𝑜}) → ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ∪ 𝐵) ≈ (1𝑜 ∪
{1𝑜}))) |
13 | 6, 12 | sylan2 280 |
. . 3
⊢ ((𝐴 ≈ 1𝑜
∧ 𝐵 ≈
1𝑜) → ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ∪ 𝐵) ≈ (1𝑜 ∪
{1𝑜}))) |
14 | | df-2o 6025 |
. . . . 5
⊢
2𝑜 = suc 1𝑜 |
15 | | df-suc 4126 |
. . . . 5
⊢ suc
1𝑜 = (1𝑜 ∪
{1𝑜}) |
16 | 14, 15 | eqtri 2101 |
. . . 4
⊢
2𝑜 = (1𝑜 ∪
{1𝑜}) |
17 | 16 | breq2i 3793 |
. . 3
⊢ ((𝐴 ∪ 𝐵) ≈ 2𝑜 ↔
(𝐴 ∪ 𝐵) ≈ (1𝑜 ∪
{1𝑜})) |
18 | 13, 17 | syl6ibr 160 |
. 2
⊢ ((𝐴 ≈ 1𝑜
∧ 𝐵 ≈
1𝑜) → ((𝐴 ∩ 𝐵) = ∅ → (𝐴 ∪ 𝐵) ≈
2𝑜)) |
19 | | en1 6302 |
. . 3
⊢ (𝐴 ≈ 1𝑜
↔ ∃𝑥 𝐴 = {𝑥}) |
20 | | en1 6302 |
. . 3
⊢ (𝐵 ≈ 1𝑜
↔ ∃𝑦 𝐵 = {𝑦}) |
21 | | 1nen2 6347 |
. . . . . . . . . . . . 13
⊢ ¬
1𝑜 ≈ 2𝑜 |
22 | 21 | a1i 9 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ¬ 1𝑜 ≈
2𝑜) |
23 | | unidm 3115 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑥} ∪ {𝑥}) = {𝑥} |
24 | | sneq 3409 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦}) |
25 | 24 | uneq2d 3126 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → ({𝑥} ∪ {𝑥}) = ({𝑥} ∪ {𝑦})) |
26 | 23, 25 | syl5reqr 2128 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → ({𝑥} ∪ {𝑦}) = {𝑥}) |
27 | | vex 2604 |
. . . . . . . . . . . . . . . 16
⊢ 𝑥 ∈ V |
28 | 27 | ensn1 6299 |
. . . . . . . . . . . . . . 15
⊢ {𝑥} ≈
1𝑜 |
29 | 26, 28 | syl6eqbr 3822 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ({𝑥} ∪ {𝑦}) ≈
1𝑜) |
30 | 29 | ensymd 6286 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → 1𝑜 ≈ ({𝑥} ∪ {𝑦})) |
31 | | entr 6287 |
. . . . . . . . . . . . 13
⊢
((1𝑜 ≈ ({𝑥} ∪ {𝑦}) ∧ ({𝑥} ∪ {𝑦}) ≈ 2𝑜) →
1𝑜 ≈ 2𝑜) |
32 | 30, 31 | sylan 277 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑦 ∧ ({𝑥} ∪ {𝑦}) ≈ 2𝑜) →
1𝑜 ≈ 2𝑜) |
33 | 22, 32 | mtand 623 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ¬ ({𝑥} ∪ {𝑦}) ≈
2𝑜) |
34 | 33 | necon2ai 2299 |
. . . . . . . . . 10
⊢ (({𝑥} ∪ {𝑦}) ≈ 2𝑜 → 𝑥 ≠ 𝑦) |
35 | | disjsn2 3455 |
. . . . . . . . . 10
⊢ (𝑥 ≠ 𝑦 → ({𝑥} ∩ {𝑦}) = ∅) |
36 | 34, 35 | syl 14 |
. . . . . . . . 9
⊢ (({𝑥} ∪ {𝑦}) ≈ 2𝑜 →
({𝑥} ∩ {𝑦}) = ∅) |
37 | 36 | a1i 9 |
. . . . . . . 8
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → (({𝑥} ∪ {𝑦}) ≈ 2𝑜 →
({𝑥} ∩ {𝑦}) = ∅)) |
38 | | uneq12 3121 |
. . . . . . . . 9
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → (𝐴 ∪ 𝐵) = ({𝑥} ∪ {𝑦})) |
39 | 38 | breq1d 3795 |
. . . . . . . 8
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → ((𝐴 ∪ 𝐵) ≈ 2𝑜 ↔
({𝑥} ∪ {𝑦}) ≈
2𝑜)) |
40 | | ineq12 3162 |
. . . . . . . . 9
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → (𝐴 ∩ 𝐵) = ({𝑥} ∩ {𝑦})) |
41 | 40 | eqeq1d 2089 |
. . . . . . . 8
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → ((𝐴 ∩ 𝐵) = ∅ ↔ ({𝑥} ∩ {𝑦}) = ∅)) |
42 | 37, 39, 41 | 3imtr4d 201 |
. . . . . . 7
⊢ ((𝐴 = {𝑥} ∧ 𝐵 = {𝑦}) → ((𝐴 ∪ 𝐵) ≈ 2𝑜 →
(𝐴 ∩ 𝐵) = ∅)) |
43 | 42 | ex 113 |
. . . . . 6
⊢ (𝐴 = {𝑥} → (𝐵 = {𝑦} → ((𝐴 ∪ 𝐵) ≈ 2𝑜 →
(𝐴 ∩ 𝐵) = ∅))) |
44 | 43 | exlimdv 1740 |
. . . . 5
⊢ (𝐴 = {𝑥} → (∃𝑦 𝐵 = {𝑦} → ((𝐴 ∪ 𝐵) ≈ 2𝑜 →
(𝐴 ∩ 𝐵) = ∅))) |
45 | 44 | exlimiv 1529 |
. . . 4
⊢
(∃𝑥 𝐴 = {𝑥} → (∃𝑦 𝐵 = {𝑦} → ((𝐴 ∪ 𝐵) ≈ 2𝑜 →
(𝐴 ∩ 𝐵) = ∅))) |
46 | 45 | imp 122 |
. . 3
⊢
((∃𝑥 𝐴 = {𝑥} ∧ ∃𝑦 𝐵 = {𝑦}) → ((𝐴 ∪ 𝐵) ≈ 2𝑜 →
(𝐴 ∩ 𝐵) = ∅)) |
47 | 19, 20, 46 | syl2anb 285 |
. 2
⊢ ((𝐴 ≈ 1𝑜
∧ 𝐵 ≈
1𝑜) → ((𝐴 ∪ 𝐵) ≈ 2𝑜 →
(𝐴 ∩ 𝐵) = ∅)) |
48 | 18, 47 | impbid 127 |
1
⊢ ((𝐴 ≈ 1𝑜
∧ 𝐵 ≈
1𝑜) → ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐴 ∪ 𝐵) ≈
2𝑜)) |