Step | Hyp | Ref
| Expression |
1 | | 1sdom2 8159 |
. . . 4
⊢
1𝑜 ≺ 2𝑜 |
2 | | sdomdom 7983 |
. . . 4
⊢
(1𝑜 ≺ 2𝑜 →
1𝑜 ≼ 2𝑜) |
3 | | cdadom2 9009 |
. . . 4
⊢
(1𝑜 ≼ 2𝑜 → (𝐴 +𝑐
1𝑜) ≼ (𝐴 +𝑐
2𝑜)) |
4 | 1, 2, 3 | mp2b 10 |
. . 3
⊢ (𝐴 +𝑐
1𝑜) ≼ (𝐴 +𝑐
2𝑜) |
5 | | canthp1lem1 9474 |
. . 3
⊢
(1𝑜 ≺ 𝐴 → (𝐴 +𝑐
2𝑜) ≼ 𝒫 𝐴) |
6 | | domtr 8009 |
. . 3
⊢ (((𝐴 +𝑐
1𝑜) ≼ (𝐴 +𝑐
2𝑜) ∧ (𝐴 +𝑐
2𝑜) ≼ 𝒫 𝐴) → (𝐴 +𝑐
1𝑜) ≼ 𝒫 𝐴) |
7 | 4, 5, 6 | sylancr 695 |
. 2
⊢
(1𝑜 ≺ 𝐴 → (𝐴 +𝑐
1𝑜) ≼ 𝒫 𝐴) |
8 | | fal 1490 |
. . 3
⊢ ¬
⊥ |
9 | | ensym 8005 |
. . . . 5
⊢ ((𝐴 +𝑐
1𝑜) ≈ 𝒫 𝐴 → 𝒫 𝐴 ≈ (𝐴 +𝑐
1𝑜)) |
10 | | bren 7964 |
. . . . 5
⊢
(𝒫 𝐴 ≈
(𝐴 +𝑐
1𝑜) ↔ ∃𝑓 𝑓:𝒫 𝐴–1-1-onto→(𝐴 +𝑐
1𝑜)) |
11 | 9, 10 | sylib 208 |
. . . 4
⊢ ((𝐴 +𝑐
1𝑜) ≈ 𝒫 𝐴 → ∃𝑓 𝑓:𝒫 𝐴–1-1-onto→(𝐴 +𝑐
1𝑜)) |
12 | | f1of 6137 |
. . . . . . . . . 10
⊢ (𝑓:𝒫 𝐴–1-1-onto→(𝐴 +𝑐
1𝑜) → 𝑓:𝒫 𝐴⟶(𝐴 +𝑐
1𝑜)) |
13 | | relsdom 7962 |
. . . . . . . . . . . 12
⊢ Rel
≺ |
14 | 13 | brrelex2i 5159 |
. . . . . . . . . . 11
⊢
(1𝑜 ≺ 𝐴 → 𝐴 ∈ V) |
15 | | pwidg 4173 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ V → 𝐴 ∈ 𝒫 𝐴) |
16 | 14, 15 | syl 17 |
. . . . . . . . . 10
⊢
(1𝑜 ≺ 𝐴 → 𝐴 ∈ 𝒫 𝐴) |
17 | | ffvelrn 6357 |
. . . . . . . . . 10
⊢ ((𝑓:𝒫 𝐴⟶(𝐴 +𝑐
1𝑜) ∧ 𝐴 ∈ 𝒫 𝐴) → (𝑓‘𝐴) ∈ (𝐴 +𝑐
1𝑜)) |
18 | 12, 16, 17 | syl2anr 495 |
. . . . . . . . 9
⊢
((1𝑜 ≺ 𝐴 ∧ 𝑓:𝒫 𝐴–1-1-onto→(𝐴 +𝑐
1𝑜)) → (𝑓‘𝐴) ∈ (𝐴 +𝑐
1𝑜)) |
19 | | cda1dif 8998 |
. . . . . . . . 9
⊢ ((𝑓‘𝐴) ∈ (𝐴 +𝑐
1𝑜) → ((𝐴 +𝑐
1𝑜) ∖ {(𝑓‘𝐴)}) ≈ 𝐴) |
20 | 18, 19 | syl 17 |
. . . . . . . 8
⊢
((1𝑜 ≺ 𝐴 ∧ 𝑓:𝒫 𝐴–1-1-onto→(𝐴 +𝑐
1𝑜)) → ((𝐴 +𝑐
1𝑜) ∖ {(𝑓‘𝐴)}) ≈ 𝐴) |
21 | | bren 7964 |
. . . . . . . 8
⊢ (((𝐴 +𝑐
1𝑜) ∖ {(𝑓‘𝐴)}) ≈ 𝐴 ↔ ∃𝑔 𝑔:((𝐴 +𝑐
1𝑜) ∖ {(𝑓‘𝐴)})–1-1-onto→𝐴) |
22 | 20, 21 | sylib 208 |
. . . . . . 7
⊢
((1𝑜 ≺ 𝐴 ∧ 𝑓:𝒫 𝐴–1-1-onto→(𝐴 +𝑐
1𝑜)) → ∃𝑔 𝑔:((𝐴 +𝑐
1𝑜) ∖ {(𝑓‘𝐴)})–1-1-onto→𝐴) |
23 | | simpll 790 |
. . . . . . . . 9
⊢
(((1𝑜 ≺ 𝐴 ∧ 𝑓:𝒫 𝐴–1-1-onto→(𝐴 +𝑐
1𝑜)) ∧ 𝑔:((𝐴 +𝑐
1𝑜) ∖ {(𝑓‘𝐴)})–1-1-onto→𝐴) → 1𝑜
≺ 𝐴) |
24 | | simplr 792 |
. . . . . . . . 9
⊢
(((1𝑜 ≺ 𝐴 ∧ 𝑓:𝒫 𝐴–1-1-onto→(𝐴 +𝑐
1𝑜)) ∧ 𝑔:((𝐴 +𝑐
1𝑜) ∖ {(𝑓‘𝐴)})–1-1-onto→𝐴) → 𝑓:𝒫 𝐴–1-1-onto→(𝐴 +𝑐
1𝑜)) |
25 | | simpr 477 |
. . . . . . . . 9
⊢
(((1𝑜 ≺ 𝐴 ∧ 𝑓:𝒫 𝐴–1-1-onto→(𝐴 +𝑐
1𝑜)) ∧ 𝑔:((𝐴 +𝑐
1𝑜) ∖ {(𝑓‘𝐴)})–1-1-onto→𝐴) → 𝑔:((𝐴 +𝑐
1𝑜) ∖ {(𝑓‘𝐴)})–1-1-onto→𝐴) |
26 | | eqeq1 2626 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑥 → (𝑤 = 𝐴 ↔ 𝑥 = 𝐴)) |
27 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑥 → 𝑤 = 𝑥) |
28 | 26, 27 | ifbieq2d 4111 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑥 → if(𝑤 = 𝐴, ∅, 𝑤) = if(𝑥 = 𝐴, ∅, 𝑥)) |
29 | 28 | cbvmptv 4750 |
. . . . . . . . . 10
⊢ (𝑤 ∈ 𝒫 𝐴 ↦ if(𝑤 = 𝐴, ∅, 𝑤)) = (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)) |
30 | 29 | coeq2i 5282 |
. . . . . . . . 9
⊢ ((𝑔 ∘ 𝑓) ∘ (𝑤 ∈ 𝒫 𝐴 ↦ if(𝑤 = 𝐴, ∅, 𝑤))) = ((𝑔 ∘ 𝑓) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))) |
31 | | eqid 2622 |
. . . . . . . . . 10
⊢
{〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 (((𝑔 ∘ 𝑓) ∘ (𝑤 ∈ 𝒫 𝐴 ↦ if(𝑤 = 𝐴, ∅, 𝑤)))‘(◡𝑠 “ {𝑧})) = 𝑧))} = {〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 (((𝑔 ∘ 𝑓) ∘ (𝑤 ∈ 𝒫 𝐴 ↦ if(𝑤 = 𝐴, ∅, 𝑤)))‘(◡𝑠 “ {𝑧})) = 𝑧))} |
32 | 31 | fpwwecbv 9466 |
. . . . . . . . 9
⊢
{〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 (((𝑔 ∘ 𝑓) ∘ (𝑤 ∈ 𝒫 𝐴 ↦ if(𝑤 = 𝐴, ∅, 𝑤)))‘(◡𝑠 “ {𝑧})) = 𝑧))} = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (((𝑔 ∘ 𝑓) ∘ (𝑤 ∈ 𝒫 𝐴 ↦ if(𝑤 = 𝐴, ∅, 𝑤)))‘(◡𝑟 “ {𝑦})) = 𝑦))} |
33 | | eqid 2622 |
. . . . . . . . 9
⊢ ∪ dom {〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 (((𝑔 ∘ 𝑓) ∘ (𝑤 ∈ 𝒫 𝐴 ↦ if(𝑤 = 𝐴, ∅, 𝑤)))‘(◡𝑠 “ {𝑧})) = 𝑧))} = ∪ dom
{〈𝑎, 𝑠〉 ∣ ((𝑎 ⊆ 𝐴 ∧ 𝑠 ⊆ (𝑎 × 𝑎)) ∧ (𝑠 We 𝑎 ∧ ∀𝑧 ∈ 𝑎 (((𝑔 ∘ 𝑓) ∘ (𝑤 ∈ 𝒫 𝐴 ↦ if(𝑤 = 𝐴, ∅, 𝑤)))‘(◡𝑠 “ {𝑧})) = 𝑧))} |
34 | 23, 24, 25, 30, 32, 33 | canthp1lem2 9475 |
. . . . . . . 8
⊢ ¬
((1𝑜 ≺ 𝐴 ∧ 𝑓:𝒫 𝐴–1-1-onto→(𝐴 +𝑐
1𝑜)) ∧ 𝑔:((𝐴 +𝑐
1𝑜) ∖ {(𝑓‘𝐴)})–1-1-onto→𝐴) |
35 | 34 | pm2.21i 116 |
. . . . . . 7
⊢
(((1𝑜 ≺ 𝐴 ∧ 𝑓:𝒫 𝐴–1-1-onto→(𝐴 +𝑐
1𝑜)) ∧ 𝑔:((𝐴 +𝑐
1𝑜) ∖ {(𝑓‘𝐴)})–1-1-onto→𝐴) →
⊥) |
36 | 22, 35 | exlimddv 1863 |
. . . . . 6
⊢
((1𝑜 ≺ 𝐴 ∧ 𝑓:𝒫 𝐴–1-1-onto→(𝐴 +𝑐
1𝑜)) → ⊥) |
37 | 36 | ex 450 |
. . . . 5
⊢
(1𝑜 ≺ 𝐴 → (𝑓:𝒫 𝐴–1-1-onto→(𝐴 +𝑐
1𝑜) → ⊥)) |
38 | 37 | exlimdv 1861 |
. . . 4
⊢
(1𝑜 ≺ 𝐴 → (∃𝑓 𝑓:𝒫 𝐴–1-1-onto→(𝐴 +𝑐
1𝑜) → ⊥)) |
39 | 11, 38 | syl5 34 |
. . 3
⊢
(1𝑜 ≺ 𝐴 → ((𝐴 +𝑐
1𝑜) ≈ 𝒫 𝐴 → ⊥)) |
40 | 8, 39 | mtoi 190 |
. 2
⊢
(1𝑜 ≺ 𝐴 → ¬ (𝐴 +𝑐
1𝑜) ≈ 𝒫 𝐴) |
41 | | brsdom 7978 |
. 2
⊢ ((𝐴 +𝑐
1𝑜) ≺ 𝒫 𝐴 ↔ ((𝐴 +𝑐
1𝑜) ≼ 𝒫 𝐴 ∧ ¬ (𝐴 +𝑐
1𝑜) ≈ 𝒫 𝐴)) |
42 | 7, 40, 41 | sylanbrc 698 |
1
⊢
(1𝑜 ≺ 𝐴 → (𝐴 +𝑐
1𝑜) ≺ 𝒫 𝐴) |