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

Theorem canthp1lem2 9687
Description: Lemma for canthp1 9688. (Contributed by Mario Carneiro, 18-May-2015.)
Hypotheses
Ref Expression
canthp1lem2.1 (𝜑 → 1𝑜𝐴)
canthp1lem2.2 (𝜑𝐹:𝒫 𝐴1-1-onto→(𝐴 +𝑐 1𝑜))
canthp1lem2.3 (𝜑𝐺:((𝐴 +𝑐 1𝑜) ∖ {(𝐹𝐴)})–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 (𝜑 → 1𝑜𝐴)
2 relsdom 8130 . . . . . . 7 Rel ≺
32brrelex2i 5316 . . . . . 6 (1𝑜𝐴𝐴 ∈ V)
41, 3syl 17 . . . . 5 (𝜑𝐴 ∈ V)
5 pwexg 4999 . . . . 5 (𝐴 ∈ V → 𝒫 𝐴 ∈ V)
64, 5syl 17 . . . 4 (𝜑 → 𝒫 𝐴 ∈ V)
7 canthp1lem2.2 . . . 4 (𝜑𝐹:𝒫 𝐴1-1-onto→(𝐴 +𝑐 1𝑜))
8 f1oeng 8142 . . . 4 ((𝒫 𝐴 ∈ V ∧ 𝐹:𝒫 𝐴1-1-onto→(𝐴 +𝑐 1𝑜)) → 𝒫 𝐴 ≈ (𝐴 +𝑐 1𝑜))
96, 7, 8syl2anc 696 . . 3 (𝜑 → 𝒫 𝐴 ≈ (𝐴 +𝑐 1𝑜))
10 ensym 8172 . . 3 (𝒫 𝐴 ≈ (𝐴 +𝑐 1𝑜) → (𝐴 +𝑐 1𝑜) ≈ 𝒫 𝐴)
119, 10syl 17 . 2 (𝜑 → (𝐴 +𝑐 1𝑜) ≈ 𝒫 𝐴)
12 canth2g 8281 . . . . . . . . . . 11 (𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴)
134, 12syl 17 . . . . . . . . . 10 (𝜑𝐴 ≺ 𝒫 𝐴)
14 sdomen2 8272 . . . . . . . . . . 11 (𝒫 𝐴 ≈ (𝐴 +𝑐 1𝑜) → (𝐴 ≺ 𝒫 𝐴𝐴 ≺ (𝐴 +𝑐 1𝑜)))
159, 14syl 17 . . . . . . . . . 10 (𝜑 → (𝐴 ≺ 𝒫 𝐴𝐴 ≺ (𝐴 +𝑐 1𝑜)))
1613, 15mpbid 222 . . . . . . . . 9 (𝜑𝐴 ≺ (𝐴 +𝑐 1𝑜))
17 sdomnen 8152 . . . . . . . . 9 (𝐴 ≺ (𝐴 +𝑐 1𝑜) → ¬ 𝐴 ≈ (𝐴 +𝑐 1𝑜))
1816, 17syl 17 . . . . . . . 8 (𝜑 → ¬ 𝐴 ≈ (𝐴 +𝑐 1𝑜))
19 omelon 8718 . . . . . . . . . . . 12 ω ∈ On
20 onenon 8985 . . . . . . . . . . . 12 (ω ∈ On → ω ∈ dom card)
2119, 20ax-mp 5 . . . . . . . . . . 11 ω ∈ dom card
22 canthp1lem2.3 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐺:((𝐴 +𝑐 1𝑜) ∖ {(𝐹𝐴)})–1-1-onto𝐴)
23 dff1o3 6305 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝒫 𝐴1-1-onto→(𝐴 +𝑐 1𝑜) ↔ (𝐹:𝒫 𝐴onto→(𝐴 +𝑐 1𝑜) ∧ Fun 𝐹))
2423simprbi 483 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹:𝒫 𝐴1-1-onto→(𝐴 +𝑐 1𝑜) → Fun 𝐹)
257, 24syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → Fun 𝐹)
26 f1ofo 6306 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝒫 𝐴1-1-onto→(𝐴 +𝑐 1𝑜) → 𝐹:𝒫 𝐴onto→(𝐴 +𝑐 1𝑜))
277, 26syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐹:𝒫 𝐴onto→(𝐴 +𝑐 1𝑜))
28 f1ofn 6300 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝒫 𝐴1-1-onto→(𝐴 +𝑐 1𝑜) → 𝐹 Fn 𝒫 𝐴)
29 fnresdm 6161 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 Fn 𝒫 𝐴 → (𝐹 ↾ 𝒫 𝐴) = 𝐹)
30 foeq1 6273 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ↾ 𝒫 𝐴) = 𝐹 → ((𝐹 ↾ 𝒫 𝐴):𝒫 𝐴onto→(𝐴 +𝑐 1𝑜) ↔ 𝐹:𝒫 𝐴onto→(𝐴 +𝑐 1𝑜)))
317, 28, 29, 304syl 19 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝐹 ↾ 𝒫 𝐴):𝒫 𝐴onto→(𝐴 +𝑐 1𝑜) ↔ 𝐹:𝒫 𝐴onto→(𝐴 +𝑐 1𝑜)))
3227, 31mpbird 247 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐹 ↾ 𝒫 𝐴):𝒫 𝐴onto→(𝐴 +𝑐 1𝑜))
33 fvex 6363 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹𝐴) ∈ V
34 f1osng 6339 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ V ∧ (𝐹𝐴) ∈ V) → {⟨𝐴, (𝐹𝐴)⟩}:{𝐴}–1-1-onto→{(𝐹𝐴)})
354, 33, 34sylancl 697 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → {⟨𝐴, (𝐹𝐴)⟩}:{𝐴}–1-1-onto→{(𝐹𝐴)})
367, 28syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹 Fn 𝒫 𝐴)
37 pwidg 4317 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 ∈ V → 𝐴 ∈ 𝒫 𝐴)
384, 37syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐴 ∈ 𝒫 𝐴)
39 fnressn 6589 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹 Fn 𝒫 𝐴𝐴 ∈ 𝒫 𝐴) → (𝐹 ↾ {𝐴}) = {⟨𝐴, (𝐹𝐴)⟩})
4036, 38, 39syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐹 ↾ {𝐴}) = {⟨𝐴, (𝐹𝐴)⟩})
41 f1oeq1 6289 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 ↾ {𝐴}) = {⟨𝐴, (𝐹𝐴)⟩} → ((𝐹 ↾ {𝐴}):{𝐴}–1-1-onto→{(𝐹𝐴)} ↔ {⟨𝐴, (𝐹𝐴)⟩}:{𝐴}–1-1-onto→{(𝐹𝐴)}))
4240, 41syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐹 ↾ {𝐴}):{𝐴}–1-1-onto→{(𝐹𝐴)} ↔ {⟨𝐴, (𝐹𝐴)⟩}:{𝐴}–1-1-onto→{(𝐹𝐴)}))
4335, 42mpbird 247 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐹 ↾ {𝐴}):{𝐴}–1-1-onto→{(𝐹𝐴)})
44 f1ofo 6306 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ↾ {𝐴}):{𝐴}–1-1-onto→{(𝐹𝐴)} → (𝐹 ↾ {𝐴}):{𝐴}–onto→{(𝐹𝐴)})
4543, 44syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐹 ↾ {𝐴}):{𝐴}–onto→{(𝐹𝐴)})
46 resdif 6319 . . . . . . . . . . . . . . . . . . . . 21 ((Fun 𝐹 ∧ (𝐹 ↾ 𝒫 𝐴):𝒫 𝐴onto→(𝐴 +𝑐 1𝑜) ∧ (𝐹 ↾ {𝐴}):{𝐴}–onto→{(𝐹𝐴)}) → (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→((𝐴 +𝑐 1𝑜) ∖ {(𝐹𝐴)}))
4725, 32, 45, 46syl3anc 1477 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→((𝐴 +𝑐 1𝑜) ∖ {(𝐹𝐴)}))
48 f1oco 6321 . . . . . . . . . . . . . . . . . . . 20 ((𝐺:((𝐴 +𝑐 1𝑜) ∖ {(𝐹𝐴)})–1-1-onto𝐴 ∧ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→((𝐴 +𝑐 1𝑜) ∖ {(𝐹𝐴)})) → (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴)
4922, 47, 48syl2anc 696 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴)
50 resco 5800 . . . . . . . . . . . . . . . . . . . 20 ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) = (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴})))
51 f1oeq1 6289 . . . . . . . . . . . . . . . . . . . 20 (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) = (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴 ↔ (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴))
5250, 51ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴 ↔ (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴)
5349, 52sylibr 224 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴)
54 f1of 6299 . . . . . . . . . . . . . . . . . 18 (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴 → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})⟶𝐴)
5553, 54syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})⟶𝐴)
56 0elpw 4983 . . . . . . . . . . . . . . . . . . . . 21 ∅ ∈ 𝒫 𝐴
5756a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ 𝑥 = 𝐴) → ∅ ∈ 𝒫 𝐴)
58 sdom0 8259 . . . . . . . . . . . . . . . . . . . . . . . 24 ¬ 1𝑜 ≺ ∅
59 breq2 4808 . . . . . . . . . . . . . . . . . . . . . . . 24 (∅ = 𝐴 → (1𝑜 ≺ ∅ ↔ 1𝑜𝐴))
6058, 59mtbii 315 . . . . . . . . . . . . . . . . . . . . . . 23 (∅ = 𝐴 → ¬ 1𝑜𝐴)
6160necon2ai 2961 . . . . . . . . . . . . . . . . . . . . . 22 (1𝑜𝐴 → ∅ ≠ 𝐴)
621, 61syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∅ ≠ 𝐴)
6362ad2antrr 764 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ 𝑥 = 𝐴) → ∅ ≠ 𝐴)
64 eldifsn 4462 . . . . . . . . . . . . . . . . . . . 20 (∅ ∈ (𝒫 𝐴 ∖ {𝐴}) ↔ (∅ ∈ 𝒫 𝐴 ∧ ∅ ≠ 𝐴))
6557, 63, 64sylanbrc 701 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ 𝑥 = 𝐴) → ∅ ∈ (𝒫 𝐴 ∖ {𝐴}))
66 simplr 809 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → 𝑥 ∈ 𝒫 𝐴)
67 simpr 479 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → ¬ 𝑥 = 𝐴)
6867neqned 2939 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → 𝑥𝐴)
69 eldifsn 4462 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝐴 ∖ {𝐴}) ↔ (𝑥 ∈ 𝒫 𝐴𝑥𝐴))
7066, 68, 69sylanbrc 701 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → 𝑥 ∈ (𝒫 𝐴 ∖ {𝐴}))
7165, 70ifclda 4264 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ 𝒫 𝐴) → if(𝑥 = 𝐴, ∅, 𝑥) ∈ (𝒫 𝐴 ∖ {𝐴}))
72 eqid 2760 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)) = (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))
7371, 72fmptd 6549 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)):𝒫 𝐴⟶(𝒫 𝐴 ∖ {𝐴}))
74 fco 6219 . . . . . . . . . . . . . . . . 17 ((((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})⟶𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)):𝒫 𝐴⟶(𝒫 𝐴 ∖ {𝐴})) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))):𝒫 𝐴𝐴)
7555, 73, 74syl2anc 696 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))):𝒫 𝐴𝐴)
76 frn 6214 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)):𝒫 𝐴⟶(𝒫 𝐴 ∖ {𝐴}) → ran (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)) ⊆ (𝒫 𝐴 ∖ {𝐴}))
7773, 76syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ran (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)) ⊆ (𝒫 𝐴 ∖ {𝐴}))
78 cores 5799 . . . . . . . . . . . . . . . . . . 19 (ran (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)) ⊆ (𝒫 𝐴 ∖ {𝐴}) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))) = ((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))))
7977, 78syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))) = ((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))))
80 canthp1lem2.4 . . . . . . . . . . . . . . . . . 18 𝐻 = ((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))
8179, 80syl6eqr 2812 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))) = 𝐻)
8281feq1d 6191 . . . . . . . . . . . . . . . 16 (𝜑 → ((((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))):𝒫 𝐴𝐴𝐻:𝒫 𝐴𝐴))
8375, 82mpbid 222 . . . . . . . . . . . . . . 15 (𝜑𝐻:𝒫 𝐴𝐴)
84 inss1 3976 . . . . . . . . . . . . . . . 16 (𝒫 𝐴 ∩ dom card) ⊆ 𝒫 𝐴
8584a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (𝒫 𝐴 ∩ dom card) ⊆ 𝒫 𝐴)
86 canthp1lem2.5 . . . . . . . . . . . . . . . 16 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 (𝐻‘(𝑟 “ {𝑦})) = 𝑦))}
87 canthp1lem2.6 . . . . . . . . . . . . . . . 16 𝐵 = dom 𝑊
88 eqid 2760 . . . . . . . . . . . . . . . 16 ((𝑊𝐵) “ {(𝐻𝐵)}) = ((𝑊𝐵) “ {(𝐻𝐵)})
8986, 87, 88canth4 9681 . . . . . . . . . . . . . . 15 ((𝐴 ∈ V ∧ 𝐻:𝒫 𝐴𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝒫 𝐴) → (𝐵𝐴 ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ⊊ 𝐵 ∧ (𝐻𝐵) = (𝐻‘((𝑊𝐵) “ {(𝐻𝐵)}))))
904, 83, 85, 89syl3anc 1477 . . . . . . . . . . . . . 14 (𝜑 → (𝐵𝐴 ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ⊊ 𝐵 ∧ (𝐻𝐵) = (𝐻‘((𝑊𝐵) “ {(𝐻𝐵)}))))
9190simp1d 1137 . . . . . . . . . . . . 13 (𝜑𝐵𝐴)
9290simp2d 1138 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑊𝐵) “ {(𝐻𝐵)}) ⊊ 𝐵)
9392pssned 3847 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑊𝐵) “ {(𝐻𝐵)}) ≠ 𝐵)
9493necomd 2987 . . . . . . . . . . . . . . 15 (𝜑𝐵 ≠ ((𝑊𝐵) “ {(𝐻𝐵)}))
9590simp3d 1139 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐻𝐵) = (𝐻‘((𝑊𝐵) “ {(𝐻𝐵)})))
9680fveq1i 6354 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐻𝐵) = (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘𝐵)
9780fveq1i 6354 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐻‘((𝑊𝐵) “ {(𝐻𝐵)})) = (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘((𝑊𝐵) “ {(𝐻𝐵)}))
9895, 96, 973eqtr3g 2817 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘𝐵) = (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘((𝑊𝐵) “ {(𝐻𝐵)})))
99 elpw2g 4976 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∈ V → (𝐵 ∈ 𝒫 𝐴𝐵𝐴))
1004, 99syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐵 ∈ 𝒫 𝐴𝐵𝐴))
10191, 100mpbird 247 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐵 ∈ 𝒫 𝐴)
102 fvco3 6438 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)):𝒫 𝐴⟶(𝒫 𝐴 ∖ {𝐴}) ∧ 𝐵 ∈ 𝒫 𝐴) → (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘𝐵) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)))
10373, 101, 102syl2anc 696 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘𝐵) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)))
10492pssssd 3846 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑊𝐵) “ {(𝐻𝐵)}) ⊆ 𝐵)
105104, 91sstrd 3754 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝑊𝐵) “ {(𝐻𝐵)}) ⊆ 𝐴)
106 elpw2g 4976 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∈ V → (((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴 ↔ ((𝑊𝐵) “ {(𝐻𝐵)}) ⊆ 𝐴))
1074, 106syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴 ↔ ((𝑊𝐵) “ {(𝐻𝐵)}) ⊆ 𝐴))
108105, 107mpbird 247 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴)
109 fvco3 6438 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)):𝒫 𝐴⟶(𝒫 𝐴 ∖ {𝐴}) ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴) → (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘((𝑊𝐵) “ {(𝐻𝐵)})) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)}))))
11073, 108, 109syl2anc 696 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘((𝑊𝐵) “ {(𝐻𝐵)})) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)}))))
11198, 103, 1103eqtr3d 2802 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)}))))
112111adantr 472 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐵𝐴) → ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)}))))
113 ifcl 4274 . . . . . . . . . . . . . . . . . . . . . . . 24 ((∅ ∈ 𝒫 𝐴𝐵 ∈ 𝒫 𝐴) → if(𝐵 = 𝐴, ∅, 𝐵) ∈ 𝒫 𝐴)
11456, 101, 113sylancr 698 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → if(𝐵 = 𝐴, ∅, 𝐵) ∈ 𝒫 𝐴)
115 eqeq1 2764 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝐵 → (𝑥 = 𝐴𝐵 = 𝐴))
116 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝐵𝑥 = 𝐵)
117115, 116ifbieq2d 4255 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝐵 → if(𝑥 = 𝐴, ∅, 𝑥) = if(𝐵 = 𝐴, ∅, 𝐵))
118117, 72fvmptg 6443 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐵 ∈ 𝒫 𝐴 ∧ if(𝐵 = 𝐴, ∅, 𝐵) ∈ 𝒫 𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵) = if(𝐵 = 𝐴, ∅, 𝐵))
119101, 114, 118syl2anc 696 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵) = if(𝐵 = 𝐴, ∅, 𝐵))
120 pssne 3845 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐵𝐴𝐵𝐴)
121120neneqd 2937 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐵𝐴 → ¬ 𝐵 = 𝐴)
122121iffalsed 4241 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵𝐴 → if(𝐵 = 𝐴, ∅, 𝐵) = 𝐵)
123119, 122sylan9eq 2814 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐵𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵) = 𝐵)
124123fveq2d 6357 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐵𝐴) → ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)) = ((𝐺𝐹)‘𝐵))
125 ifcl 4274 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((∅ ∈ 𝒫 𝐴 ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴) → if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})) ∈ 𝒫 𝐴)
12656, 108, 125sylancr 698 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})) ∈ 𝒫 𝐴)
127 eqeq1 2764 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = ((𝑊𝐵) “ {(𝐻𝐵)}) → (𝑥 = 𝐴 ↔ ((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴))
128 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = ((𝑊𝐵) “ {(𝐻𝐵)}) → 𝑥 = ((𝑊𝐵) “ {(𝐻𝐵)}))
129127, 128ifbieq2d 4255 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = ((𝑊𝐵) “ {(𝐻𝐵)}) → if(𝑥 = 𝐴, ∅, 𝑥) = if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})))
130129, 72fvmptg 6443 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴 ∧ if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})) ∈ 𝒫 𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)})) = if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})))
131108, 126, 130syl2anc 696 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)})) = if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})))
132131adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝐵𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)})) = if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})))
133 sspsstr 3854 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑊𝐵) “ {(𝐻𝐵)}) ⊆ 𝐵𝐵𝐴) → ((𝑊𝐵) “ {(𝐻𝐵)}) ⊊ 𝐴)
134104, 133sylan 489 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝐵𝐴) → ((𝑊𝐵) “ {(𝐻𝐵)}) ⊊ 𝐴)
135134pssned 3847 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝐵𝐴) → ((𝑊𝐵) “ {(𝐻𝐵)}) ≠ 𝐴)
136135neneqd 2937 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝐵𝐴) → ¬ ((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴)
137136iffalsed 4241 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝐵𝐴) → if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})) = ((𝑊𝐵) “ {(𝐻𝐵)}))
138132, 137eqtrd 2794 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐵𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)})) = ((𝑊𝐵) “ {(𝐻𝐵)}))
139138fveq2d 6357 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐵𝐴) → ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)}))) = ((𝐺𝐹)‘((𝑊𝐵) “ {(𝐻𝐵)})))
140112, 124, 1393eqtr3d 2802 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐵𝐴) → ((𝐺𝐹)‘𝐵) = ((𝐺𝐹)‘((𝑊𝐵) “ {(𝐻𝐵)})))
141101, 120anim12i 591 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐵𝐴) → (𝐵 ∈ 𝒫 𝐴𝐵𝐴))
142 eldifsn 4462 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 ∈ (𝒫 𝐴 ∖ {𝐴}) ↔ (𝐵 ∈ 𝒫 𝐴𝐵𝐴))
143141, 142sylibr 224 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐵𝐴) → 𝐵 ∈ (𝒫 𝐴 ∖ {𝐴}))
144 fvres 6369 . . . . . . . . . . . . . . . . . . . 20 (𝐵 ∈ (𝒫 𝐴 ∖ {𝐴}) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = ((𝐺𝐹)‘𝐵))
145143, 144syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐵𝐴) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = ((𝐺𝐹)‘𝐵))
146108adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐵𝐴) → ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴)
147 eldifsn 4462 . . . . . . . . . . . . . . . . . . . . 21 (((𝑊𝐵) “ {(𝐻𝐵)}) ∈ (𝒫 𝐴 ∖ {𝐴}) ↔ (((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴 ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ≠ 𝐴))
148146, 135, 147sylanbrc 701 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐵𝐴) → ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ (𝒫 𝐴 ∖ {𝐴}))
149 fvres 6369 . . . . . . . . . . . . . . . . . . . 20 (((𝑊𝐵) “ {(𝐻𝐵)}) ∈ (𝒫 𝐴 ∖ {𝐴}) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘((𝑊𝐵) “ {(𝐻𝐵)})) = ((𝐺𝐹)‘((𝑊𝐵) “ {(𝐻𝐵)})))
150148, 149syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐵𝐴) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘((𝑊𝐵) “ {(𝐻𝐵)})) = ((𝐺𝐹)‘((𝑊𝐵) “ {(𝐻𝐵)})))
151140, 145, 1503eqtr4d 2804 . . . . . . . . . . . . . . . . . 18 ((𝜑𝐵𝐴) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘((𝑊𝐵) “ {(𝐻𝐵)})))
152 f1of1 6298 . . . . . . . . . . . . . . . . . . . . 21 (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴 → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1𝐴)
15353, 152syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1𝐴)
154153adantr 472 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐵𝐴) → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1𝐴)
155 f1fveq 6683 . . . . . . . . . . . . . . . . . . 19 ((((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1𝐴 ∧ (𝐵 ∈ (𝒫 𝐴 ∖ {𝐴}) ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ (𝒫 𝐴 ∖ {𝐴}))) → ((((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘((𝑊𝐵) “ {(𝐻𝐵)})) ↔ 𝐵 = ((𝑊𝐵) “ {(𝐻𝐵)})))
156154, 143, 148, 155syl12anc 1475 . . . . . . . . . . . . . . . . . 18 ((𝜑𝐵𝐴) → ((((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘((𝑊𝐵) “ {(𝐻𝐵)})) ↔ 𝐵 = ((𝑊𝐵) “ {(𝐻𝐵)})))
157151, 156mpbid 222 . . . . . . . . . . . . . . . . 17 ((𝜑𝐵𝐴) → 𝐵 = ((𝑊𝐵) “ {(𝐻𝐵)}))
158157ex 449 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵𝐴𝐵 = ((𝑊𝐵) “ {(𝐻𝐵)})))
159158necon3ad 2945 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 ≠ ((𝑊𝐵) “ {(𝐻𝐵)}) → ¬ 𝐵𝐴))
16094, 159mpd 15 . . . . . . . . . . . . . 14 (𝜑 → ¬ 𝐵𝐴)
161 npss 3859 . . . . . . . . . . . . . 14 𝐵𝐴 ↔ (𝐵𝐴𝐵 = 𝐴))
162160, 161sylib 208 . . . . . . . . . . . . 13 (𝜑 → (𝐵𝐴𝐵 = 𝐴))
16391, 162mpd 15 . . . . . . . . . . . 12 (𝜑𝐵 = 𝐴)
164 eqid 2760 . . . . . . . . . . . . . . . . . . . 20 𝐵 = 𝐵
165 eqid 2760 . . . . . . . . . . . . . . . . . . . 20 (𝑊𝐵) = (𝑊𝐵)
166164, 165pm3.2i 470 . . . . . . . . . . . . . . . . . . 19 (𝐵 = 𝐵 ∧ (𝑊𝐵) = (𝑊𝐵))
16784sseli 3740 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝐴 ∩ dom card) → 𝑥 ∈ 𝒫 𝐴)
168 ffvelrn 6521 . . . . . . . . . . . . . . . . . . . . 21 ((𝐻:𝒫 𝐴𝐴𝑥 ∈ 𝒫 𝐴) → (𝐻𝑥) ∈ 𝐴)
16983, 167, 168syl2an 495 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (𝒫 𝐴 ∩ dom card)) → (𝐻𝑥) ∈ 𝐴)
17086, 4, 169, 87fpwwe 9680 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐵𝑊(𝑊𝐵) ∧ (𝐻𝐵) ∈ 𝐵) ↔ (𝐵 = 𝐵 ∧ (𝑊𝐵) = (𝑊𝐵))))
171166, 170mpbiri 248 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐵𝑊(𝑊𝐵) ∧ (𝐻𝐵) ∈ 𝐵))
172171simpld 477 . . . . . . . . . . . . . . . . 17 (𝜑𝐵𝑊(𝑊𝐵))
17386, 4fpwwelem 9679 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝑊(𝑊𝐵) ↔ ((𝐵𝐴 ∧ (𝑊𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊𝐵) We 𝐵 ∧ ∀𝑦𝐵 (𝐻‘((𝑊𝐵) “ {𝑦})) = 𝑦))))
174172, 173mpbid 222 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵𝐴 ∧ (𝑊𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊𝐵) We 𝐵 ∧ ∀𝑦𝐵 (𝐻‘((𝑊𝐵) “ {𝑦})) = 𝑦)))
175174simprd 482 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑊𝐵) We 𝐵 ∧ ∀𝑦𝐵 (𝐻‘((𝑊𝐵) “ {𝑦})) = 𝑦))
176175simpld 477 . . . . . . . . . . . . . 14 (𝜑 → (𝑊𝐵) We 𝐵)
177 fvex 6363 . . . . . . . . . . . . . . 15 (𝑊𝐵) ∈ V
178 weeq1 5254 . . . . . . . . . . . . . . 15 (𝑟 = (𝑊𝐵) → (𝑟 We 𝐵 ↔ (𝑊𝐵) We 𝐵))
179177, 178spcev 3440 . . . . . . . . . . . . . 14 ((𝑊𝐵) We 𝐵 → ∃𝑟 𝑟 We 𝐵)
180176, 179syl 17 . . . . . . . . . . . . 13 (𝜑 → ∃𝑟 𝑟 We 𝐵)
181 ween 9068 . . . . . . . . . . . . 13 (𝐵 ∈ dom card ↔ ∃𝑟 𝑟 We 𝐵)
182180, 181sylibr 224 . . . . . . . . . . . 12 (𝜑𝐵 ∈ dom card)
183163, 182eqeltrrd 2840 . . . . . . . . . . 11 (𝜑𝐴 ∈ dom card)
184 domtri2 9025 . . . . . . . . . . 11 ((ω ∈ dom card ∧ 𝐴 ∈ dom card) → (ω ≼ 𝐴 ↔ ¬ 𝐴 ≺ ω))
18521, 183, 184sylancr 698 . . . . . . . . . 10 (𝜑 → (ω ≼ 𝐴 ↔ ¬ 𝐴 ≺ ω))
186 infcda1 9227 . . . . . . . . . 10 (ω ≼ 𝐴 → (𝐴 +𝑐 1𝑜) ≈ 𝐴)
187185, 186syl6bir 244 . . . . . . . . 9 (𝜑 → (¬ 𝐴 ≺ ω → (𝐴 +𝑐 1𝑜) ≈ 𝐴))
188 ensym 8172 . . . . . . . . 9 ((𝐴 +𝑐 1𝑜) ≈ 𝐴𝐴 ≈ (𝐴 +𝑐 1𝑜))
189187, 188syl6 35 . . . . . . . 8 (𝜑 → (¬ 𝐴 ≺ ω → 𝐴 ≈ (𝐴 +𝑐 1𝑜)))
19018, 189mt3d 140 . . . . . . 7 (𝜑𝐴 ≺ ω)
191 2onn 7891 . . . . . . . 8 2𝑜 ∈ ω
192 nnsdom 8726 . . . . . . . 8 (2𝑜 ∈ ω → 2𝑜 ≺ ω)
193191, 192ax-mp 5 . . . . . . 7 2𝑜 ≺ ω
194 cdafi 9224 . . . . . . 7 ((𝐴 ≺ ω ∧ 2𝑜 ≺ ω) → (𝐴 +𝑐 2𝑜) ≺ ω)
195190, 193, 194sylancl 697 . . . . . 6 (𝜑 → (𝐴 +𝑐 2𝑜) ≺ ω)
196 isfinite 8724 . . . . . 6 ((𝐴 +𝑐 2𝑜) ∈ Fin ↔ (𝐴 +𝑐 2𝑜) ≺ ω)
197195, 196sylibr 224 . . . . 5 (𝜑 → (𝐴 +𝑐 2𝑜) ∈ Fin)
198 sssucid 5963 . . . . . . . . . 10 1𝑜 ⊆ suc 1𝑜
199 df-2o 7731 . . . . . . . . . 10 2𝑜 = suc 1𝑜
200198, 199sseqtr4i 3779 . . . . . . . . 9 1𝑜 ⊆ 2𝑜
201 xpss1 5284 . . . . . . . . 9 (1𝑜 ⊆ 2𝑜 → (1𝑜 × {1𝑜}) ⊆ (2𝑜 × {1𝑜}))
202200, 201ax-mp 5 . . . . . . . 8 (1𝑜 × {1𝑜}) ⊆ (2𝑜 × {1𝑜})
203 unss2 3927 . . . . . . . 8 ((1𝑜 × {1𝑜}) ⊆ (2𝑜 × {1𝑜}) → ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})) ⊆ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜})))
204202, 203mp1i 13 . . . . . . 7 (𝜑 → ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})) ⊆ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜})))
205 ssun2 3920 . . . . . . . . 9 (2𝑜 × {1𝑜}) ⊆ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜}))
206 1onn 7890 . . . . . . . . . . . . 13 1𝑜 ∈ ω
207206elexi 3353 . . . . . . . . . . . 12 1𝑜 ∈ V
208207sucid 5965 . . . . . . . . . . 11 1𝑜 ∈ suc 1𝑜
209208, 199eleqtrri 2838 . . . . . . . . . 10 1𝑜 ∈ 2𝑜
210207snid 4353 . . . . . . . . . 10 1𝑜 ∈ {1𝑜}
211 opelxpi 5305 . . . . . . . . . 10 ((1𝑜 ∈ 2𝑜 ∧ 1𝑜 ∈ {1𝑜}) → ⟨1𝑜, 1𝑜⟩ ∈ (2𝑜 × {1𝑜}))
212209, 210, 211mp2an 710 . . . . . . . . 9 ⟨1𝑜, 1𝑜⟩ ∈ (2𝑜 × {1𝑜})
213205, 212sselii 3741 . . . . . . . 8 ⟨1𝑜, 1𝑜⟩ ∈ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜}))
214 1n0 7746 . . . . . . . . . . . 12 1𝑜 ≠ ∅
215214neii 2934 . . . . . . . . . . 11 ¬ 1𝑜 = ∅
216 opelxp2 5308 . . . . . . . . . . . 12 (⟨1𝑜, 1𝑜⟩ ∈ (𝐴 × {∅}) → 1𝑜 ∈ {∅})
217 elsni 4338 . . . . . . . . . . . 12 (1𝑜 ∈ {∅} → 1𝑜 = ∅)
218216, 217syl 17 . . . . . . . . . . 11 (⟨1𝑜, 1𝑜⟩ ∈ (𝐴 × {∅}) → 1𝑜 = ∅)
219215, 218mto 188 . . . . . . . . . 10 ¬ ⟨1𝑜, 1𝑜⟩ ∈ (𝐴 × {∅})
220 nnord 7239 . . . . . . . . . . . 12 (1𝑜 ∈ ω → Ord 1𝑜)
221 ordirr 5902 . . . . . . . . . . . 12 (Ord 1𝑜 → ¬ 1𝑜 ∈ 1𝑜)
222206, 220, 221mp2b 10 . . . . . . . . . . 11 ¬ 1𝑜 ∈ 1𝑜
223 opelxp1 5307 . . . . . . . . . . 11 (⟨1𝑜, 1𝑜⟩ ∈ (1𝑜 × {1𝑜}) → 1𝑜 ∈ 1𝑜)
224222, 223mto 188 . . . . . . . . . 10 ¬ ⟨1𝑜, 1𝑜⟩ ∈ (1𝑜 × {1𝑜})
225219, 224pm3.2ni 935 . . . . . . . . 9 ¬ (⟨1𝑜, 1𝑜⟩ ∈ (𝐴 × {∅}) ∨ ⟨1𝑜, 1𝑜⟩ ∈ (1𝑜 × {1𝑜}))
226 elun 3896 . . . . . . . . 9 (⟨1𝑜, 1𝑜⟩ ∈ ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})) ↔ (⟨1𝑜, 1𝑜⟩ ∈ (𝐴 × {∅}) ∨ ⟨1𝑜, 1𝑜⟩ ∈ (1𝑜 × {1𝑜})))
227225, 226mtbir 312 . . . . . . . 8 ¬ ⟨1𝑜, 1𝑜⟩ ∈ ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜}))
228 ssnelpss 3860 . . . . . . . 8 (((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})) ⊆ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜})) → ((⟨1𝑜, 1𝑜⟩ ∈ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜})) ∧ ¬ ⟨1𝑜, 1𝑜⟩ ∈ ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜}))) → ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})) ⊊ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜}))))
229213, 227, 228mp2ani 716 . . . . . . 7 (((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})) ⊆ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜})) → ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})) ⊊ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜})))
230204, 229syl 17 . . . . . 6 (𝜑 → ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})) ⊊ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜})))
231 cdaval 9204 . . . . . . . 8 ((𝐴 ∈ V ∧ 1𝑜 ∈ ω) → (𝐴 +𝑐 1𝑜) = ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})))
2324, 206, 231sylancl 697 . . . . . . 7 (𝜑 → (𝐴 +𝑐 1𝑜) = ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})))
233 cdaval 9204 . . . . . . . 8 ((𝐴 ∈ V ∧ 2𝑜 ∈ ω) → (𝐴 +𝑐 2𝑜) = ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜})))
2344, 191, 233sylancl 697 . . . . . . 7 (𝜑 → (𝐴 +𝑐 2𝑜) = ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜})))
235232, 234psseq12d 3843 . . . . . 6 (𝜑 → ((𝐴 +𝑐 1𝑜) ⊊ (𝐴 +𝑐 2𝑜) ↔ ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})) ⊊ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜}))))
236230, 235mpbird 247 . . . . 5 (𝜑 → (𝐴 +𝑐 1𝑜) ⊊ (𝐴 +𝑐 2𝑜))
237 php3 8313 . . . . 5 (((𝐴 +𝑐 2𝑜) ∈ Fin ∧ (𝐴 +𝑐 1𝑜) ⊊ (𝐴 +𝑐 2𝑜)) → (𝐴 +𝑐 1𝑜) ≺ (𝐴 +𝑐 2𝑜))
238197, 236, 237syl2anc 696 . . . 4 (𝜑 → (𝐴 +𝑐 1𝑜) ≺ (𝐴 +𝑐 2𝑜))
239 canthp1lem1 9686 . . . . 5 (1𝑜𝐴 → (𝐴 +𝑐 2𝑜) ≼ 𝒫 𝐴)
2401, 239syl 17 . . . 4 (𝜑 → (𝐴 +𝑐 2𝑜) ≼ 𝒫 𝐴)
241 sdomdomtr 8260 . . . 4 (((𝐴 +𝑐 1𝑜) ≺ (𝐴 +𝑐 2𝑜) ∧ (𝐴 +𝑐 2𝑜) ≼ 𝒫 𝐴) → (𝐴 +𝑐 1𝑜) ≺ 𝒫 𝐴)
242238, 240, 241syl2anc 696 . . 3 (𝜑 → (𝐴 +𝑐 1𝑜) ≺ 𝒫 𝐴)
243 sdomnen 8152 . . 3 ((𝐴 +𝑐 1𝑜) ≺ 𝒫 𝐴 → ¬ (𝐴 +𝑐 1𝑜) ≈ 𝒫 𝐴)
244242, 243syl 17 . 2 (𝜑 → ¬ (𝐴 +𝑐 1𝑜) ≈ 𝒫 𝐴)
24511, 244pm2.65i 185 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383  w3a 1072   = wceq 1632  wex 1853  wcel 2139  wne 2932  wral 3050  Vcvv 3340  cdif 3712  cun 3713  cin 3714  wss 3715  wpss 3716  c0 4058  ifcif 4230  𝒫 cpw 4302  {csn 4321  cop 4327   cuni 4588   class class class wbr 4804  {copab 4864  cmpt 4881   We wwe 5224   × cxp 5264  ccnv 5265  dom cdm 5266  ran crn 5267  cres 5268  cima 5269  ccom 5270  Ord word 5883  Oncon0 5884  suc csuc 5886  Fun wfun 6043   Fn wfn 6044  wf 6045  1-1wf1 6046  ontowfo 6047  1-1-ontowf1o 6048  cfv 6049  (class class class)co 6814  ωcom 7231  1𝑜c1o 7723  2𝑜c2o 7724  cen 8120  cdom 8121  csdm 8122  Fincfn 8123  cardccrd 8971   +𝑐 ccda 9201
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-inf2 8713
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6775  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-om 7232  df-1st 7334  df-2nd 7335  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-1o 7730  df-2o 7731  df-oadd 7734  df-er 7913  df-map 8027  df-en 8124  df-dom 8125  df-sdom 8126  df-fin 8127  df-oi 8582  df-card 8975  df-cda 9202
This theorem is referenced by:  canthp1  9688
  Copyright terms: Public domain W3C validator