Proof of Theorem canthp1lem2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | canthp1lem2.1 | . . . . . 6
⊢ (𝜑 → 1o ≺
𝐴) | 
| 2 |  | relsdom 8993 | . . . . . . 7
⊢ Rel
≺ | 
| 3 | 2 | brrelex2i 5741 | . . . . . 6
⊢
(1o ≺ 𝐴 → 𝐴 ∈ V) | 
| 4 | 1, 3 | syl 17 | . . . . 5
⊢ (𝜑 → 𝐴 ∈ V) | 
| 5 | 4 | pwexd 5378 | . . . 4
⊢ (𝜑 → 𝒫 𝐴 ∈ V) | 
| 6 |  | canthp1lem2.2 | . . . 4
⊢ (𝜑 → 𝐹:𝒫 𝐴–1-1-onto→(𝐴 ⊔ 1o)) | 
| 7 |  | f1oeng 9012 | . . . 4
⊢
((𝒫 𝐴 ∈
V ∧ 𝐹:𝒫 𝐴–1-1-onto→(𝐴 ⊔ 1o)) → 𝒫
𝐴 ≈ (𝐴 ⊔
1o)) | 
| 8 | 5, 6, 7 | syl2anc 584 | . . 3
⊢ (𝜑 → 𝒫 𝐴 ≈ (𝐴 ⊔ 1o)) | 
| 9 | 8 | ensymd 9046 | . 2
⊢ (𝜑 → (𝐴 ⊔ 1o) ≈ 𝒫
𝐴) | 
| 10 |  | canth2g 9172 | . . . . . . . . . . 11
⊢ (𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴) | 
| 11 | 4, 10 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝐴 ≺ 𝒫 𝐴) | 
| 12 |  | sdomen2 9163 | . . . . . . . . . . 11
⊢
(𝒫 𝐴 ≈
(𝐴 ⊔ 1o)
→ (𝐴 ≺ 𝒫
𝐴 ↔ 𝐴 ≺ (𝐴 ⊔ 1o))) | 
| 13 | 8, 12 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝐴 ≺ 𝒫 𝐴 ↔ 𝐴 ≺ (𝐴 ⊔ 1o))) | 
| 14 | 11, 13 | mpbid 232 | . . . . . . . . 9
⊢ (𝜑 → 𝐴 ≺ (𝐴 ⊔ 1o)) | 
| 15 |  | sdomnen 9022 | . . . . . . . . 9
⊢ (𝐴 ≺ (𝐴 ⊔ 1o) → ¬ 𝐴 ≈ (𝐴 ⊔ 1o)) | 
| 16 | 14, 15 | syl 17 | . . . . . . . 8
⊢ (𝜑 → ¬ 𝐴 ≈ (𝐴 ⊔ 1o)) | 
| 17 |  | omelon 9687 | . . . . . . . . . . . 12
⊢ ω
∈ On | 
| 18 |  | onenon 9990 | . . . . . . . . . . . 12
⊢ (ω
∈ On → ω ∈ dom card) | 
| 19 | 17, 18 | ax-mp 5 | . . . . . . . . . . 11
⊢ ω
∈ dom card | 
| 20 |  | canthp1lem2.3 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐺:((𝐴 ⊔ 1o) ∖ {(𝐹‘𝐴)})–1-1-onto→𝐴) | 
| 21 |  | dff1o3 6853 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹:𝒫 𝐴–1-1-onto→(𝐴 ⊔ 1o) ↔ (𝐹:𝒫 𝐴–onto→(𝐴 ⊔ 1o) ∧ Fun ◡𝐹)) | 
| 22 | 21 | simprbi 496 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹:𝒫 𝐴–1-1-onto→(𝐴 ⊔ 1o) → Fun ◡𝐹) | 
| 23 | 6, 22 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → Fun ◡𝐹) | 
| 24 |  | f1ofo 6854 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹:𝒫 𝐴–1-1-onto→(𝐴 ⊔ 1o) → 𝐹:𝒫 𝐴–onto→(𝐴 ⊔ 1o)) | 
| 25 | 6, 24 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐹:𝒫 𝐴–onto→(𝐴 ⊔ 1o)) | 
| 26 |  | f1ofn 6848 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹:𝒫 𝐴–1-1-onto→(𝐴 ⊔ 1o) → 𝐹 Fn 𝒫 𝐴) | 
| 27 |  | fnresdm 6686 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹 Fn 𝒫 𝐴 → (𝐹 ↾ 𝒫 𝐴) = 𝐹) | 
| 28 |  | foeq1 6815 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐹 ↾ 𝒫 𝐴) = 𝐹 → ((𝐹 ↾ 𝒫 𝐴):𝒫 𝐴–onto→(𝐴 ⊔ 1o) ↔ 𝐹:𝒫 𝐴–onto→(𝐴 ⊔ 1o))) | 
| 29 | 6, 26, 27, 28 | 4syl 19 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((𝐹 ↾ 𝒫 𝐴):𝒫 𝐴–onto→(𝐴 ⊔ 1o) ↔ 𝐹:𝒫 𝐴–onto→(𝐴 ⊔ 1o))) | 
| 30 | 25, 29 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐹 ↾ 𝒫 𝐴):𝒫 𝐴–onto→(𝐴 ⊔ 1o)) | 
| 31 |  | fvex 6918 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐹‘𝐴) ∈ V | 
| 32 |  | f1osng 6888 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ∈ V ∧ (𝐹‘𝐴) ∈ V) → {〈𝐴, (𝐹‘𝐴)〉}:{𝐴}–1-1-onto→{(𝐹‘𝐴)}) | 
| 33 | 4, 31, 32 | sylancl 586 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → {〈𝐴, (𝐹‘𝐴)〉}:{𝐴}–1-1-onto→{(𝐹‘𝐴)}) | 
| 34 | 6, 26 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝐹 Fn 𝒫 𝐴) | 
| 35 |  | pwidg 4619 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐴 ∈ V → 𝐴 ∈ 𝒫 𝐴) | 
| 36 | 4, 35 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝐴 ∈ 𝒫 𝐴) | 
| 37 |  | fnressn 7177 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹 Fn 𝒫 𝐴 ∧ 𝐴 ∈ 𝒫 𝐴) → (𝐹 ↾ {𝐴}) = {〈𝐴, (𝐹‘𝐴)〉}) | 
| 38 | 34, 36, 37 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝐹 ↾ {𝐴}) = {〈𝐴, (𝐹‘𝐴)〉}) | 
| 39 | 38 | f1oeq1d 6842 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((𝐹 ↾ {𝐴}):{𝐴}–1-1-onto→{(𝐹‘𝐴)} ↔ {〈𝐴, (𝐹‘𝐴)〉}:{𝐴}–1-1-onto→{(𝐹‘𝐴)})) | 
| 40 | 33, 39 | mpbird 257 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐹 ↾ {𝐴}):{𝐴}–1-1-onto→{(𝐹‘𝐴)}) | 
| 41 |  | f1ofo 6854 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐹 ↾ {𝐴}):{𝐴}–1-1-onto→{(𝐹‘𝐴)} → (𝐹 ↾ {𝐴}):{𝐴}–onto→{(𝐹‘𝐴)}) | 
| 42 | 40, 41 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐹 ↾ {𝐴}):{𝐴}–onto→{(𝐹‘𝐴)}) | 
| 43 |  | resdif 6868 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((Fun
◡𝐹 ∧ (𝐹 ↾ 𝒫 𝐴):𝒫 𝐴–onto→(𝐴 ⊔ 1o) ∧ (𝐹 ↾ {𝐴}):{𝐴}–onto→{(𝐹‘𝐴)}) → (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→((𝐴 ⊔ 1o) ∖ {(𝐹‘𝐴)})) | 
| 44 | 23, 30, 42, 43 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→((𝐴 ⊔ 1o) ∖ {(𝐹‘𝐴)})) | 
| 45 |  | f1oco 6870 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺:((𝐴 ⊔ 1o) ∖ {(𝐹‘𝐴)})–1-1-onto→𝐴 ∧ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→((𝐴 ⊔ 1o) ∖ {(𝐹‘𝐴)})) → (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→𝐴) | 
| 46 | 20, 44, 45 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→𝐴) | 
| 47 |  | resco 6269 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) = (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))) | 
| 48 |  | f1oeq1 6835 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) = (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))) → (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→𝐴 ↔ (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→𝐴)) | 
| 49 | 47, 48 | ax-mp 5 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→𝐴 ↔ (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→𝐴) | 
| 50 | 46, 49 | sylibr 234 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→𝐴) | 
| 51 |  | f1of 6847 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→𝐴 → ((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})⟶𝐴) | 
| 52 | 50, 51 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})⟶𝐴) | 
| 53 |  | 0elpw 5355 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ∅
∈ 𝒫 𝐴 | 
| 54 | 53 | a1i 11 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) ∧ 𝑥 = 𝐴) → ∅ ∈ 𝒫 𝐴) | 
| 55 |  | sdom0 9149 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢  ¬
1o ≺ ∅ | 
| 56 |  | breq2 5146 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (∅
= 𝐴 → (1o
≺ ∅ ↔ 1o ≺ 𝐴)) | 
| 57 | 55, 56 | mtbii 326 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (∅
= 𝐴 → ¬
1o ≺ 𝐴) | 
| 58 | 57 | necon2ai 2969 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(1o ≺ 𝐴 → ∅ ≠ 𝐴) | 
| 59 | 1, 58 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ∅ ≠ 𝐴) | 
| 60 | 59 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) ∧ 𝑥 = 𝐴) → ∅ ≠ 𝐴) | 
| 61 |  | eldifsn 4785 | . . . . . . . . . . . . . . . . . . . 20
⊢ (∅
∈ (𝒫 𝐴 ∖
{𝐴}) ↔ (∅ ∈
𝒫 𝐴 ∧ ∅
≠ 𝐴)) | 
| 62 | 54, 60, 61 | sylanbrc 583 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) ∧ 𝑥 = 𝐴) → ∅ ∈ (𝒫 𝐴 ∖ {𝐴})) | 
| 63 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → 𝑥 ∈ 𝒫 𝐴) | 
| 64 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → ¬ 𝑥 = 𝐴) | 
| 65 | 64 | neqned 2946 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → 𝑥 ≠ 𝐴) | 
| 66 |  | eldifsn 4785 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (𝒫 𝐴 ∖ {𝐴}) ↔ (𝑥 ∈ 𝒫 𝐴 ∧ 𝑥 ≠ 𝐴)) | 
| 67 | 63, 65, 66 | sylanbrc 583 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → 𝑥 ∈ (𝒫 𝐴 ∖ {𝐴})) | 
| 68 | 62, 67 | ifclda 4560 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝒫 𝐴) → if(𝑥 = 𝐴, ∅, 𝑥) ∈ (𝒫 𝐴 ∖ {𝐴})) | 
| 69 | 68 | fmpttd 7134 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)):𝒫 𝐴⟶(𝒫 𝐴 ∖ {𝐴})) | 
| 70 | 52, 69 | fcod 6760 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))):𝒫 𝐴⟶𝐴) | 
| 71 | 69 | frnd 6743 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ran (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)) ⊆ (𝒫 𝐴 ∖ {𝐴})) | 
| 72 |  | cores 6268 | . . . . . . . . . . . . . . . . . . 19
⊢ (ran
(𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)) ⊆ (𝒫 𝐴 ∖ {𝐴}) → (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))) = ((𝐺 ∘ 𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))) | 
| 73 | 71, 72 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))) = ((𝐺 ∘ 𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))) | 
| 74 |  | canthp1lem2.4 | . . . . . . . . . . . . . . . . . 18
⊢ 𝐻 = ((𝐺 ∘ 𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))) | 
| 75 | 73, 74 | eqtr4di 2794 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))) = 𝐻) | 
| 76 | 75 | feq1d 6719 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))):𝒫 𝐴⟶𝐴 ↔ 𝐻:𝒫 𝐴⟶𝐴)) | 
| 77 | 70, 76 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐻:𝒫 𝐴⟶𝐴) | 
| 78 |  | inss1 4236 | . . . . . . . . . . . . . . . 16
⊢
(𝒫 𝐴 ∩
dom card) ⊆ 𝒫 𝐴 | 
| 79 | 78 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝒫 𝐴 ∩ dom card) ⊆
𝒫 𝐴) | 
| 80 |  | canthp1lem2.5 | . . . . . . . . . . . . . . . 16
⊢ 𝑊 = {〈𝑥, 𝑟〉 ∣ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝐻‘(◡𝑟 “ {𝑦})) = 𝑦))} | 
| 81 |  | canthp1lem2.6 | . . . . . . . . . . . . . . . 16
⊢ 𝐵 = ∪
dom 𝑊 | 
| 82 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢ (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) = (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) | 
| 83 | 80, 81, 82 | canth4 10688 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ V ∧ 𝐻:𝒫 𝐴⟶𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝒫 𝐴) → (𝐵 ⊆ 𝐴 ∧ (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ⊊ 𝐵 ∧ (𝐻‘𝐵) = (𝐻‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})))) | 
| 84 | 4, 77, 79, 83 | syl3anc 1372 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 ⊆ 𝐴 ∧ (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ⊊ 𝐵 ∧ (𝐻‘𝐵) = (𝐻‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})))) | 
| 85 | 84 | simp1d 1142 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ⊆ 𝐴) | 
| 86 | 84 | simp2d 1143 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ⊊ 𝐵) | 
| 87 | 86 | pssned 4100 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ≠ 𝐵) | 
| 88 | 87 | necomd 2995 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ≠ (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) | 
| 89 | 84 | simp3d 1144 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝐻‘𝐵) = (𝐻‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}))) | 
| 90 | 74 | fveq1i 6906 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐻‘𝐵) = (((𝐺 ∘ 𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘𝐵) | 
| 91 | 74 | fveq1i 6906 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐻‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) = (((𝐺 ∘ 𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) | 
| 92 | 89, 90, 91 | 3eqtr3g 2799 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (((𝐺 ∘ 𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘𝐵) = (((𝐺 ∘ 𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}))) | 
| 93 | 4, 85 | sselpwd 5327 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐵 ∈ 𝒫 𝐴) | 
| 94 | 69, 93 | fvco3d 7008 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (((𝐺 ∘ 𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘𝐵) = ((𝐺 ∘ 𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵))) | 
| 95 | 86 | pssssd 4099 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ⊆ 𝐵) | 
| 96 | 95, 85 | sstrd 3993 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ⊆ 𝐴) | 
| 97 | 4, 96 | sselpwd 5327 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ∈ 𝒫 𝐴) | 
| 98 | 69, 97 | fvco3d 7008 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (((𝐺 ∘ 𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) = ((𝐺 ∘ 𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})))) | 
| 99 | 92, 94, 98 | 3eqtr3d 2784 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝐺 ∘ 𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)) = ((𝐺 ∘ 𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})))) | 
| 100 | 99 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → ((𝐺 ∘ 𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)) = ((𝐺 ∘ 𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})))) | 
| 101 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)) = (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)) | 
| 102 |  | eqeq1 2740 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝐵 → (𝑥 = 𝐴 ↔ 𝐵 = 𝐴)) | 
| 103 |  | id 22 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝐵 → 𝑥 = 𝐵) | 
| 104 | 102, 103 | ifbieq2d 4551 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝐵 → if(𝑥 = 𝐴, ∅, 𝑥) = if(𝐵 = 𝐴, ∅, 𝐵)) | 
| 105 |  | ifcl 4570 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((∅
∈ 𝒫 𝐴 ∧
𝐵 ∈ 𝒫 𝐴) → if(𝐵 = 𝐴, ∅, 𝐵) ∈ 𝒫 𝐴) | 
| 106 | 53, 93, 105 | sylancr 587 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → if(𝐵 = 𝐴, ∅, 𝐵) ∈ 𝒫 𝐴) | 
| 107 | 101, 104,
93, 106 | fvmptd3 7038 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵) = if(𝐵 = 𝐴, ∅, 𝐵)) | 
| 108 |  | pssne 4098 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐵 ⊊ 𝐴 → 𝐵 ≠ 𝐴) | 
| 109 | 108 | neneqd 2944 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐵 ⊊ 𝐴 → ¬ 𝐵 = 𝐴) | 
| 110 | 109 | iffalsed 4535 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐵 ⊊ 𝐴 → if(𝐵 = 𝐴, ∅, 𝐵) = 𝐵) | 
| 111 | 107, 110 | sylan9eq 2796 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵) = 𝐵) | 
| 112 | 111 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → ((𝐺 ∘ 𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)) = ((𝐺 ∘ 𝐹)‘𝐵)) | 
| 113 |  | eqeq1 2740 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) → (𝑥 = 𝐴 ↔ (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) = 𝐴)) | 
| 114 |  | id 22 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) → 𝑥 = (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) | 
| 115 | 113, 114 | ifbieq2d 4551 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) → if(𝑥 = 𝐴, ∅, 𝑥) = if((◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) = 𝐴, ∅, (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}))) | 
| 116 |  | ifcl 4570 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((∅
∈ 𝒫 𝐴 ∧
(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ∈ 𝒫 𝐴) → if((◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) = 𝐴, ∅, (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) ∈ 𝒫 𝐴) | 
| 117 | 53, 97, 116 | sylancr 587 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → if((◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) = 𝐴, ∅, (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) ∈ 𝒫 𝐴) | 
| 118 | 101, 115,
97, 117 | fvmptd3 7038 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) = if((◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) = 𝐴, ∅, (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}))) | 
| 119 | 118 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) = if((◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) = 𝐴, ∅, (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}))) | 
| 120 |  | sspsstr 4107 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ⊆ 𝐵 ∧ 𝐵 ⊊ 𝐴) → (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ⊊ 𝐴) | 
| 121 | 95, 120 | sylan 580 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ⊊ 𝐴) | 
| 122 | 121 | pssned 4100 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ≠ 𝐴) | 
| 123 | 122 | neneqd 2944 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → ¬ (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) = 𝐴) | 
| 124 | 123 | iffalsed 4535 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → if((◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) = 𝐴, ∅, (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) = (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) | 
| 125 | 119, 124 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) = (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) | 
| 126 | 125 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → ((𝐺 ∘ 𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}))) = ((𝐺 ∘ 𝐹)‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}))) | 
| 127 | 100, 112,
126 | 3eqtr3d 2784 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → ((𝐺 ∘ 𝐹)‘𝐵) = ((𝐺 ∘ 𝐹)‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}))) | 
| 128 | 93, 108 | anim12i 613 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → (𝐵 ∈ 𝒫 𝐴 ∧ 𝐵 ≠ 𝐴)) | 
| 129 |  | eldifsn 4785 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐵 ∈ (𝒫 𝐴 ∖ {𝐴}) ↔ (𝐵 ∈ 𝒫 𝐴 ∧ 𝐵 ≠ 𝐴)) | 
| 130 | 128, 129 | sylibr 234 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → 𝐵 ∈ (𝒫 𝐴 ∖ {𝐴})) | 
| 131 | 130 | fvresd 6925 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = ((𝐺 ∘ 𝐹)‘𝐵)) | 
| 132 | 97 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ∈ 𝒫 𝐴) | 
| 133 |  | eldifsn 4785 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ∈ (𝒫 𝐴 ∖ {𝐴}) ↔ ((◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ∈ 𝒫 𝐴 ∧ (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ≠ 𝐴)) | 
| 134 | 132, 122,
133 | sylanbrc 583 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ∈ (𝒫 𝐴 ∖ {𝐴})) | 
| 135 | 134 | fvresd 6925 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) = ((𝐺 ∘ 𝐹)‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}))) | 
| 136 | 127, 131,
135 | 3eqtr4d 2786 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}))) | 
| 137 |  | f1of1 6846 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→𝐴 → ((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1→𝐴) | 
| 138 | 50, 137 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1→𝐴) | 
| 139 | 138 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → ((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1→𝐴) | 
| 140 |  | f1fveq 7283 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1→𝐴 ∧ (𝐵 ∈ (𝒫 𝐴 ∖ {𝐴}) ∧ (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) ∈ (𝒫 𝐴 ∖ {𝐴}))) → ((((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) ↔ 𝐵 = (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}))) | 
| 141 | 139, 130,
134, 140 | syl12anc 836 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → ((((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = (((𝐺 ∘ 𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘(◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) ↔ 𝐵 = (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}))) | 
| 142 | 136, 141 | mpbid 232 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝐵 ⊊ 𝐴) → 𝐵 = (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)})) | 
| 143 | 142 | ex 412 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐵 ⊊ 𝐴 → 𝐵 = (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}))) | 
| 144 | 143 | necon3ad 2952 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐵 ≠ (◡(𝑊‘𝐵) “ {(𝐻‘𝐵)}) → ¬ 𝐵 ⊊ 𝐴)) | 
| 145 | 88, 144 | mpd 15 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ¬ 𝐵 ⊊ 𝐴) | 
| 146 |  | npss 4112 | . . . . . . . . . . . . . 14
⊢ (¬
𝐵 ⊊ 𝐴 ↔ (𝐵 ⊆ 𝐴 → 𝐵 = 𝐴)) | 
| 147 | 145, 146 | sylib 218 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵 ⊆ 𝐴 → 𝐵 = 𝐴)) | 
| 148 | 85, 147 | mpd 15 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 = 𝐴) | 
| 149 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . 19
⊢ 𝐵 = 𝐵 | 
| 150 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑊‘𝐵) = (𝑊‘𝐵) | 
| 151 | 149, 150 | pm3.2i 470 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐵 = 𝐵 ∧ (𝑊‘𝐵) = (𝑊‘𝐵)) | 
| 152 |  | elinel1 4200 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ dom card) → 𝑥 ∈ 𝒫 𝐴) | 
| 153 |  | ffvelcdm 7100 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐻:𝒫 𝐴⟶𝐴 ∧ 𝑥 ∈ 𝒫 𝐴) → (𝐻‘𝑥) ∈ 𝐴) | 
| 154 | 77, 152, 153 | syl2an 596 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ dom card)) → (𝐻‘𝑥) ∈ 𝐴) | 
| 155 | 80, 4, 154, 81 | fpwwe 10687 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐵𝑊(𝑊‘𝐵) ∧ (𝐻‘𝐵) ∈ 𝐵) ↔ (𝐵 = 𝐵 ∧ (𝑊‘𝐵) = (𝑊‘𝐵)))) | 
| 156 | 151, 155 | mpbiri 258 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐵𝑊(𝑊‘𝐵) ∧ (𝐻‘𝐵) ∈ 𝐵)) | 
| 157 | 156 | simpld 494 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵𝑊(𝑊‘𝐵)) | 
| 158 | 80, 4 | fpwwelem 10686 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐵𝑊(𝑊‘𝐵) ↔ ((𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊‘𝐵) We 𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝐻‘(◡(𝑊‘𝐵) “ {𝑦})) = 𝑦)))) | 
| 159 | 157, 158 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐵 ⊆ 𝐴 ∧ (𝑊‘𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊‘𝐵) We 𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝐻‘(◡(𝑊‘𝐵) “ {𝑦})) = 𝑦))) | 
| 160 | 159 | simprld 771 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑊‘𝐵) We 𝐵) | 
| 161 |  | fvex 6918 | . . . . . . . . . . . . . . 15
⊢ (𝑊‘𝐵) ∈ V | 
| 162 |  | weeq1 5671 | . . . . . . . . . . . . . . 15
⊢ (𝑟 = (𝑊‘𝐵) → (𝑟 We 𝐵 ↔ (𝑊‘𝐵) We 𝐵)) | 
| 163 | 161, 162 | spcev 3605 | . . . . . . . . . . . . . 14
⊢ ((𝑊‘𝐵) We 𝐵 → ∃𝑟 𝑟 We 𝐵) | 
| 164 | 160, 163 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → ∃𝑟 𝑟 We 𝐵) | 
| 165 |  | ween 10076 | . . . . . . . . . . . . 13
⊢ (𝐵 ∈ dom card ↔
∃𝑟 𝑟 We 𝐵) | 
| 166 | 164, 165 | sylibr 234 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ dom card) | 
| 167 | 148, 166 | eqeltrrd 2841 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ dom card) | 
| 168 |  | domtri2 10030 | . . . . . . . . . . 11
⊢ ((ω
∈ dom card ∧ 𝐴
∈ dom card) → (ω ≼ 𝐴 ↔ ¬ 𝐴 ≺ ω)) | 
| 169 | 19, 167, 168 | sylancr 587 | . . . . . . . . . 10
⊢ (𝜑 → (ω ≼ 𝐴 ↔ ¬ 𝐴 ≺ ω)) | 
| 170 |  | infdju1 10231 | . . . . . . . . . 10
⊢ (ω
≼ 𝐴 → (𝐴 ⊔ 1o) ≈
𝐴) | 
| 171 | 169, 170 | biimtrrdi 254 | . . . . . . . . 9
⊢ (𝜑 → (¬ 𝐴 ≺ ω → (𝐴 ⊔ 1o) ≈ 𝐴)) | 
| 172 |  | ensym 9044 | . . . . . . . . 9
⊢ ((𝐴 ⊔ 1o) ≈
𝐴 → 𝐴 ≈ (𝐴 ⊔ 1o)) | 
| 173 | 171, 172 | syl6 35 | . . . . . . . 8
⊢ (𝜑 → (¬ 𝐴 ≺ ω → 𝐴 ≈ (𝐴 ⊔ 1o))) | 
| 174 | 16, 173 | mt3d 148 | . . . . . . 7
⊢ (𝜑 → 𝐴 ≺ ω) | 
| 175 |  | 2onn 8681 | . . . . . . . 8
⊢
2o ∈ ω | 
| 176 |  | nnsdom 9695 | . . . . . . . 8
⊢
(2o ∈ ω → 2o ≺
ω) | 
| 177 | 175, 176 | ax-mp 5 | . . . . . . 7
⊢
2o ≺ ω | 
| 178 |  | djufi 10228 | . . . . . . 7
⊢ ((𝐴 ≺ ω ∧
2o ≺ ω) → (𝐴 ⊔ 2o) ≺
ω) | 
| 179 | 174, 177,
178 | sylancl 586 | . . . . . 6
⊢ (𝜑 → (𝐴 ⊔ 2o) ≺
ω) | 
| 180 |  | isfinite 9693 | . . . . . 6
⊢ ((𝐴 ⊔ 2o) ∈
Fin ↔ (𝐴 ⊔
2o) ≺ ω) | 
| 181 | 179, 180 | sylibr 234 | . . . . 5
⊢ (𝜑 → (𝐴 ⊔ 2o) ∈
Fin) | 
| 182 |  | sssucid 6463 | . . . . . . . . . 10
⊢
1o ⊆ suc 1o | 
| 183 |  | df-2o 8508 | . . . . . . . . . 10
⊢
2o = suc 1o | 
| 184 | 182, 183 | sseqtrri 4032 | . . . . . . . . 9
⊢
1o ⊆ 2o | 
| 185 |  | xpss2 5704 | . . . . . . . . 9
⊢
(1o ⊆ 2o → ({1o} ×
1o) ⊆ ({1o} ×
2o)) | 
| 186 | 184, 185 | ax-mp 5 | . . . . . . . 8
⊢
({1o} × 1o) ⊆ ({1o} ×
2o) | 
| 187 |  | unss2 4186 | . . . . . . . 8
⊢
(({1o} × 1o) ⊆ ({1o}
× 2o) → (({∅} × 𝐴) ∪ ({1o} ×
1o)) ⊆ (({∅} × 𝐴) ∪ ({1o} ×
2o))) | 
| 188 | 186, 187 | mp1i 13 | . . . . . . 7
⊢ (𝜑 → (({∅} × 𝐴) ∪ ({1o} ×
1o)) ⊆ (({∅} × 𝐴) ∪ ({1o} ×
2o))) | 
| 189 |  | ssun2 4178 | . . . . . . . . 9
⊢
({1o} × 2o) ⊆ (({∅} ×
𝐴) ∪ ({1o}
× 2o)) | 
| 190 |  | 1oex 8517 | . . . . . . . . . . 11
⊢
1o ∈ V | 
| 191 | 190 | snid 4661 | . . . . . . . . . 10
⊢
1o ∈ {1o} | 
| 192 | 190 | sucid 6465 | . . . . . . . . . . 11
⊢
1o ∈ suc 1o | 
| 193 | 192, 183 | eleqtrri 2839 | . . . . . . . . . 10
⊢
1o ∈ 2o | 
| 194 |  | opelxpi 5721 | . . . . . . . . . 10
⊢
((1o ∈ {1o} ∧ 1o ∈
2o) → 〈1o, 1o〉 ∈
({1o} × 2o)) | 
| 195 | 191, 193,
194 | mp2an 692 | . . . . . . . . 9
⊢
〈1o, 1o〉 ∈ ({1o} ×
2o) | 
| 196 | 189, 195 | sselii 3979 | . . . . . . . 8
⊢
〈1o, 1o〉 ∈ (({∅} ×
𝐴) ∪ ({1o}
× 2o)) | 
| 197 |  | 1n0 8527 | . . . . . . . . . . . 12
⊢
1o ≠ ∅ | 
| 198 | 197 | neii 2941 | . . . . . . . . . . 11
⊢  ¬
1o = ∅ | 
| 199 |  | opelxp1 5726 | . . . . . . . . . . . 12
⊢
(〈1o, 1o〉 ∈ ({∅} ×
𝐴) → 1o
∈ {∅}) | 
| 200 |  | elsni 4642 | . . . . . . . . . . . 12
⊢
(1o ∈ {∅} → 1o =
∅) | 
| 201 | 199, 200 | syl 17 | . . . . . . . . . . 11
⊢
(〈1o, 1o〉 ∈ ({∅} ×
𝐴) → 1o =
∅) | 
| 202 | 198, 201 | mto 197 | . . . . . . . . . 10
⊢  ¬
〈1o, 1o〉 ∈ ({∅} × 𝐴) | 
| 203 |  | 1onn 8679 | . . . . . . . . . . . 12
⊢
1o ∈ ω | 
| 204 |  | nnord 7896 | . . . . . . . . . . . 12
⊢
(1o ∈ ω → Ord 1o) | 
| 205 |  | ordirr 6401 | . . . . . . . . . . . 12
⊢ (Ord
1o → ¬ 1o ∈ 1o) | 
| 206 | 203, 204,
205 | mp2b 10 | . . . . . . . . . . 11
⊢  ¬
1o ∈ 1o | 
| 207 |  | opelxp2 5727 | . . . . . . . . . . 11
⊢
(〈1o, 1o〉 ∈ ({1o}
× 1o) → 1o ∈
1o) | 
| 208 | 206, 207 | mto 197 | . . . . . . . . . 10
⊢  ¬
〈1o, 1o〉 ∈ ({1o} ×
1o) | 
| 209 | 202, 208 | pm3.2ni 880 | . . . . . . . . 9
⊢  ¬
(〈1o, 1o〉 ∈ ({∅} × 𝐴) ∨ 〈1o,
1o〉 ∈ ({1o} ×
1o)) | 
| 210 |  | elun 4152 | . . . . . . . . 9
⊢
(〈1o, 1o〉 ∈ (({∅} ×
𝐴) ∪ ({1o}
× 1o)) ↔ (〈1o, 1o〉 ∈
({∅} × 𝐴) ∨
〈1o, 1o〉 ∈ ({1o} ×
1o))) | 
| 211 | 209, 210 | mtbir 323 | . . . . . . . 8
⊢  ¬
〈1o, 1o〉 ∈ (({∅} × 𝐴) ∪ ({1o} ×
1o)) | 
| 212 |  | ssnelpss 4113 | . . . . . . . 8
⊢
((({∅} × 𝐴) ∪ ({1o} ×
1o)) ⊆ (({∅} × 𝐴) ∪ ({1o} ×
2o)) → ((〈1o, 1o〉 ∈
(({∅} × 𝐴)
∪ ({1o} × 2o)) ∧ ¬ 〈1o,
1o〉 ∈ (({∅} × 𝐴) ∪ ({1o} ×
1o))) → (({∅} × 𝐴) ∪ ({1o} ×
1o)) ⊊ (({∅} × 𝐴) ∪ ({1o} ×
2o)))) | 
| 213 | 196, 211,
212 | mp2ani 698 | . . . . . . 7
⊢
((({∅} × 𝐴) ∪ ({1o} ×
1o)) ⊆ (({∅} × 𝐴) ∪ ({1o} ×
2o)) → (({∅} × 𝐴) ∪ ({1o} ×
1o)) ⊊ (({∅} × 𝐴) ∪ ({1o} ×
2o))) | 
| 214 | 188, 213 | syl 17 | . . . . . 6
⊢ (𝜑 → (({∅} × 𝐴) ∪ ({1o} ×
1o)) ⊊ (({∅} × 𝐴) ∪ ({1o} ×
2o))) | 
| 215 |  | df-dju 9942 | . . . . . . 7
⊢ (𝐴 ⊔ 1o) =
(({∅} × 𝐴)
∪ ({1o} × 1o)) | 
| 216 |  | df-dju 9942 | . . . . . . 7
⊢ (𝐴 ⊔ 2o) =
(({∅} × 𝐴)
∪ ({1o} × 2o)) | 
| 217 | 215, 216 | psseq12i 4093 | . . . . . 6
⊢ ((𝐴 ⊔ 1o)
⊊ (𝐴 ⊔
2o) ↔ (({∅} × 𝐴) ∪ ({1o} ×
1o)) ⊊ (({∅} × 𝐴) ∪ ({1o} ×
2o))) | 
| 218 | 214, 217 | sylibr 234 | . . . . 5
⊢ (𝜑 → (𝐴 ⊔ 1o) ⊊ (𝐴 ⊔
2o)) | 
| 219 |  | php3 9250 | . . . . 5
⊢ (((𝐴 ⊔ 2o) ∈
Fin ∧ (𝐴 ⊔
1o) ⊊ (𝐴
⊔ 2o)) → (𝐴 ⊔ 1o) ≺ (𝐴 ⊔
2o)) | 
| 220 | 181, 218,
219 | syl2anc 584 | . . . 4
⊢ (𝜑 → (𝐴 ⊔ 1o) ≺ (𝐴 ⊔
2o)) | 
| 221 |  | canthp1lem1 10693 | . . . . 5
⊢
(1o ≺ 𝐴 → (𝐴 ⊔ 2o) ≼ 𝒫
𝐴) | 
| 222 | 1, 221 | syl 17 | . . . 4
⊢ (𝜑 → (𝐴 ⊔ 2o) ≼ 𝒫
𝐴) | 
| 223 |  | sdomdomtr 9151 | . . . 4
⊢ (((𝐴 ⊔ 1o) ≺
(𝐴 ⊔ 2o)
∧ (𝐴 ⊔
2o) ≼ 𝒫 𝐴) → (𝐴 ⊔ 1o) ≺ 𝒫
𝐴) | 
| 224 | 220, 222,
223 | syl2anc 584 | . . 3
⊢ (𝜑 → (𝐴 ⊔ 1o) ≺ 𝒫
𝐴) | 
| 225 |  | sdomnen 9022 | . . 3
⊢ ((𝐴 ⊔ 1o) ≺
𝒫 𝐴 → ¬
(𝐴 ⊔ 1o)
≈ 𝒫 𝐴) | 
| 226 | 224, 225 | syl 17 | . 2
⊢ (𝜑 → ¬ (𝐴 ⊔ 1o) ≈ 𝒫
𝐴) | 
| 227 | 9, 226 | pm2.65i 194 | 1
⊢  ¬
𝜑 |