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

Theorem canthp1lem2 10589
Description: Lemma for canthp1 10590. (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 8890 . . . . . . 7 Rel ≺
32brrelex2i 5689 . . . . . 6 (1o𝐴𝐴 ∈ V)
41, 3syl 17 . . . . 5 (𝜑𝐴 ∈ V)
54pwexd 5334 . . . 4 (𝜑 → 𝒫 𝐴 ∈ V)
6 canthp1lem2.2 . . . 4 (𝜑𝐹:𝒫 𝐴1-1-onto→(𝐴 ⊔ 1o))
7 f1oeng 8911 . . . 4 ((𝒫 𝐴 ∈ V ∧ 𝐹:𝒫 𝐴1-1-onto→(𝐴 ⊔ 1o)) → 𝒫 𝐴 ≈ (𝐴 ⊔ 1o))
85, 6, 7syl2anc 584 . . 3 (𝜑 → 𝒫 𝐴 ≈ (𝐴 ⊔ 1o))
98ensymd 8945 . 2 (𝜑 → (𝐴 ⊔ 1o) ≈ 𝒫 𝐴)
10 canth2g 9075 . . . . . . . . . . 11 (𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴)
114, 10syl 17 . . . . . . . . . 10 (𝜑𝐴 ≺ 𝒫 𝐴)
12 sdomen2 9066 . . . . . . . . . . 11 (𝒫 𝐴 ≈ (𝐴 ⊔ 1o) → (𝐴 ≺ 𝒫 𝐴𝐴 ≺ (𝐴 ⊔ 1o)))
138, 12syl 17 . . . . . . . . . 10 (𝜑 → (𝐴 ≺ 𝒫 𝐴𝐴 ≺ (𝐴 ⊔ 1o)))
1411, 13mpbid 231 . . . . . . . . 9 (𝜑𝐴 ≺ (𝐴 ⊔ 1o))
15 sdomnen 8921 . . . . . . . . 9 (𝐴 ≺ (𝐴 ⊔ 1o) → ¬ 𝐴 ≈ (𝐴 ⊔ 1o))
1614, 15syl 17 . . . . . . . 8 (𝜑 → ¬ 𝐴 ≈ (𝐴 ⊔ 1o))
17 omelon 9582 . . . . . . . . . . . 12 ω ∈ On
18 onenon 9885 . . . . . . . . . . . 12 (ω ∈ On → ω ∈ dom card)
1917, 18ax-mp 5 . . . . . . . . . . 11 ω ∈ dom card
20 canthp1lem2.3 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐺:((𝐴 ⊔ 1o) ∖ {(𝐹𝐴)})–1-1-onto𝐴)
21 dff1o3 6790 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝒫 𝐴1-1-onto→(𝐴 ⊔ 1o) ↔ (𝐹:𝒫 𝐴onto→(𝐴 ⊔ 1o) ∧ Fun 𝐹))
2221simprbi 497 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹:𝒫 𝐴1-1-onto→(𝐴 ⊔ 1o) → Fun 𝐹)
236, 22syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → Fun 𝐹)
24 f1ofo 6791 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝒫 𝐴1-1-onto→(𝐴 ⊔ 1o) → 𝐹:𝒫 𝐴onto→(𝐴 ⊔ 1o))
256, 24syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐹:𝒫 𝐴onto→(𝐴 ⊔ 1o))
26 f1ofn 6785 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝒫 𝐴1-1-onto→(𝐴 ⊔ 1o) → 𝐹 Fn 𝒫 𝐴)
27 fnresdm 6620 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 Fn 𝒫 𝐴 → (𝐹 ↾ 𝒫 𝐴) = 𝐹)
28 foeq1 6752 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ↾ 𝒫 𝐴) = 𝐹 → ((𝐹 ↾ 𝒫 𝐴):𝒫 𝐴onto→(𝐴 ⊔ 1o) ↔ 𝐹:𝒫 𝐴onto→(𝐴 ⊔ 1o)))
296, 26, 27, 284syl 19 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝐹 ↾ 𝒫 𝐴):𝒫 𝐴onto→(𝐴 ⊔ 1o) ↔ 𝐹:𝒫 𝐴onto→(𝐴 ⊔ 1o)))
3025, 29mpbird 256 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐹 ↾ 𝒫 𝐴):𝒫 𝐴onto→(𝐴 ⊔ 1o))
31 fvex 6855 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹𝐴) ∈ V
32 f1osng 6825 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ V ∧ (𝐹𝐴) ∈ V) → {⟨𝐴, (𝐹𝐴)⟩}:{𝐴}–1-1-onto→{(𝐹𝐴)})
334, 31, 32sylancl 586 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → {⟨𝐴, (𝐹𝐴)⟩}:{𝐴}–1-1-onto→{(𝐹𝐴)})
346, 26syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹 Fn 𝒫 𝐴)
35 pwidg 4580 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 ∈ V → 𝐴 ∈ 𝒫 𝐴)
364, 35syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐴 ∈ 𝒫 𝐴)
37 fnressn 7104 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹 Fn 𝒫 𝐴𝐴 ∈ 𝒫 𝐴) → (𝐹 ↾ {𝐴}) = {⟨𝐴, (𝐹𝐴)⟩})
3834, 36, 37syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐹 ↾ {𝐴}) = {⟨𝐴, (𝐹𝐴)⟩})
3938f1oeq1d 6779 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐹 ↾ {𝐴}):{𝐴}–1-1-onto→{(𝐹𝐴)} ↔ {⟨𝐴, (𝐹𝐴)⟩}:{𝐴}–1-1-onto→{(𝐹𝐴)}))
4033, 39mpbird 256 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐹 ↾ {𝐴}):{𝐴}–1-1-onto→{(𝐹𝐴)})
41 f1ofo 6791 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ↾ {𝐴}):{𝐴}–1-1-onto→{(𝐹𝐴)} → (𝐹 ↾ {𝐴}):{𝐴}–onto→{(𝐹𝐴)})
4240, 41syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐹 ↾ {𝐴}):{𝐴}–onto→{(𝐹𝐴)})
43 resdif 6805 . . . . . . . . . . . . . . . . . . . . 21 ((Fun 𝐹 ∧ (𝐹 ↾ 𝒫 𝐴):𝒫 𝐴onto→(𝐴 ⊔ 1o) ∧ (𝐹 ↾ {𝐴}):{𝐴}–onto→{(𝐹𝐴)}) → (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→((𝐴 ⊔ 1o) ∖ {(𝐹𝐴)}))
4423, 30, 42, 43syl3anc 1371 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→((𝐴 ⊔ 1o) ∖ {(𝐹𝐴)}))
45 f1oco 6807 . . . . . . . . . . . . . . . . . . . 20 ((𝐺:((𝐴 ⊔ 1o) ∖ {(𝐹𝐴)})–1-1-onto𝐴 ∧ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→((𝐴 ⊔ 1o) ∖ {(𝐹𝐴)})) → (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴)
4620, 44, 45syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴)
47 resco 6202 . . . . . . . . . . . . . . . . . . . 20 ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) = (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴})))
48 f1oeq1 6772 . . . . . . . . . . . . . . . . . . . 20 (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) = (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴 ↔ (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴))
4947, 48ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴 ↔ (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴)
5046, 49sylibr 233 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴)
51 f1of 6784 . . . . . . . . . . . . . . . . . 18 (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴 → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})⟶𝐴)
5250, 51syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})⟶𝐴)
53 0elpw 5311 . . . . . . . . . . . . . . . . . . . . 21 ∅ ∈ 𝒫 𝐴
5453a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ 𝑥 = 𝐴) → ∅ ∈ 𝒫 𝐴)
55 sdom0 9052 . . . . . . . . . . . . . . . . . . . . . . . 24 ¬ 1o ≺ ∅
56 breq2 5109 . . . . . . . . . . . . . . . . . . . . . . . 24 (∅ = 𝐴 → (1o ≺ ∅ ↔ 1o𝐴))
5755, 56mtbii 325 . . . . . . . . . . . . . . . . . . . . . . 23 (∅ = 𝐴 → ¬ 1o𝐴)
5857necon2ai 2973 . . . . . . . . . . . . . . . . . . . . . 22 (1o𝐴 → ∅ ≠ 𝐴)
591, 58syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∅ ≠ 𝐴)
6059ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ 𝑥 = 𝐴) → ∅ ≠ 𝐴)
61 eldifsn 4747 . . . . . . . . . . . . . . . . . . . 20 (∅ ∈ (𝒫 𝐴 ∖ {𝐴}) ↔ (∅ ∈ 𝒫 𝐴 ∧ ∅ ≠ 𝐴))
6254, 60, 61sylanbrc 583 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ 𝑥 = 𝐴) → ∅ ∈ (𝒫 𝐴 ∖ {𝐴}))
63 simplr 767 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → 𝑥 ∈ 𝒫 𝐴)
64 simpr 485 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → ¬ 𝑥 = 𝐴)
6564neqned 2950 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → 𝑥𝐴)
66 eldifsn 4747 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝐴 ∖ {𝐴}) ↔ (𝑥 ∈ 𝒫 𝐴𝑥𝐴))
6763, 65, 66sylanbrc 583 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → 𝑥 ∈ (𝒫 𝐴 ∖ {𝐴}))
6862, 67ifclda 4521 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ 𝒫 𝐴) → if(𝑥 = 𝐴, ∅, 𝑥) ∈ (𝒫 𝐴 ∖ {𝐴}))
6968fmpttd 7063 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)):𝒫 𝐴⟶(𝒫 𝐴 ∖ {𝐴}))
7052, 69fcod 6694 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))):𝒫 𝐴𝐴)
7169frnd 6676 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ran (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)) ⊆ (𝒫 𝐴 ∖ {𝐴}))
72 cores 6201 . . . . . . . . . . . . . . . . . . 19 (ran (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)) ⊆ (𝒫 𝐴 ∖ {𝐴}) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))) = ((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))))
7371, 72syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))) = ((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))))
74 canthp1lem2.4 . . . . . . . . . . . . . . . . . 18 𝐻 = ((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))
7573, 74eqtr4di 2794 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))) = 𝐻)
7675feq1d 6653 . . . . . . . . . . . . . . . 16 (𝜑 → ((((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))):𝒫 𝐴𝐴𝐻:𝒫 𝐴𝐴))
7770, 76mpbid 231 . . . . . . . . . . . . . . 15 (𝜑𝐻:𝒫 𝐴𝐴)
78 inss1 4188 . . . . . . . . . . . . . . . 16 (𝒫 𝐴 ∩ dom card) ⊆ 𝒫 𝐴
7978a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (𝒫 𝐴 ∩ dom card) ⊆ 𝒫 𝐴)
80 canthp1lem2.5 . . . . . . . . . . . . . . . 16 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 (𝐻‘(𝑟 “ {𝑦})) = 𝑦))}
81 canthp1lem2.6 . . . . . . . . . . . . . . . 16 𝐵 = dom 𝑊
82 eqid 2736 . . . . . . . . . . . . . . . 16 ((𝑊𝐵) “ {(𝐻𝐵)}) = ((𝑊𝐵) “ {(𝐻𝐵)})
8380, 81, 82canth4 10583 . . . . . . . . . . . . . . 15 ((𝐴 ∈ V ∧ 𝐻:𝒫 𝐴𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝒫 𝐴) → (𝐵𝐴 ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ⊊ 𝐵 ∧ (𝐻𝐵) = (𝐻‘((𝑊𝐵) “ {(𝐻𝐵)}))))
844, 77, 79, 83syl3anc 1371 . . . . . . . . . . . . . 14 (𝜑 → (𝐵𝐴 ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ⊊ 𝐵 ∧ (𝐻𝐵) = (𝐻‘((𝑊𝐵) “ {(𝐻𝐵)}))))
8584simp1d 1142 . . . . . . . . . . . . 13 (𝜑𝐵𝐴)
8684simp2d 1143 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑊𝐵) “ {(𝐻𝐵)}) ⊊ 𝐵)
8786pssned 4058 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑊𝐵) “ {(𝐻𝐵)}) ≠ 𝐵)
8887necomd 2999 . . . . . . . . . . . . . . 15 (𝜑𝐵 ≠ ((𝑊𝐵) “ {(𝐻𝐵)}))
8984simp3d 1144 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐻𝐵) = (𝐻‘((𝑊𝐵) “ {(𝐻𝐵)})))
9074fveq1i 6843 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐻𝐵) = (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘𝐵)
9174fveq1i 6843 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐻‘((𝑊𝐵) “ {(𝐻𝐵)})) = (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘((𝑊𝐵) “ {(𝐻𝐵)}))
9289, 90, 913eqtr3g 2799 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘𝐵) = (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘((𝑊𝐵) “ {(𝐻𝐵)})))
934, 85sselpwd 5283 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐵 ∈ 𝒫 𝐴)
9469, 93fvco3d 6941 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘𝐵) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)))
9586pssssd 4057 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑊𝐵) “ {(𝐻𝐵)}) ⊆ 𝐵)
9695, 85sstrd 3954 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝑊𝐵) “ {(𝐻𝐵)}) ⊆ 𝐴)
974, 96sselpwd 5283 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴)
9869, 97fvco3d 6941 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘((𝑊𝐵) “ {(𝐻𝐵)})) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)}))))
9992, 94, 983eqtr3d 2784 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)}))))
10099adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐵𝐴) → ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)}))))
101 eqid 2736 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)) = (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))
102 eqeq1 2740 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝐵 → (𝑥 = 𝐴𝐵 = 𝐴))
103 id 22 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝐵𝑥 = 𝐵)
104102, 103ifbieq2d 4512 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑥 = 𝐵 → if(𝑥 = 𝐴, ∅, 𝑥) = if(𝐵 = 𝐴, ∅, 𝐵))
105 ifcl 4531 . . . . . . . . . . . . . . . . . . . . . . . 24 ((∅ ∈ 𝒫 𝐴𝐵 ∈ 𝒫 𝐴) → if(𝐵 = 𝐴, ∅, 𝐵) ∈ 𝒫 𝐴)
10653, 93, 105sylancr 587 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → if(𝐵 = 𝐴, ∅, 𝐵) ∈ 𝒫 𝐴)
107101, 104, 93, 106fvmptd3 6971 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵) = if(𝐵 = 𝐴, ∅, 𝐵))
108 pssne 4056 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐵𝐴𝐵𝐴)
109108neneqd 2948 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐵𝐴 → ¬ 𝐵 = 𝐴)
110109iffalsed 4497 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵𝐴 → if(𝐵 = 𝐴, ∅, 𝐵) = 𝐵)
111107, 110sylan9eq 2796 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐵𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵) = 𝐵)
112111fveq2d 6846 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐵𝐴) → ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)) = ((𝐺𝐹)‘𝐵))
113 eqeq1 2740 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = ((𝑊𝐵) “ {(𝐻𝐵)}) → (𝑥 = 𝐴 ↔ ((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴))
114 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = ((𝑊𝐵) “ {(𝐻𝐵)}) → 𝑥 = ((𝑊𝐵) “ {(𝐻𝐵)}))
115113, 114ifbieq2d 4512 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = ((𝑊𝐵) “ {(𝐻𝐵)}) → if(𝑥 = 𝐴, ∅, 𝑥) = if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})))
116 ifcl 4531 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((∅ ∈ 𝒫 𝐴 ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴) → if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})) ∈ 𝒫 𝐴)
11753, 97, 116sylancr 587 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})) ∈ 𝒫 𝐴)
118101, 115, 97, 117fvmptd3 6971 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)})) = if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})))
119118adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝐵𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)})) = if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})))
120 sspsstr 4065 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑊𝐵) “ {(𝐻𝐵)}) ⊆ 𝐵𝐵𝐴) → ((𝑊𝐵) “ {(𝐻𝐵)}) ⊊ 𝐴)
12195, 120sylan 580 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝐵𝐴) → ((𝑊𝐵) “ {(𝐻𝐵)}) ⊊ 𝐴)
122121pssned 4058 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝐵𝐴) → ((𝑊𝐵) “ {(𝐻𝐵)}) ≠ 𝐴)
123122neneqd 2948 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝐵𝐴) → ¬ ((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴)
124123iffalsed 4497 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝐵𝐴) → if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})) = ((𝑊𝐵) “ {(𝐻𝐵)}))
125119, 124eqtrd 2776 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐵𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)})) = ((𝑊𝐵) “ {(𝐻𝐵)}))
126125fveq2d 6846 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐵𝐴) → ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)}))) = ((𝐺𝐹)‘((𝑊𝐵) “ {(𝐻𝐵)})))
127100, 112, 1263eqtr3d 2784 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐵𝐴) → ((𝐺𝐹)‘𝐵) = ((𝐺𝐹)‘((𝑊𝐵) “ {(𝐻𝐵)})))
12893, 108anim12i 613 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐵𝐴) → (𝐵 ∈ 𝒫 𝐴𝐵𝐴))
129 eldifsn 4747 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 ∈ (𝒫 𝐴 ∖ {𝐴}) ↔ (𝐵 ∈ 𝒫 𝐴𝐵𝐴))
130128, 129sylibr 233 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐵𝐴) → 𝐵 ∈ (𝒫 𝐴 ∖ {𝐴}))
131130fvresd 6862 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐵𝐴) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = ((𝐺𝐹)‘𝐵))
13297adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐵𝐴) → ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴)
133 eldifsn 4747 . . . . . . . . . . . . . . . . . . . . 21 (((𝑊𝐵) “ {(𝐻𝐵)}) ∈ (𝒫 𝐴 ∖ {𝐴}) ↔ (((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴 ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ≠ 𝐴))
134132, 122, 133sylanbrc 583 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐵𝐴) → ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ (𝒫 𝐴 ∖ {𝐴}))
135134fvresd 6862 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐵𝐴) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘((𝑊𝐵) “ {(𝐻𝐵)})) = ((𝐺𝐹)‘((𝑊𝐵) “ {(𝐻𝐵)})))
136127, 131, 1353eqtr4d 2786 . . . . . . . . . . . . . . . . . 18 ((𝜑𝐵𝐴) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘((𝑊𝐵) “ {(𝐻𝐵)})))
137 f1of1 6783 . . . . . . . . . . . . . . . . . . . . 21 (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴 → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1𝐴)
13850, 137syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1𝐴)
139138adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐵𝐴) → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1𝐴)
140 f1fveq 7209 . . . . . . . . . . . . . . . . . . 19 ((((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1𝐴 ∧ (𝐵 ∈ (𝒫 𝐴 ∖ {𝐴}) ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ (𝒫 𝐴 ∖ {𝐴}))) → ((((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘((𝑊𝐵) “ {(𝐻𝐵)})) ↔ 𝐵 = ((𝑊𝐵) “ {(𝐻𝐵)})))
141139, 130, 134, 140syl12anc 835 . . . . . . . . . . . . . . . . . 18 ((𝜑𝐵𝐴) → ((((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘((𝑊𝐵) “ {(𝐻𝐵)})) ↔ 𝐵 = ((𝑊𝐵) “ {(𝐻𝐵)})))
142136, 141mpbid 231 . . . . . . . . . . . . . . . . 17 ((𝜑𝐵𝐴) → 𝐵 = ((𝑊𝐵) “ {(𝐻𝐵)}))
143142ex 413 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵𝐴𝐵 = ((𝑊𝐵) “ {(𝐻𝐵)})))
144143necon3ad 2956 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 ≠ ((𝑊𝐵) “ {(𝐻𝐵)}) → ¬ 𝐵𝐴))
14588, 144mpd 15 . . . . . . . . . . . . . 14 (𝜑 → ¬ 𝐵𝐴)
146 npss 4070 . . . . . . . . . . . . . 14 𝐵𝐴 ↔ (𝐵𝐴𝐵 = 𝐴))
147145, 146sylib 217 . . . . . . . . . . . . 13 (𝜑 → (𝐵𝐴𝐵 = 𝐴))
14885, 147mpd 15 . . . . . . . . . . . 12 (𝜑𝐵 = 𝐴)
149 eqid 2736 . . . . . . . . . . . . . . . . . . 19 𝐵 = 𝐵
150 eqid 2736 . . . . . . . . . . . . . . . . . . 19 (𝑊𝐵) = (𝑊𝐵)
151149, 150pm3.2i 471 . . . . . . . . . . . . . . . . . 18 (𝐵 = 𝐵 ∧ (𝑊𝐵) = (𝑊𝐵))
152 elinel1 4155 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝐴 ∩ dom card) → 𝑥 ∈ 𝒫 𝐴)
153 ffvelcdm 7032 . . . . . . . . . . . . . . . . . . . 20 ((𝐻:𝒫 𝐴𝐴𝑥 ∈ 𝒫 𝐴) → (𝐻𝑥) ∈ 𝐴)
15477, 152, 153syl2an 596 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑥 ∈ (𝒫 𝐴 ∩ dom card)) → (𝐻𝑥) ∈ 𝐴)
15580, 4, 154, 81fpwwe 10582 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵𝑊(𝑊𝐵) ∧ (𝐻𝐵) ∈ 𝐵) ↔ (𝐵 = 𝐵 ∧ (𝑊𝐵) = (𝑊𝐵))))
156151, 155mpbiri 257 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝑊(𝑊𝐵) ∧ (𝐻𝐵) ∈ 𝐵))
157156simpld 495 . . . . . . . . . . . . . . . 16 (𝜑𝐵𝑊(𝑊𝐵))
15880, 4fpwwelem 10581 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵𝑊(𝑊𝐵) ↔ ((𝐵𝐴 ∧ (𝑊𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊𝐵) We 𝐵 ∧ ∀𝑦𝐵 (𝐻‘((𝑊𝐵) “ {𝑦})) = 𝑦))))
159157, 158mpbid 231 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵𝐴 ∧ (𝑊𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊𝐵) We 𝐵 ∧ ∀𝑦𝐵 (𝐻‘((𝑊𝐵) “ {𝑦})) = 𝑦)))
160159simprld 770 . . . . . . . . . . . . . 14 (𝜑 → (𝑊𝐵) We 𝐵)
161 fvex 6855 . . . . . . . . . . . . . . 15 (𝑊𝐵) ∈ V
162 weeq1 5621 . . . . . . . . . . . . . . 15 (𝑟 = (𝑊𝐵) → (𝑟 We 𝐵 ↔ (𝑊𝐵) We 𝐵))
163161, 162spcev 3565 . . . . . . . . . . . . . 14 ((𝑊𝐵) We 𝐵 → ∃𝑟 𝑟 We 𝐵)
164160, 163syl 17 . . . . . . . . . . . . 13 (𝜑 → ∃𝑟 𝑟 We 𝐵)
165 ween 9971 . . . . . . . . . . . . 13 (𝐵 ∈ dom card ↔ ∃𝑟 𝑟 We 𝐵)
166164, 165sylibr 233 . . . . . . . . . . . 12 (𝜑𝐵 ∈ dom card)
167148, 166eqeltrrd 2839 . . . . . . . . . . 11 (𝜑𝐴 ∈ dom card)
168 domtri2 9925 . . . . . . . . . . 11 ((ω ∈ dom card ∧ 𝐴 ∈ dom card) → (ω ≼ 𝐴 ↔ ¬ 𝐴 ≺ ω))
16919, 167, 168sylancr 587 . . . . . . . . . 10 (𝜑 → (ω ≼ 𝐴 ↔ ¬ 𝐴 ≺ ω))
170 infdju1 10125 . . . . . . . . . 10 (ω ≼ 𝐴 → (𝐴 ⊔ 1o) ≈ 𝐴)
171169, 170syl6bir 253 . . . . . . . . 9 (𝜑 → (¬ 𝐴 ≺ ω → (𝐴 ⊔ 1o) ≈ 𝐴))
172 ensym 8943 . . . . . . . . 9 ((𝐴 ⊔ 1o) ≈ 𝐴𝐴 ≈ (𝐴 ⊔ 1o))
173171, 172syl6 35 . . . . . . . 8 (𝜑 → (¬ 𝐴 ≺ ω → 𝐴 ≈ (𝐴 ⊔ 1o)))
17416, 173mt3d 148 . . . . . . 7 (𝜑𝐴 ≺ ω)
175 2onn 8588 . . . . . . . 8 2o ∈ ω
176 nnsdom 9590 . . . . . . . 8 (2o ∈ ω → 2o ≺ ω)
177175, 176ax-mp 5 . . . . . . 7 2o ≺ ω
178 djufi 10122 . . . . . . 7 ((𝐴 ≺ ω ∧ 2o ≺ ω) → (𝐴 ⊔ 2o) ≺ ω)
179174, 177, 178sylancl 586 . . . . . 6 (𝜑 → (𝐴 ⊔ 2o) ≺ ω)
180 isfinite 9588 . . . . . 6 ((𝐴 ⊔ 2o) ∈ Fin ↔ (𝐴 ⊔ 2o) ≺ ω)
181179, 180sylibr 233 . . . . 5 (𝜑 → (𝐴 ⊔ 2o) ∈ Fin)
182 sssucid 6397 . . . . . . . . . 10 1o ⊆ suc 1o
183 df-2o 8413 . . . . . . . . . 10 2o = suc 1o
184182, 183sseqtrri 3981 . . . . . . . . 9 1o ⊆ 2o
185 xpss2 5653 . . . . . . . . 9 (1o ⊆ 2o → ({1o} × 1o) ⊆ ({1o} × 2o))
186184, 185ax-mp 5 . . . . . . . 8 ({1o} × 1o) ⊆ ({1o} × 2o)
187 unss2 4141 . . . . . . . 8 (({1o} × 1o) ⊆ ({1o} × 2o) → (({∅} × 𝐴) ∪ ({1o} × 1o)) ⊆ (({∅} × 𝐴) ∪ ({1o} × 2o)))
188186, 187mp1i 13 . . . . . . 7 (𝜑 → (({∅} × 𝐴) ∪ ({1o} × 1o)) ⊆ (({∅} × 𝐴) ∪ ({1o} × 2o)))
189 ssun2 4133 . . . . . . . . 9 ({1o} × 2o) ⊆ (({∅} × 𝐴) ∪ ({1o} × 2o))
190 1oex 8422 . . . . . . . . . . 11 1o ∈ V
191190snid 4622 . . . . . . . . . 10 1o ∈ {1o}
192190sucid 6399 . . . . . . . . . . 11 1o ∈ suc 1o
193192, 183eleqtrri 2837 . . . . . . . . . 10 1o ∈ 2o
194 opelxpi 5670 . . . . . . . . . 10 ((1o ∈ {1o} ∧ 1o ∈ 2o) → ⟨1o, 1o⟩ ∈ ({1o} × 2o))
195191, 193, 194mp2an 690 . . . . . . . . 9 ⟨1o, 1o⟩ ∈ ({1o} × 2o)
196189, 195sselii 3941 . . . . . . . 8 ⟨1o, 1o⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 2o))
197 1n0 8434 . . . . . . . . . . . 12 1o ≠ ∅
198197neii 2945 . . . . . . . . . . 11 ¬ 1o = ∅
199 opelxp1 5674 . . . . . . . . . . . 12 (⟨1o, 1o⟩ ∈ ({∅} × 𝐴) → 1o ∈ {∅})
200 elsni 4603 . . . . . . . . . . . 12 (1o ∈ {∅} → 1o = ∅)
201199, 200syl 17 . . . . . . . . . . 11 (⟨1o, 1o⟩ ∈ ({∅} × 𝐴) → 1o = ∅)
202198, 201mto 196 . . . . . . . . . 10 ¬ ⟨1o, 1o⟩ ∈ ({∅} × 𝐴)
203 1onn 8586 . . . . . . . . . . . 12 1o ∈ ω
204 nnord 7810 . . . . . . . . . . . 12 (1o ∈ ω → Ord 1o)
205 ordirr 6335 . . . . . . . . . . . 12 (Ord 1o → ¬ 1o ∈ 1o)
206203, 204, 205mp2b 10 . . . . . . . . . . 11 ¬ 1o ∈ 1o
207 opelxp2 5675 . . . . . . . . . . 11 (⟨1o, 1o⟩ ∈ ({1o} × 1o) → 1o ∈ 1o)
208206, 207mto 196 . . . . . . . . . 10 ¬ ⟨1o, 1o⟩ ∈ ({1o} × 1o)
209202, 208pm3.2ni 879 . . . . . . . . 9 ¬ (⟨1o, 1o⟩ ∈ ({∅} × 𝐴) ∨ ⟨1o, 1o⟩ ∈ ({1o} × 1o))
210 elun 4108 . . . . . . . . 9 (⟨1o, 1o⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 1o)) ↔ (⟨1o, 1o⟩ ∈ ({∅} × 𝐴) ∨ ⟨1o, 1o⟩ ∈ ({1o} × 1o)))
211209, 210mtbir 322 . . . . . . . 8 ¬ ⟨1o, 1o⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 1o))
212 ssnelpss 4071 . . . . . . . 8 ((({∅} × 𝐴) ∪ ({1o} × 1o)) ⊆ (({∅} × 𝐴) ∪ ({1o} × 2o)) → ((⟨1o, 1o⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 2o)) ∧ ¬ ⟨1o, 1o⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 1o))) → (({∅} × 𝐴) ∪ ({1o} × 1o)) ⊊ (({∅} × 𝐴) ∪ ({1o} × 2o))))
213196, 211, 212mp2ani 696 . . . . . . 7 ((({∅} × 𝐴) ∪ ({1o} × 1o)) ⊆ (({∅} × 𝐴) ∪ ({1o} × 2o)) → (({∅} × 𝐴) ∪ ({1o} × 1o)) ⊊ (({∅} × 𝐴) ∪ ({1o} × 2o)))
214188, 213syl 17 . . . . . 6 (𝜑 → (({∅} × 𝐴) ∪ ({1o} × 1o)) ⊊ (({∅} × 𝐴) ∪ ({1o} × 2o)))
215 df-dju 9837 . . . . . . 7 (𝐴 ⊔ 1o) = (({∅} × 𝐴) ∪ ({1o} × 1o))
216 df-dju 9837 . . . . . . 7 (𝐴 ⊔ 2o) = (({∅} × 𝐴) ∪ ({1o} × 2o))
217215, 216psseq12i 4051 . . . . . 6 ((𝐴 ⊔ 1o) ⊊ (𝐴 ⊔ 2o) ↔ (({∅} × 𝐴) ∪ ({1o} × 1o)) ⊊ (({∅} × 𝐴) ∪ ({1o} × 2o)))
218214, 217sylibr 233 . . . . 5 (𝜑 → (𝐴 ⊔ 1o) ⊊ (𝐴 ⊔ 2o))
219 php3 9156 . . . . 5 (((𝐴 ⊔ 2o) ∈ Fin ∧ (𝐴 ⊔ 1o) ⊊ (𝐴 ⊔ 2o)) → (𝐴 ⊔ 1o) ≺ (𝐴 ⊔ 2o))
220181, 218, 219syl2anc 584 . . . 4 (𝜑 → (𝐴 ⊔ 1o) ≺ (𝐴 ⊔ 2o))
221 canthp1lem1 10588 . . . . 5 (1o𝐴 → (𝐴 ⊔ 2o) ≼ 𝒫 𝐴)
2221, 221syl 17 . . . 4 (𝜑 → (𝐴 ⊔ 2o) ≼ 𝒫 𝐴)
223 sdomdomtr 9054 . . . 4 (((𝐴 ⊔ 1o) ≺ (𝐴 ⊔ 2o) ∧ (𝐴 ⊔ 2o) ≼ 𝒫 𝐴) → (𝐴 ⊔ 1o) ≺ 𝒫 𝐴)
224220, 222, 223syl2anc 584 . . 3 (𝜑 → (𝐴 ⊔ 1o) ≺ 𝒫 𝐴)
225 sdomnen 8921 . . 3 ((𝐴 ⊔ 1o) ≺ 𝒫 𝐴 → ¬ (𝐴 ⊔ 1o) ≈ 𝒫 𝐴)
226224, 225syl 17 . 2 (𝜑 → ¬ (𝐴 ⊔ 1o) ≈ 𝒫 𝐴)
2279, 226pm2.65i 193 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  w3a 1087   = wceq 1541  wex 1781  wcel 2106  wne 2943  wral 3064  Vcvv 3445  cdif 3907  cun 3908  cin 3909  wss 3910  wpss 3911  c0 4282  ifcif 4486  𝒫 cpw 4560  {csn 4586  cop 4592   cuni 4865   class class class wbr 5105  {copab 5167  cmpt 5188   We wwe 5587   × cxp 5631  ccnv 5632  dom cdm 5633  ran crn 5634  cres 5635  cima 5636  ccom 5637  Ord word 6316  Oncon0 6317  suc csuc 6319  Fun wfun 6490   Fn wfn 6491  wf 6492  1-1wf1 6493  ontowfo 6494  1-1-ontowf1o 6495  cfv 6496  ωcom 7802  1oc1o 8405  2oc2o 8406  cen 8880  cdom 8881  csdm 8882  Fincfn 8883  cdju 9834  cardccrd 9871
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-er 8648  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-oi 9446  df-dju 9837  df-card 9875
This theorem is referenced by:  canthp1  10590
  Copyright terms: Public domain W3C validator