Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  canthp1lem2 Structured version   Visualization version   GIF version

Theorem canthp1lem2 10073
 Description: Lemma for canthp1 10074. (Contributed by Mario Carneiro, 18-May-2015.)
Hypotheses
Ref Expression
canthp1lem2.1 (𝜑 → 1o𝐴)
canthp1lem2.2 (𝜑𝐹:𝒫 𝐴1-1-onto→(𝐴 ⊔ 1o))
canthp1lem2.3 (𝜑𝐺:((𝐴 ⊔ 1o) ∖ {(𝐹𝐴)})–1-1-onto𝐴)
canthp1lem2.4 𝐻 = ((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))
canthp1lem2.5 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 (𝐻‘(𝑟 “ {𝑦})) = 𝑦))}
canthp1lem2.6 𝐵 = dom 𝑊
Assertion
Ref Expression
canthp1lem2 ¬ 𝜑
Distinct variable groups:   𝑥,𝑟,𝑦,𝐴   𝐵,𝑟,𝑥,𝑦   𝐻,𝑟,𝑥,𝑦   𝜑,𝑟,𝑥,𝑦   𝑊,𝑟,𝑥,𝑦
Allowed substitution hints:   𝐹(𝑥,𝑦,𝑟)   𝐺(𝑥,𝑦,𝑟)

Proof of Theorem canthp1lem2
StepHypRef Expression
1 canthp1lem2.1 . . . . . 6 (𝜑 → 1o𝐴)
2 relsdom 8512 . . . . . . 7 Rel ≺
32brrelex2i 5596 . . . . . 6 (1o𝐴𝐴 ∈ V)
41, 3syl 17 . . . . 5 (𝜑𝐴 ∈ V)
54pwexd 5267 . . . 4 (𝜑 → 𝒫 𝐴 ∈ V)
6 canthp1lem2.2 . . . 4 (𝜑𝐹:𝒫 𝐴1-1-onto→(𝐴 ⊔ 1o))
7 f1oeng 8524 . . . 4 ((𝒫 𝐴 ∈ V ∧ 𝐹:𝒫 𝐴1-1-onto→(𝐴 ⊔ 1o)) → 𝒫 𝐴 ≈ (𝐴 ⊔ 1o))
85, 6, 7syl2anc 587 . . 3 (𝜑 → 𝒫 𝐴 ≈ (𝐴 ⊔ 1o))
98ensymd 8556 . 2 (𝜑 → (𝐴 ⊔ 1o) ≈ 𝒫 𝐴)
10 canth2g 8668 . . . . . . . . . . 11 (𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴)
114, 10syl 17 . . . . . . . . . 10 (𝜑𝐴 ≺ 𝒫 𝐴)
12 sdomen2 8659 . . . . . . . . . . 11 (𝒫 𝐴 ≈ (𝐴 ⊔ 1o) → (𝐴 ≺ 𝒫 𝐴𝐴 ≺ (𝐴 ⊔ 1o)))
138, 12syl 17 . . . . . . . . . 10 (𝜑 → (𝐴 ≺ 𝒫 𝐴𝐴 ≺ (𝐴 ⊔ 1o)))
1411, 13mpbid 235 . . . . . . . . 9 (𝜑𝐴 ≺ (𝐴 ⊔ 1o))
15 sdomnen 8534 . . . . . . . . 9 (𝐴 ≺ (𝐴 ⊔ 1o) → ¬ 𝐴 ≈ (𝐴 ⊔ 1o))
1614, 15syl 17 . . . . . . . 8 (𝜑 → ¬ 𝐴 ≈ (𝐴 ⊔ 1o))
17 omelon 9106 . . . . . . . . . . . 12 ω ∈ On
18 onenon 9375 . . . . . . . . . . . 12 (ω ∈ On → ω ∈ dom card)
1917, 18ax-mp 5 . . . . . . . . . . 11 ω ∈ dom card
20 canthp1lem2.3 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐺:((𝐴 ⊔ 1o) ∖ {(𝐹𝐴)})–1-1-onto𝐴)
21 dff1o3 6612 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝒫 𝐴1-1-onto→(𝐴 ⊔ 1o) ↔ (𝐹:𝒫 𝐴onto→(𝐴 ⊔ 1o) ∧ Fun 𝐹))
2221simprbi 500 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹:𝒫 𝐴1-1-onto→(𝐴 ⊔ 1o) → Fun 𝐹)
236, 22syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → Fun 𝐹)
24 f1ofo 6613 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝒫 𝐴1-1-onto→(𝐴 ⊔ 1o) → 𝐹:𝒫 𝐴onto→(𝐴 ⊔ 1o))
256, 24syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐹:𝒫 𝐴onto→(𝐴 ⊔ 1o))
26 f1ofn 6607 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝒫 𝐴1-1-onto→(𝐴 ⊔ 1o) → 𝐹 Fn 𝒫 𝐴)
27 fnresdm 6455 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 Fn 𝒫 𝐴 → (𝐹 ↾ 𝒫 𝐴) = 𝐹)
28 foeq1 6577 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ↾ 𝒫 𝐴) = 𝐹 → ((𝐹 ↾ 𝒫 𝐴):𝒫 𝐴onto→(𝐴 ⊔ 1o) ↔ 𝐹:𝒫 𝐴onto→(𝐴 ⊔ 1o)))
296, 26, 27, 284syl 19 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝐹 ↾ 𝒫 𝐴):𝒫 𝐴onto→(𝐴 ⊔ 1o) ↔ 𝐹:𝒫 𝐴onto→(𝐴 ⊔ 1o)))
3025, 29mpbird 260 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐹 ↾ 𝒫 𝐴):𝒫 𝐴onto→(𝐴 ⊔ 1o))
31 fvex 6674 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹𝐴) ∈ V
32 f1osng 6646 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ V ∧ (𝐹𝐴) ∈ V) → {⟨𝐴, (𝐹𝐴)⟩}:{𝐴}–1-1-onto→{(𝐹𝐴)})
334, 31, 32sylancl 589 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → {⟨𝐴, (𝐹𝐴)⟩}:{𝐴}–1-1-onto→{(𝐹𝐴)})
346, 26syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹 Fn 𝒫 𝐴)
35 pwidg 4544 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 ∈ V → 𝐴 ∈ 𝒫 𝐴)
364, 35syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐴 ∈ 𝒫 𝐴)
37 fnressn 6911 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹 Fn 𝒫 𝐴𝐴 ∈ 𝒫 𝐴) → (𝐹 ↾ {𝐴}) = {⟨𝐴, (𝐹𝐴)⟩})
3834, 36, 37syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐹 ↾ {𝐴}) = {⟨𝐴, (𝐹𝐴)⟩})
39 f1oeq1 6595 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 ↾ {𝐴}) = {⟨𝐴, (𝐹𝐴)⟩} → ((𝐹 ↾ {𝐴}):{𝐴}–1-1-onto→{(𝐹𝐴)} ↔ {⟨𝐴, (𝐹𝐴)⟩}:{𝐴}–1-1-onto→{(𝐹𝐴)}))
4038, 39syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐹 ↾ {𝐴}):{𝐴}–1-1-onto→{(𝐹𝐴)} ↔ {⟨𝐴, (𝐹𝐴)⟩}:{𝐴}–1-1-onto→{(𝐹𝐴)}))
4133, 40mpbird 260 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐹 ↾ {𝐴}):{𝐴}–1-1-onto→{(𝐹𝐴)})
42 f1ofo 6613 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ↾ {𝐴}):{𝐴}–1-1-onto→{(𝐹𝐴)} → (𝐹 ↾ {𝐴}):{𝐴}–onto→{(𝐹𝐴)})
4341, 42syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐹 ↾ {𝐴}):{𝐴}–onto→{(𝐹𝐴)})
44 resdif 6626 . . . . . . . . . . . . . . . . . . . . 21 ((Fun 𝐹 ∧ (𝐹 ↾ 𝒫 𝐴):𝒫 𝐴onto→(𝐴 ⊔ 1o) ∧ (𝐹 ↾ {𝐴}):{𝐴}–onto→{(𝐹𝐴)}) → (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→((𝐴 ⊔ 1o) ∖ {(𝐹𝐴)}))
4523, 30, 43, 44syl3anc 1368 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→((𝐴 ⊔ 1o) ∖ {(𝐹𝐴)}))
46 f1oco 6628 . . . . . . . . . . . . . . . . . . . 20 ((𝐺:((𝐴 ⊔ 1o) ∖ {(𝐹𝐴)})–1-1-onto𝐴 ∧ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→((𝐴 ⊔ 1o) ∖ {(𝐹𝐴)})) → (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴)
4720, 45, 46syl2anc 587 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴)
48 resco 6090 . . . . . . . . . . . . . . . . . . . 20 ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) = (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴})))
49 f1oeq1 6595 . . . . . . . . . . . . . . . . . . . 20 (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) = (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴 ↔ (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴))
5048, 49ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴 ↔ (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴)
5147, 50sylibr 237 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴)
52 f1of 6606 . . . . . . . . . . . . . . . . . 18 (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴 → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})⟶𝐴)
5351, 52syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})⟶𝐴)
54 0elpw 5243 . . . . . . . . . . . . . . . . . . . . 21 ∅ ∈ 𝒫 𝐴
5554a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ 𝑥 = 𝐴) → ∅ ∈ 𝒫 𝐴)
56 sdom0 8646 . . . . . . . . . . . . . . . . . . . . . . . 24 ¬ 1o ≺ ∅
57 breq2 5056 . . . . . . . . . . . . . . . . . . . . . . . 24 (∅ = 𝐴 → (1o ≺ ∅ ↔ 1o𝐴))
5856, 57mtbii 329 . . . . . . . . . . . . . . . . . . . . . . 23 (∅ = 𝐴 → ¬ 1o𝐴)
5958necon2ai 3043 . . . . . . . . . . . . . . . . . . . . . 22 (1o𝐴 → ∅ ≠ 𝐴)
601, 59syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∅ ≠ 𝐴)
6160ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ 𝑥 = 𝐴) → ∅ ≠ 𝐴)
62 eldifsn 4704 . . . . . . . . . . . . . . . . . . . 20 (∅ ∈ (𝒫 𝐴 ∖ {𝐴}) ↔ (∅ ∈ 𝒫 𝐴 ∧ ∅ ≠ 𝐴))
6355, 61, 62sylanbrc 586 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ 𝑥 = 𝐴) → ∅ ∈ (𝒫 𝐴 ∖ {𝐴}))
64 simplr 768 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → 𝑥 ∈ 𝒫 𝐴)
65 simpr 488 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → ¬ 𝑥 = 𝐴)
6665neqned 3021 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → 𝑥𝐴)
67 eldifsn 4704 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝐴 ∖ {𝐴}) ↔ (𝑥 ∈ 𝒫 𝐴𝑥𝐴))
6864, 66, 67sylanbrc 586 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → 𝑥 ∈ (𝒫 𝐴 ∖ {𝐴}))
6963, 68ifclda 4484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ 𝒫 𝐴) → if(𝑥 = 𝐴, ∅, 𝑥) ∈ (𝒫 𝐴 ∖ {𝐴}))
7069fmpttd 6870 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)):𝒫 𝐴⟶(𝒫 𝐴 ∖ {𝐴}))
71 fco 6521 . . . . . . . . . . . . . . . . 17 ((((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})⟶𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)):𝒫 𝐴⟶(𝒫 𝐴 ∖ {𝐴})) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))):𝒫 𝐴𝐴)
7253, 70, 71syl2anc 587 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))):𝒫 𝐴𝐴)
7370frnd 6510 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ran (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)) ⊆ (𝒫 𝐴 ∖ {𝐴}))
74 cores 6089 . . . . . . . . . . . . . . . . . . 19 (ran (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)) ⊆ (𝒫 𝐴 ∖ {𝐴}) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))) = ((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))))
7573, 74syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))) = ((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))))
76 canthp1lem2.4 . . . . . . . . . . . . . . . . . 18 𝐻 = ((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))
7775, 76eqtr4di 2877 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))) = 𝐻)
7877feq1d 6488 . . . . . . . . . . . . . . . 16 (𝜑 → ((((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))):𝒫 𝐴𝐴𝐻:𝒫 𝐴𝐴))
7972, 78mpbid 235 . . . . . . . . . . . . . . 15 (𝜑𝐻:𝒫 𝐴𝐴)
80 inss1 4190 . . . . . . . . . . . . . . . 16 (𝒫 𝐴 ∩ dom card) ⊆ 𝒫 𝐴
8180a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (𝒫 𝐴 ∩ dom card) ⊆ 𝒫 𝐴)
82 canthp1lem2.5 . . . . . . . . . . . . . . . 16 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 (𝐻‘(𝑟 “ {𝑦})) = 𝑦))}
83 canthp1lem2.6 . . . . . . . . . . . . . . . 16 𝐵 = dom 𝑊
84 eqid 2824 . . . . . . . . . . . . . . . 16 ((𝑊𝐵) “ {(𝐻𝐵)}) = ((𝑊𝐵) “ {(𝐻𝐵)})
8582, 83, 84canth4 10067 . . . . . . . . . . . . . . 15 ((𝐴 ∈ V ∧ 𝐻:𝒫 𝐴𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝒫 𝐴) → (𝐵𝐴 ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ⊊ 𝐵 ∧ (𝐻𝐵) = (𝐻‘((𝑊𝐵) “ {(𝐻𝐵)}))))
864, 79, 81, 85syl3anc 1368 . . . . . . . . . . . . . 14 (𝜑 → (𝐵𝐴 ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ⊊ 𝐵 ∧ (𝐻𝐵) = (𝐻‘((𝑊𝐵) “ {(𝐻𝐵)}))))
8786simp1d 1139 . . . . . . . . . . . . 13 (𝜑𝐵𝐴)
8886simp2d 1140 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑊𝐵) “ {(𝐻𝐵)}) ⊊ 𝐵)
8988pssned 4061 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑊𝐵) “ {(𝐻𝐵)}) ≠ 𝐵)
9089necomd 3069 . . . . . . . . . . . . . . 15 (𝜑𝐵 ≠ ((𝑊𝐵) “ {(𝐻𝐵)}))
9186simp3d 1141 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐻𝐵) = (𝐻‘((𝑊𝐵) “ {(𝐻𝐵)})))
9276fveq1i 6662 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐻𝐵) = (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘𝐵)
9376fveq1i 6662 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐻‘((𝑊𝐵) “ {(𝐻𝐵)})) = (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘((𝑊𝐵) “ {(𝐻𝐵)}))
9491, 92, 933eqtr3g 2882 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘𝐵) = (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘((𝑊𝐵) “ {(𝐻𝐵)})))
954, 87sselpwd 5216 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐵 ∈ 𝒫 𝐴)
96 fvco3 6751 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)):𝒫 𝐴⟶(𝒫 𝐴 ∖ {𝐴}) ∧ 𝐵 ∈ 𝒫 𝐴) → (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘𝐵) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)))
9770, 95, 96syl2anc 587 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘𝐵) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)))
9888pssssd 4060 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑊𝐵) “ {(𝐻𝐵)}) ⊆ 𝐵)
9998, 87sstrd 3963 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝑊𝐵) “ {(𝐻𝐵)}) ⊆ 𝐴)
1004, 99sselpwd 5216 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴)
101 fvco3 6751 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)):𝒫 𝐴⟶(𝒫 𝐴 ∖ {𝐴}) ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴) → (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘((𝑊𝐵) “ {(𝐻𝐵)})) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)}))))
10270, 100, 101syl2anc 587 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘((𝑊𝐵) “ {(𝐻𝐵)})) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)}))))
10394, 97, 1023eqtr3d 2867 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)}))))
104103adantr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐵𝐴) → ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)}))))
105 eqid 2824 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)) = (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))
106 eqeq1 2828 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝐵 → (𝑥 = 𝐴𝐵 = 𝐴))
107 id 22 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝐵𝑥 = 𝐵)
108106, 107ifbieq2d 4475 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝐵 → if(𝑥 = 𝐴, ∅, 𝑥) = if(𝐵 = 𝐴, ∅, 𝐵))
109 ifcl 4494 . . . . . . . . . . . . . . . . . . . . . . . 24 ((∅ ∈ 𝒫 𝐴𝐵 ∈ 𝒫 𝐴) → if(𝐵 = 𝐴, ∅, 𝐵) ∈ 𝒫 𝐴)
11054, 95, 109sylancr 590 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → if(𝐵 = 𝐴, ∅, 𝐵) ∈ 𝒫 𝐴)
111105, 108, 95, 110fvmptd3 6782 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵) = if(𝐵 = 𝐴, ∅, 𝐵))
112 pssne 4059 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐵𝐴𝐵𝐴)
113112neneqd 3019 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐵𝐴 → ¬ 𝐵 = 𝐴)
114113iffalsed 4461 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵𝐴 → if(𝐵 = 𝐴, ∅, 𝐵) = 𝐵)
115111, 114sylan9eq 2879 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐵𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵) = 𝐵)
116115fveq2d 6665 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐵𝐴) → ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)) = ((𝐺𝐹)‘𝐵))
117 eqeq1 2828 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = ((𝑊𝐵) “ {(𝐻𝐵)}) → (𝑥 = 𝐴 ↔ ((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴))
118 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = ((𝑊𝐵) “ {(𝐻𝐵)}) → 𝑥 = ((𝑊𝐵) “ {(𝐻𝐵)}))
119117, 118ifbieq2d 4475 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = ((𝑊𝐵) “ {(𝐻𝐵)}) → if(𝑥 = 𝐴, ∅, 𝑥) = if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})))
120 ifcl 4494 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((∅ ∈ 𝒫 𝐴 ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴) → if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})) ∈ 𝒫 𝐴)
12154, 100, 120sylancr 590 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})) ∈ 𝒫 𝐴)
122105, 119, 100, 121fvmptd3 6782 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)})) = if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})))
123122adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝐵𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)})) = if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})))
124 sspsstr 4068 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑊𝐵) “ {(𝐻𝐵)}) ⊆ 𝐵𝐵𝐴) → ((𝑊𝐵) “ {(𝐻𝐵)}) ⊊ 𝐴)
12598, 124sylan 583 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝐵𝐴) → ((𝑊𝐵) “ {(𝐻𝐵)}) ⊊ 𝐴)
126125pssned 4061 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝐵𝐴) → ((𝑊𝐵) “ {(𝐻𝐵)}) ≠ 𝐴)
127126neneqd 3019 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝐵𝐴) → ¬ ((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴)
128127iffalsed 4461 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝐵𝐴) → if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})) = ((𝑊𝐵) “ {(𝐻𝐵)}))
129123, 128eqtrd 2859 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐵𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)})) = ((𝑊𝐵) “ {(𝐻𝐵)}))
130129fveq2d 6665 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐵𝐴) → ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)}))) = ((𝐺𝐹)‘((𝑊𝐵) “ {(𝐻𝐵)})))
131104, 116, 1303eqtr3d 2867 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐵𝐴) → ((𝐺𝐹)‘𝐵) = ((𝐺𝐹)‘((𝑊𝐵) “ {(𝐻𝐵)})))
13295, 112anim12i 615 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐵𝐴) → (𝐵 ∈ 𝒫 𝐴𝐵𝐴))
133 eldifsn 4704 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 ∈ (𝒫 𝐴 ∖ {𝐴}) ↔ (𝐵 ∈ 𝒫 𝐴𝐵𝐴))
134132, 133sylibr 237 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐵𝐴) → 𝐵 ∈ (𝒫 𝐴 ∖ {𝐴}))
135134fvresd 6681 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐵𝐴) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = ((𝐺𝐹)‘𝐵))
136100adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐵𝐴) → ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴)
137 eldifsn 4704 . . . . . . . . . . . . . . . . . . . . 21 (((𝑊𝐵) “ {(𝐻𝐵)}) ∈ (𝒫 𝐴 ∖ {𝐴}) ↔ (((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴 ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ≠ 𝐴))
138136, 126, 137sylanbrc 586 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐵𝐴) → ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ (𝒫 𝐴 ∖ {𝐴}))
139138fvresd 6681 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐵𝐴) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘((𝑊𝐵) “ {(𝐻𝐵)})) = ((𝐺𝐹)‘((𝑊𝐵) “ {(𝐻𝐵)})))
140131, 135, 1393eqtr4d 2869 . . . . . . . . . . . . . . . . . 18 ((𝜑𝐵𝐴) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘((𝑊𝐵) “ {(𝐻𝐵)})))
141 f1of1 6605 . . . . . . . . . . . . . . . . . . . . 21 (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴 → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1𝐴)
14251, 141syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1𝐴)
143142adantr 484 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐵𝐴) → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1𝐴)
144 f1fveq 7012 . . . . . . . . . . . . . . . . . . 19 ((((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1𝐴 ∧ (𝐵 ∈ (𝒫 𝐴 ∖ {𝐴}) ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ (𝒫 𝐴 ∖ {𝐴}))) → ((((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘((𝑊𝐵) “ {(𝐻𝐵)})) ↔ 𝐵 = ((𝑊𝐵) “ {(𝐻𝐵)})))
145143, 134, 138, 144syl12anc 835 . . . . . . . . . . . . . . . . . 18 ((𝜑𝐵𝐴) → ((((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘((𝑊𝐵) “ {(𝐻𝐵)})) ↔ 𝐵 = ((𝑊𝐵) “ {(𝐻𝐵)})))
146140, 145mpbid 235 . . . . . . . . . . . . . . . . 17 ((𝜑𝐵𝐴) → 𝐵 = ((𝑊𝐵) “ {(𝐻𝐵)}))
147146ex 416 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵𝐴𝐵 = ((𝑊𝐵) “ {(𝐻𝐵)})))
148147necon3ad 3027 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 ≠ ((𝑊𝐵) “ {(𝐻𝐵)}) → ¬ 𝐵𝐴))
14990, 148mpd 15 . . . . . . . . . . . . . 14 (𝜑 → ¬ 𝐵𝐴)
150 npss 4073 . . . . . . . . . . . . . 14 𝐵𝐴 ↔ (𝐵𝐴𝐵 = 𝐴))
151149, 150sylib 221 . . . . . . . . . . . . 13 (𝜑 → (𝐵𝐴𝐵 = 𝐴))
15287, 151mpd 15 . . . . . . . . . . . 12 (𝜑𝐵 = 𝐴)
153 eqid 2824 . . . . . . . . . . . . . . . . . . 19 𝐵 = 𝐵
154 eqid 2824 . . . . . . . . . . . . . . . . . . 19 (𝑊𝐵) = (𝑊𝐵)
155153, 154pm3.2i 474 . . . . . . . . . . . . . . . . . 18 (𝐵 = 𝐵 ∧ (𝑊𝐵) = (𝑊𝐵))
156 elinel1 4157 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝐴 ∩ dom card) → 𝑥 ∈ 𝒫 𝐴)
157 ffvelrn 6840 . . . . . . . . . . . . . . . . . . . 20 ((𝐻:𝒫 𝐴𝐴𝑥 ∈ 𝒫 𝐴) → (𝐻𝑥) ∈ 𝐴)
15879, 156, 157syl2an 598 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝒫 𝐴 ∩ dom card)) → (𝐻𝑥) ∈ 𝐴)
15982, 4, 158, 83fpwwe 10066 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵𝑊(𝑊𝐵) ∧ (𝐻𝐵) ∈ 𝐵) ↔ (𝐵 = 𝐵 ∧ (𝑊𝐵) = (𝑊𝐵))))
160155, 159mpbiri 261 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝑊(𝑊𝐵) ∧ (𝐻𝐵) ∈ 𝐵))
161160simpld 498 . . . . . . . . . . . . . . . 16 (𝜑𝐵𝑊(𝑊𝐵))
16282, 4fpwwelem 10065 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵𝑊(𝑊𝐵) ↔ ((𝐵𝐴 ∧ (𝑊𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊𝐵) We 𝐵 ∧ ∀𝑦𝐵 (𝐻‘((𝑊𝐵) “ {𝑦})) = 𝑦))))
163161, 162mpbid 235 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵𝐴 ∧ (𝑊𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊𝐵) We 𝐵 ∧ ∀𝑦𝐵 (𝐻‘((𝑊𝐵) “ {𝑦})) = 𝑦)))
164163simprld 771 . . . . . . . . . . . . . 14 (𝜑 → (𝑊𝐵) We 𝐵)
165 fvex 6674 . . . . . . . . . . . . . . 15 (𝑊𝐵) ∈ V
166 weeq1 5530 . . . . . . . . . . . . . . 15 (𝑟 = (𝑊𝐵) → (𝑟 We 𝐵 ↔ (𝑊𝐵) We 𝐵))
167165, 166spcev 3593 . . . . . . . . . . . . . 14 ((𝑊𝐵) We 𝐵 → ∃𝑟 𝑟 We 𝐵)
168164, 167syl 17 . . . . . . . . . . . . 13 (𝜑 → ∃𝑟 𝑟 We 𝐵)
169 ween 9459 . . . . . . . . . . . . 13 (𝐵 ∈ dom card ↔ ∃𝑟 𝑟 We 𝐵)
170168, 169sylibr 237 . . . . . . . . . . . 12 (𝜑𝐵 ∈ dom card)
171152, 170eqeltrrd 2917 . . . . . . . . . . 11 (𝜑𝐴 ∈ dom card)
172 domtri2 9415 . . . . . . . . . . 11 ((ω ∈ dom card ∧ 𝐴 ∈ dom card) → (ω ≼ 𝐴 ↔ ¬ 𝐴 ≺ ω))
17319, 171, 172sylancr 590 . . . . . . . . . 10 (𝜑 → (ω ≼ 𝐴 ↔ ¬ 𝐴 ≺ ω))
174 infdju1 9613 . . . . . . . . . 10 (ω ≼ 𝐴 → (𝐴 ⊔ 1o) ≈ 𝐴)
175173, 174syl6bir 257 . . . . . . . . 9 (𝜑 → (¬ 𝐴 ≺ ω → (𝐴 ⊔ 1o) ≈ 𝐴))
176 ensym 8554 . . . . . . . . 9 ((𝐴 ⊔ 1o) ≈ 𝐴𝐴 ≈ (𝐴 ⊔ 1o))
177175, 176syl6 35 . . . . . . . 8 (𝜑 → (¬ 𝐴 ≺ ω → 𝐴 ≈ (𝐴 ⊔ 1o)))
17816, 177mt3d 150 . . . . . . 7 (𝜑𝐴 ≺ ω)
179 2onn 8262 . . . . . . . 8 2o ∈ ω
180 nnsdom 9114 . . . . . . . 8 (2o ∈ ω → 2o ≺ ω)
181179, 180ax-mp 5 . . . . . . 7 2o ≺ ω
182 djufi 9610 . . . . . . 7 ((𝐴 ≺ ω ∧ 2o ≺ ω) → (𝐴 ⊔ 2o) ≺ ω)
183178, 181, 182sylancl 589 . . . . . 6 (𝜑 → (𝐴 ⊔ 2o) ≺ ω)
184 isfinite 9112 . . . . . 6 ((𝐴 ⊔ 2o) ∈ Fin ↔ (𝐴 ⊔ 2o) ≺ ω)
185183, 184sylibr 237 . . . . 5 (𝜑 → (𝐴 ⊔ 2o) ∈ Fin)
186 sssucid 6255 . . . . . . . . . 10 1o ⊆ suc 1o
187 df-2o 8099 . . . . . . . . . 10 2o = suc 1o
188186, 187sseqtrri 3990 . . . . . . . . 9 1o ⊆ 2o
189 xpss2 5562 . . . . . . . . 9 (1o ⊆ 2o → ({1o} × 1o) ⊆ ({1o} × 2o))
190188, 189ax-mp 5 . . . . . . . 8 ({1o} × 1o) ⊆ ({1o} × 2o)
191 unss2 4143 . . . . . . . 8 (({1o} × 1o) ⊆ ({1o} × 2o) → (({∅} × 𝐴) ∪ ({1o} × 1o)) ⊆ (({∅} × 𝐴) ∪ ({1o} × 2o)))
192190, 191mp1i 13 . . . . . . 7 (𝜑 → (({∅} × 𝐴) ∪ ({1o} × 1o)) ⊆ (({∅} × 𝐴) ∪ ({1o} × 2o)))
193 ssun2 4135 . . . . . . . . 9 ({1o} × 2o) ⊆ (({∅} × 𝐴) ∪ ({1o} × 2o))
194 1oex 8106 . . . . . . . . . . 11 1o ∈ V
195194snid 4586 . . . . . . . . . 10 1o ∈ {1o}
196194sucid 6257 . . . . . . . . . . 11 1o ∈ suc 1o
197196, 187eleqtrri 2915 . . . . . . . . . 10 1o ∈ 2o
198 opelxpi 5579 . . . . . . . . . 10 ((1o ∈ {1o} ∧ 1o ∈ 2o) → ⟨1o, 1o⟩ ∈ ({1o} × 2o))
199195, 197, 198mp2an 691 . . . . . . . . 9 ⟨1o, 1o⟩ ∈ ({1o} × 2o)
200193, 199sselii 3950 . . . . . . . 8 ⟨1o, 1o⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 2o))
201 1n0 8115 . . . . . . . . . . . 12 1o ≠ ∅
202201neii 3016 . . . . . . . . . . 11 ¬ 1o = ∅
203 opelxp1 5583 . . . . . . . . . . . 12 (⟨1o, 1o⟩ ∈ ({∅} × 𝐴) → 1o ∈ {∅})
204 elsni 4567 . . . . . . . . . . . 12 (1o ∈ {∅} → 1o = ∅)
205203, 204syl 17 . . . . . . . . . . 11 (⟨1o, 1o⟩ ∈ ({∅} × 𝐴) → 1o = ∅)
206202, 205mto 200 . . . . . . . . . 10 ¬ ⟨1o, 1o⟩ ∈ ({∅} × 𝐴)
207 1onn 8261 . . . . . . . . . . . 12 1o ∈ ω
208 nnord 7582 . . . . . . . . . . . 12 (1o ∈ ω → Ord 1o)
209 ordirr 6196 . . . . . . . . . . . 12 (Ord 1o → ¬ 1o ∈ 1o)
210207, 208, 209mp2b 10 . . . . . . . . . . 11 ¬ 1o ∈ 1o
211 opelxp2 5584 . . . . . . . . . . 11 (⟨1o, 1o⟩ ∈ ({1o} × 1o) → 1o ∈ 1o)
212210, 211mto 200 . . . . . . . . . 10 ¬ ⟨1o, 1o⟩ ∈ ({1o} × 1o)
213206, 212pm3.2ni 878 . . . . . . . . 9 ¬ (⟨1o, 1o⟩ ∈ ({∅} × 𝐴) ∨ ⟨1o, 1o⟩ ∈ ({1o} × 1o))
214 elun 4111 . . . . . . . . 9 (⟨1o, 1o⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 1o)) ↔ (⟨1o, 1o⟩ ∈ ({∅} × 𝐴) ∨ ⟨1o, 1o⟩ ∈ ({1o} × 1o)))
215213, 214mtbir 326 . . . . . . . 8 ¬ ⟨1o, 1o⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 1o))
216 ssnelpss 4074 . . . . . . . 8 ((({∅} × 𝐴) ∪ ({1o} × 1o)) ⊆ (({∅} × 𝐴) ∪ ({1o} × 2o)) → ((⟨1o, 1o⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 2o)) ∧ ¬ ⟨1o, 1o⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 1o))) → (({∅} × 𝐴) ∪ ({1o} × 1o)) ⊊ (({∅} × 𝐴) ∪ ({1o} × 2o))))
217200, 215, 216mp2ani 697 . . . . . . 7 ((({∅} × 𝐴) ∪ ({1o} × 1o)) ⊆ (({∅} × 𝐴) ∪ ({1o} × 2o)) → (({∅} × 𝐴) ∪ ({1o} × 1o)) ⊊ (({∅} × 𝐴) ∪ ({1o} × 2o)))
218192, 217syl 17 . . . . . 6 (𝜑 → (({∅} × 𝐴) ∪ ({1o} × 1o)) ⊊ (({∅} × 𝐴) ∪ ({1o} × 2o)))
219 df-dju 9327 . . . . . . 7 (𝐴 ⊔ 1o) = (({∅} × 𝐴) ∪ ({1o} × 1o))
220 df-dju 9327 . . . . . . 7 (𝐴 ⊔ 2o) = (({∅} × 𝐴) ∪ ({1o} × 2o))
221219, 220psseq12i 4054 . . . . . 6 ((𝐴 ⊔ 1o) ⊊ (𝐴 ⊔ 2o) ↔ (({∅} × 𝐴) ∪ ({1o} × 1o)) ⊊ (({∅} × 𝐴) ∪ ({1o} × 2o)))
222218, 221sylibr 237 . . . . 5 (𝜑 → (𝐴 ⊔ 1o) ⊊ (𝐴 ⊔ 2o))
223 php3 8700 . . . . 5 (((𝐴 ⊔ 2o) ∈ Fin ∧ (𝐴 ⊔ 1o) ⊊ (𝐴 ⊔ 2o)) → (𝐴 ⊔ 1o) ≺ (𝐴 ⊔ 2o))
224185, 222, 223syl2anc 587 . . . 4 (𝜑 → (𝐴 ⊔ 1o) ≺ (𝐴 ⊔ 2o))
225 canthp1lem1 10072 . . . . 5 (1o𝐴 → (𝐴 ⊔ 2o) ≼ 𝒫 𝐴)
2261, 225syl 17 . . . 4 (𝜑 → (𝐴 ⊔ 2o) ≼ 𝒫 𝐴)
227 sdomdomtr 8647 . . . 4 (((𝐴 ⊔ 1o) ≺ (𝐴 ⊔ 2o) ∧ (𝐴 ⊔ 2o) ≼ 𝒫 𝐴) → (𝐴 ⊔ 1o) ≺ 𝒫 𝐴)
228224, 226, 227syl2anc 587 . . 3 (𝜑 → (𝐴 ⊔ 1o) ≺ 𝒫 𝐴)
229 sdomnen 8534 . . 3 ((𝐴 ⊔ 1o) ≺ 𝒫 𝐴 → ¬ (𝐴 ⊔ 1o) ≈ 𝒫 𝐴)
230228, 229syl 17 . 2 (𝜑 → ¬ (𝐴 ⊔ 1o) ≈ 𝒫 𝐴)
2319, 230pm2.65i 197 1 ¬ 𝜑
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2115   ≠ wne 3014  ∀wral 3133  Vcvv 3480   ∖ cdif 3916   ∪ cun 3917   ∩ cin 3918   ⊆ wss 3919   ⊊ wpss 3920  ∅c0 4276  ifcif 4450  𝒫 cpw 4522  {csn 4550  ⟨cop 4556  ∪ cuni 4824   class class class wbr 5052  {copab 5114   ↦ cmpt 5132   We wwe 5500   × cxp 5540  ◡ccnv 5541  dom cdm 5542  ran crn 5543   ↾ cres 5544   “ cima 5545   ∘ ccom 5546  Ord word 6177  Oncon0 6178  suc csuc 6180  Fun wfun 6337   Fn wfn 6338  ⟶wf 6339  –1-1→wf1 6340  –onto→wfo 6341  –1-1-onto→wf1o 6342  ‘cfv 6343  ωcom 7574  1oc1o 8091  2oc2o 8092   ≈ cen 8502   ≼ cdom 8503   ≺ csdm 8504  Fincfn 8505   ⊔ cdju 9324  cardccrd 9361 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455  ax-inf2 9101 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-se 5502  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-isom 6352  df-riota 7107  df-ov 7152  df-oprab 7153  df-mpo 7154  df-om 7575  df-1st 7684  df-2nd 7685  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-2o 8099  df-oadd 8102  df-er 8285  df-map 8404  df-en 8506  df-dom 8507  df-sdom 8508  df-fin 8509  df-oi 8971  df-dju 9327  df-card 9365 This theorem is referenced by:  canthp1  10074
 Copyright terms: Public domain W3C validator