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

Theorem canthp1lem2 9419
Description: Lemma for canthp1 9420. (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 7906 . . . . . . 7 Rel ≺
32brrelex2i 5119 . . . . . 6 (1𝑜𝐴𝐴 ∈ V)
41, 3syl 17 . . . . 5 (𝜑𝐴 ∈ V)
5 pwexg 4810 . . . . 5 (𝐴 ∈ V → 𝒫 𝐴 ∈ V)
64, 5syl 17 . . . 4 (𝜑 → 𝒫 𝐴 ∈ V)
7 canthp1lem2.2 . . . 4 (𝜑𝐹:𝒫 𝐴1-1-onto→(𝐴 +𝑐 1𝑜))
8 f1oeng 7918 . . . 4 ((𝒫 𝐴 ∈ V ∧ 𝐹:𝒫 𝐴1-1-onto→(𝐴 +𝑐 1𝑜)) → 𝒫 𝐴 ≈ (𝐴 +𝑐 1𝑜))
96, 7, 8syl2anc 692 . . 3 (𝜑 → 𝒫 𝐴 ≈ (𝐴 +𝑐 1𝑜))
10 ensym 7949 . . 3 (𝒫 𝐴 ≈ (𝐴 +𝑐 1𝑜) → (𝐴 +𝑐 1𝑜) ≈ 𝒫 𝐴)
119, 10syl 17 . 2 (𝜑 → (𝐴 +𝑐 1𝑜) ≈ 𝒫 𝐴)
12 canth2g 8058 . . . . . . . . . . 11 (𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴)
134, 12syl 17 . . . . . . . . . 10 (𝜑𝐴 ≺ 𝒫 𝐴)
14 sdomen2 8049 . . . . . . . . . . 11 (𝒫 𝐴 ≈ (𝐴 +𝑐 1𝑜) → (𝐴 ≺ 𝒫 𝐴𝐴 ≺ (𝐴 +𝑐 1𝑜)))
159, 14syl 17 . . . . . . . . . 10 (𝜑 → (𝐴 ≺ 𝒫 𝐴𝐴 ≺ (𝐴 +𝑐 1𝑜)))
1613, 15mpbid 222 . . . . . . . . 9 (𝜑𝐴 ≺ (𝐴 +𝑐 1𝑜))
17 sdomnen 7928 . . . . . . . . 9 (𝐴 ≺ (𝐴 +𝑐 1𝑜) → ¬ 𝐴 ≈ (𝐴 +𝑐 1𝑜))
1816, 17syl 17 . . . . . . . 8 (𝜑 → ¬ 𝐴 ≈ (𝐴 +𝑐 1𝑜))
19 omelon 8487 . . . . . . . . . . . 12 ω ∈ On
20 onenon 8719 . . . . . . . . . . . 12 (ω ∈ On → ω ∈ dom card)
2119, 20ax-mp 5 . . . . . . . . . . 11 ω ∈ dom card
22 canthp1lem2.3 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐺:((𝐴 +𝑐 1𝑜) ∖ {(𝐹𝐴)})–1-1-onto𝐴)
23 dff1o3 6100 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝒫 𝐴1-1-onto→(𝐴 +𝑐 1𝑜) ↔ (𝐹:𝒫 𝐴onto→(𝐴 +𝑐 1𝑜) ∧ Fun 𝐹))
2423simprbi 480 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹:𝒫 𝐴1-1-onto→(𝐴 +𝑐 1𝑜) → Fun 𝐹)
257, 24syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → Fun 𝐹)
26 f1ofo 6101 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝒫 𝐴1-1-onto→(𝐴 +𝑐 1𝑜) → 𝐹:𝒫 𝐴onto→(𝐴 +𝑐 1𝑜))
277, 26syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐹:𝒫 𝐴onto→(𝐴 +𝑐 1𝑜))
28 f1ofn 6095 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝒫 𝐴1-1-onto→(𝐴 +𝑐 1𝑜) → 𝐹 Fn 𝒫 𝐴)
29 fnresdm 5958 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 Fn 𝒫 𝐴 → (𝐹 ↾ 𝒫 𝐴) = 𝐹)
30 foeq1 6068 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ↾ 𝒫 𝐴) = 𝐹 → ((𝐹 ↾ 𝒫 𝐴):𝒫 𝐴onto→(𝐴 +𝑐 1𝑜) ↔ 𝐹:𝒫 𝐴onto→(𝐴 +𝑐 1𝑜)))
317, 28, 29, 304syl 19 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝐹 ↾ 𝒫 𝐴):𝒫 𝐴onto→(𝐴 +𝑐 1𝑜) ↔ 𝐹:𝒫 𝐴onto→(𝐴 +𝑐 1𝑜)))
3227, 31mpbird 247 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐹 ↾ 𝒫 𝐴):𝒫 𝐴onto→(𝐴 +𝑐 1𝑜))
33 fvex 6158 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹𝐴) ∈ V
34 f1osng 6134 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ V ∧ (𝐹𝐴) ∈ V) → {⟨𝐴, (𝐹𝐴)⟩}:{𝐴}–1-1-onto→{(𝐹𝐴)})
354, 33, 34sylancl 693 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → {⟨𝐴, (𝐹𝐴)⟩}:{𝐴}–1-1-onto→{(𝐹𝐴)})
367, 28syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹 Fn 𝒫 𝐴)
37 pwidg 4144 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 ∈ V → 𝐴 ∈ 𝒫 𝐴)
384, 37syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐴 ∈ 𝒫 𝐴)
39 fnressn 6379 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹 Fn 𝒫 𝐴𝐴 ∈ 𝒫 𝐴) → (𝐹 ↾ {𝐴}) = {⟨𝐴, (𝐹𝐴)⟩})
4036, 38, 39syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐹 ↾ {𝐴}) = {⟨𝐴, (𝐹𝐴)⟩})
41 f1oeq1 6084 . . . . . . . . . . . . . . . . . . . . . . . 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 6101 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ↾ {𝐴}):{𝐴}–1-1-onto→{(𝐹𝐴)} → (𝐹 ↾ {𝐴}):{𝐴}–onto→{(𝐹𝐴)})
4543, 44syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐹 ↾ {𝐴}):{𝐴}–onto→{(𝐹𝐴)})
46 resdif 6114 . . . . . . . . . . . . . . . . . . . . 21 ((Fun 𝐹 ∧ (𝐹 ↾ 𝒫 𝐴):𝒫 𝐴onto→(𝐴 +𝑐 1𝑜) ∧ (𝐹 ↾ {𝐴}):{𝐴}–onto→{(𝐹𝐴)}) → (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→((𝐴 +𝑐 1𝑜) ∖ {(𝐹𝐴)}))
4725, 32, 45, 46syl3anc 1323 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→((𝐴 +𝑐 1𝑜) ∖ {(𝐹𝐴)}))
48 f1oco 6116 . . . . . . . . . . . . . . . . . . . 20 ((𝐺:((𝐴 +𝑐 1𝑜) ∖ {(𝐹𝐴)})–1-1-onto𝐴 ∧ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→((𝐴 +𝑐 1𝑜) ∖ {(𝐹𝐴)})) → (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴)
4922, 47, 48syl2anc 692 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴)
50 resco 5598 . . . . . . . . . . . . . . . . . . . 20 ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) = (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴})))
51 f1oeq1 6084 . . . . . . . . . . . . . . . . . . . 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 6094 . . . . . . . . . . . . . . . . . 18 (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴 → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})⟶𝐴)
5553, 54syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})⟶𝐴)
56 0elpw 4794 . . . . . . . . . . . . . . . . . . . . 21 ∅ ∈ 𝒫 𝐴
5756a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ 𝑥 = 𝐴) → ∅ ∈ 𝒫 𝐴)
58 sdom0 8036 . . . . . . . . . . . . . . . . . . . . . . . 24 ¬ 1𝑜 ≺ ∅
59 breq2 4617 . . . . . . . . . . . . . . . . . . . . . . . 24 (∅ = 𝐴 → (1𝑜 ≺ ∅ ↔ 1𝑜𝐴))
6058, 59mtbii 316 . . . . . . . . . . . . . . . . . . . . . . 23 (∅ = 𝐴 → ¬ 1𝑜𝐴)
6160necon2ai 2819 . . . . . . . . . . . . . . . . . . . . . 22 (1𝑜𝐴 → ∅ ≠ 𝐴)
621, 61syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∅ ≠ 𝐴)
6362ad2antrr 761 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ 𝑥 = 𝐴) → ∅ ≠ 𝐴)
64 eldifsn 4287 . . . . . . . . . . . . . . . . . . . 20 (∅ ∈ (𝒫 𝐴 ∖ {𝐴}) ↔ (∅ ∈ 𝒫 𝐴 ∧ ∅ ≠ 𝐴))
6557, 63, 64sylanbrc 697 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ 𝑥 = 𝐴) → ∅ ∈ (𝒫 𝐴 ∖ {𝐴}))
66 simplr 791 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → 𝑥 ∈ 𝒫 𝐴)
67 simpr 477 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → ¬ 𝑥 = 𝐴)
6867neqned 2797 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → 𝑥𝐴)
69 eldifsn 4287 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝐴 ∖ {𝐴}) ↔ (𝑥 ∈ 𝒫 𝐴𝑥𝐴))
7066, 68, 69sylanbrc 697 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → 𝑥 ∈ (𝒫 𝐴 ∖ {𝐴}))
7165, 70ifclda 4092 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ 𝒫 𝐴) → if(𝑥 = 𝐴, ∅, 𝑥) ∈ (𝒫 𝐴 ∖ {𝐴}))
72 eqid 2621 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)) = (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))
7371, 72fmptd 6340 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)):𝒫 𝐴⟶(𝒫 𝐴 ∖ {𝐴}))
74 fco 6015 . . . . . . . . . . . . . . . . 17 ((((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})⟶𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)):𝒫 𝐴⟶(𝒫 𝐴 ∖ {𝐴})) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))):𝒫 𝐴𝐴)
7555, 73, 74syl2anc 692 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))):𝒫 𝐴𝐴)
76 frn 6010 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)):𝒫 𝐴⟶(𝒫 𝐴 ∖ {𝐴}) → ran (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)) ⊆ (𝒫 𝐴 ∖ {𝐴}))
7773, 76syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ran (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)) ⊆ (𝒫 𝐴 ∖ {𝐴}))
78 cores 5597 . . . . . . . . . . . . . . . . . . 19 (ran (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)) ⊆ (𝒫 𝐴 ∖ {𝐴}) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))) = ((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))))
7977, 78syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))) = ((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))))
80 canthp1lem2.4 . . . . . . . . . . . . . . . . . 18 𝐻 = ((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))
8179, 80syl6eqr 2673 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))) = 𝐻)
8281feq1d 5987 . . . . . . . . . . . . . . . 16 (𝜑 → ((((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))):𝒫 𝐴𝐴𝐻:𝒫 𝐴𝐴))
8375, 82mpbid 222 . . . . . . . . . . . . . . 15 (𝜑𝐻:𝒫 𝐴𝐴)
84 inss1 3811 . . . . . . . . . . . . . . . 16 (𝒫 𝐴 ∩ dom card) ⊆ 𝒫 𝐴
8584a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (𝒫 𝐴 ∩ dom card) ⊆ 𝒫 𝐴)
86 canthp1lem2.5 . . . . . . . . . . . . . . . 16 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 (𝐻‘(𝑟 “ {𝑦})) = 𝑦))}
87 canthp1lem2.6 . . . . . . . . . . . . . . . 16 𝐵 = dom 𝑊
88 eqid 2621 . . . . . . . . . . . . . . . 16 ((𝑊𝐵) “ {(𝐻𝐵)}) = ((𝑊𝐵) “ {(𝐻𝐵)})
8986, 87, 88canth4 9413 . . . . . . . . . . . . . . 15 ((𝐴 ∈ V ∧ 𝐻:𝒫 𝐴𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝒫 𝐴) → (𝐵𝐴 ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ⊊ 𝐵 ∧ (𝐻𝐵) = (𝐻‘((𝑊𝐵) “ {(𝐻𝐵)}))))
904, 83, 85, 89syl3anc 1323 . . . . . . . . . . . . . 14 (𝜑 → (𝐵𝐴 ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ⊊ 𝐵 ∧ (𝐻𝐵) = (𝐻‘((𝑊𝐵) “ {(𝐻𝐵)}))))
9190simp1d 1071 . . . . . . . . . . . . 13 (𝜑𝐵𝐴)
9290simp2d 1072 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑊𝐵) “ {(𝐻𝐵)}) ⊊ 𝐵)
9392pssned 3683 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑊𝐵) “ {(𝐻𝐵)}) ≠ 𝐵)
9493necomd 2845 . . . . . . . . . . . . . . 15 (𝜑𝐵 ≠ ((𝑊𝐵) “ {(𝐻𝐵)}))
9590simp3d 1073 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐻𝐵) = (𝐻‘((𝑊𝐵) “ {(𝐻𝐵)})))
9680fveq1i 6149 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐻𝐵) = (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘𝐵)
9780fveq1i 6149 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐻‘((𝑊𝐵) “ {(𝐻𝐵)})) = (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘((𝑊𝐵) “ {(𝐻𝐵)}))
9895, 96, 973eqtr3g 2678 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘𝐵) = (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘((𝑊𝐵) “ {(𝐻𝐵)})))
99 elpw2g 4787 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∈ V → (𝐵 ∈ 𝒫 𝐴𝐵𝐴))
1004, 99syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐵 ∈ 𝒫 𝐴𝐵𝐴))
10191, 100mpbird 247 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐵 ∈ 𝒫 𝐴)
102 fvco3 6232 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)):𝒫 𝐴⟶(𝒫 𝐴 ∖ {𝐴}) ∧ 𝐵 ∈ 𝒫 𝐴) → (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘𝐵) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)))
10373, 101, 102syl2anc 692 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘𝐵) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)))
10492pssssd 3682 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑊𝐵) “ {(𝐻𝐵)}) ⊆ 𝐵)
105104, 91sstrd 3593 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝑊𝐵) “ {(𝐻𝐵)}) ⊆ 𝐴)
106 elpw2g 4787 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∈ V → (((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴 ↔ ((𝑊𝐵) “ {(𝐻𝐵)}) ⊆ 𝐴))
1074, 106syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴 ↔ ((𝑊𝐵) “ {(𝐻𝐵)}) ⊆ 𝐴))
108105, 107mpbird 247 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴)
109 fvco3 6232 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)):𝒫 𝐴⟶(𝒫 𝐴 ∖ {𝐴}) ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴) → (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘((𝑊𝐵) “ {(𝐻𝐵)})) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)}))))
11073, 108, 109syl2anc 692 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘((𝑊𝐵) “ {(𝐻𝐵)})) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)}))))
11198, 103, 1103eqtr3d 2663 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)}))))
112111adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐵𝐴) → ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)}))))
113 ifcl 4102 . . . . . . . . . . . . . . . . . . . . . . . 24 ((∅ ∈ 𝒫 𝐴𝐵 ∈ 𝒫 𝐴) → if(𝐵 = 𝐴, ∅, 𝐵) ∈ 𝒫 𝐴)
11456, 101, 113sylancr 694 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → if(𝐵 = 𝐴, ∅, 𝐵) ∈ 𝒫 𝐴)
115 eqeq1 2625 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝐵 → (𝑥 = 𝐴𝐵 = 𝐴))
116 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝐵𝑥 = 𝐵)
117115, 116ifbieq2d 4083 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝐵 → if(𝑥 = 𝐴, ∅, 𝑥) = if(𝐵 = 𝐴, ∅, 𝐵))
118117, 72fvmptg 6237 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐵 ∈ 𝒫 𝐴 ∧ if(𝐵 = 𝐴, ∅, 𝐵) ∈ 𝒫 𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵) = if(𝐵 = 𝐴, ∅, 𝐵))
119101, 114, 118syl2anc 692 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵) = if(𝐵 = 𝐴, ∅, 𝐵))
120 pssne 3681 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐵𝐴𝐵𝐴)
121120neneqd 2795 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐵𝐴 → ¬ 𝐵 = 𝐴)
122121iffalsed 4069 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵𝐴 → if(𝐵 = 𝐴, ∅, 𝐵) = 𝐵)
123119, 122sylan9eq 2675 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐵𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵) = 𝐵)
124123fveq2d 6152 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐵𝐴) → ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)) = ((𝐺𝐹)‘𝐵))
125 ifcl 4102 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((∅ ∈ 𝒫 𝐴 ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴) → if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})) ∈ 𝒫 𝐴)
12656, 108, 125sylancr 694 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})) ∈ 𝒫 𝐴)
127 eqeq1 2625 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = ((𝑊𝐵) “ {(𝐻𝐵)}) → (𝑥 = 𝐴 ↔ ((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴))
128 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = ((𝑊𝐵) “ {(𝐻𝐵)}) → 𝑥 = ((𝑊𝐵) “ {(𝐻𝐵)}))
129127, 128ifbieq2d 4083 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = ((𝑊𝐵) “ {(𝐻𝐵)}) → if(𝑥 = 𝐴, ∅, 𝑥) = if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})))
130129, 72fvmptg 6237 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴 ∧ if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})) ∈ 𝒫 𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)})) = if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})))
131108, 126, 130syl2anc 692 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)})) = if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})))
132131adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝐵𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)})) = if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})))
133 sspsstr 3690 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑊𝐵) “ {(𝐻𝐵)}) ⊆ 𝐵𝐵𝐴) → ((𝑊𝐵) “ {(𝐻𝐵)}) ⊊ 𝐴)
134104, 133sylan 488 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝐵𝐴) → ((𝑊𝐵) “ {(𝐻𝐵)}) ⊊ 𝐴)
135134pssned 3683 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝐵𝐴) → ((𝑊𝐵) “ {(𝐻𝐵)}) ≠ 𝐴)
136135neneqd 2795 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝐵𝐴) → ¬ ((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴)
137136iffalsed 4069 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝐵𝐴) → if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})) = ((𝑊𝐵) “ {(𝐻𝐵)}))
138132, 137eqtrd 2655 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐵𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)})) = ((𝑊𝐵) “ {(𝐻𝐵)}))
139138fveq2d 6152 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐵𝐴) → ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)}))) = ((𝐺𝐹)‘((𝑊𝐵) “ {(𝐻𝐵)})))
140112, 124, 1393eqtr3d 2663 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐵𝐴) → ((𝐺𝐹)‘𝐵) = ((𝐺𝐹)‘((𝑊𝐵) “ {(𝐻𝐵)})))
141101, 120anim12i 589 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐵𝐴) → (𝐵 ∈ 𝒫 𝐴𝐵𝐴))
142 eldifsn 4287 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 ∈ (𝒫 𝐴 ∖ {𝐴}) ↔ (𝐵 ∈ 𝒫 𝐴𝐵𝐴))
143141, 142sylibr 224 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐵𝐴) → 𝐵 ∈ (𝒫 𝐴 ∖ {𝐴}))
144 fvres 6164 . . . . . . . . . . . . . . . . . . . 20 (𝐵 ∈ (𝒫 𝐴 ∖ {𝐴}) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = ((𝐺𝐹)‘𝐵))
145143, 144syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐵𝐴) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = ((𝐺𝐹)‘𝐵))
146108adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐵𝐴) → ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴)
147 eldifsn 4287 . . . . . . . . . . . . . . . . . . . . 21 (((𝑊𝐵) “ {(𝐻𝐵)}) ∈ (𝒫 𝐴 ∖ {𝐴}) ↔ (((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴 ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ≠ 𝐴))
148146, 135, 147sylanbrc 697 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐵𝐴) → ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ (𝒫 𝐴 ∖ {𝐴}))
149 fvres 6164 . . . . . . . . . . . . . . . . . . . 20 (((𝑊𝐵) “ {(𝐻𝐵)}) ∈ (𝒫 𝐴 ∖ {𝐴}) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘((𝑊𝐵) “ {(𝐻𝐵)})) = ((𝐺𝐹)‘((𝑊𝐵) “ {(𝐻𝐵)})))
150148, 149syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐵𝐴) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘((𝑊𝐵) “ {(𝐻𝐵)})) = ((𝐺𝐹)‘((𝑊𝐵) “ {(𝐻𝐵)})))
151140, 145, 1503eqtr4d 2665 . . . . . . . . . . . . . . . . . 18 ((𝜑𝐵𝐴) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘((𝑊𝐵) “ {(𝐻𝐵)})))
152 f1of1 6093 . . . . . . . . . . . . . . . . . . . . 21 (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴 → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1𝐴)
15353, 152syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1𝐴)
154153adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐵𝐴) → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1𝐴)
155 f1fveq 6473 . . . . . . . . . . . . . . . . . . 19 ((((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1𝐴 ∧ (𝐵 ∈ (𝒫 𝐴 ∖ {𝐴}) ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ (𝒫 𝐴 ∖ {𝐴}))) → ((((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘((𝑊𝐵) “ {(𝐻𝐵)})) ↔ 𝐵 = ((𝑊𝐵) “ {(𝐻𝐵)})))
156154, 143, 148, 155syl12anc 1321 . . . . . . . . . . . . . . . . . 18 ((𝜑𝐵𝐴) → ((((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘((𝑊𝐵) “ {(𝐻𝐵)})) ↔ 𝐵 = ((𝑊𝐵) “ {(𝐻𝐵)})))
157151, 156mpbid 222 . . . . . . . . . . . . . . . . 17 ((𝜑𝐵𝐴) → 𝐵 = ((𝑊𝐵) “ {(𝐻𝐵)}))
158157ex 450 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵𝐴𝐵 = ((𝑊𝐵) “ {(𝐻𝐵)})))
159158necon3ad 2803 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 ≠ ((𝑊𝐵) “ {(𝐻𝐵)}) → ¬ 𝐵𝐴))
16094, 159mpd 15 . . . . . . . . . . . . . 14 (𝜑 → ¬ 𝐵𝐴)
161 npss 3695 . . . . . . . . . . . . . 14 𝐵𝐴 ↔ (𝐵𝐴𝐵 = 𝐴))
162160, 161sylib 208 . . . . . . . . . . . . 13 (𝜑 → (𝐵𝐴𝐵 = 𝐴))
16391, 162mpd 15 . . . . . . . . . . . 12 (𝜑𝐵 = 𝐴)
164 eqid 2621 . . . . . . . . . . . . . . . . . . . 20 𝐵 = 𝐵
165 eqid 2621 . . . . . . . . . . . . . . . . . . . 20 (𝑊𝐵) = (𝑊𝐵)
166164, 165pm3.2i 471 . . . . . . . . . . . . . . . . . . 19 (𝐵 = 𝐵 ∧ (𝑊𝐵) = (𝑊𝐵))
16784sseli 3579 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝐴 ∩ dom card) → 𝑥 ∈ 𝒫 𝐴)
168 ffvelrn 6313 . . . . . . . . . . . . . . . . . . . . 21 ((𝐻:𝒫 𝐴𝐴𝑥 ∈ 𝒫 𝐴) → (𝐻𝑥) ∈ 𝐴)
16983, 167, 168syl2an 494 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (𝒫 𝐴 ∩ dom card)) → (𝐻𝑥) ∈ 𝐴)
17086, 4, 169, 87fpwwe 9412 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐵𝑊(𝑊𝐵) ∧ (𝐻𝐵) ∈ 𝐵) ↔ (𝐵 = 𝐵 ∧ (𝑊𝐵) = (𝑊𝐵))))
171166, 170mpbiri 248 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐵𝑊(𝑊𝐵) ∧ (𝐻𝐵) ∈ 𝐵))
172171simpld 475 . . . . . . . . . . . . . . . . 17 (𝜑𝐵𝑊(𝑊𝐵))
17386, 4fpwwelem 9411 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝑊(𝑊𝐵) ↔ ((𝐵𝐴 ∧ (𝑊𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊𝐵) We 𝐵 ∧ ∀𝑦𝐵 (𝐻‘((𝑊𝐵) “ {𝑦})) = 𝑦))))
174172, 173mpbid 222 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵𝐴 ∧ (𝑊𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊𝐵) We 𝐵 ∧ ∀𝑦𝐵 (𝐻‘((𝑊𝐵) “ {𝑦})) = 𝑦)))
175174simprd 479 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑊𝐵) We 𝐵 ∧ ∀𝑦𝐵 (𝐻‘((𝑊𝐵) “ {𝑦})) = 𝑦))
176175simpld 475 . . . . . . . . . . . . . 14 (𝜑 → (𝑊𝐵) We 𝐵)
177 fvex 6158 . . . . . . . . . . . . . . 15 (𝑊𝐵) ∈ V
178 weeq1 5062 . . . . . . . . . . . . . . 15 (𝑟 = (𝑊𝐵) → (𝑟 We 𝐵 ↔ (𝑊𝐵) We 𝐵))
179177, 178spcev 3286 . . . . . . . . . . . . . 14 ((𝑊𝐵) We 𝐵 → ∃𝑟 𝑟 We 𝐵)
180176, 179syl 17 . . . . . . . . . . . . 13 (𝜑 → ∃𝑟 𝑟 We 𝐵)
181 ween 8802 . . . . . . . . . . . . 13 (𝐵 ∈ dom card ↔ ∃𝑟 𝑟 We 𝐵)
182180, 181sylibr 224 . . . . . . . . . . . 12 (𝜑𝐵 ∈ dom card)
183163, 182eqeltrrd 2699 . . . . . . . . . . 11 (𝜑𝐴 ∈ dom card)
184 domtri2 8759 . . . . . . . . . . 11 ((ω ∈ dom card ∧ 𝐴 ∈ dom card) → (ω ≼ 𝐴 ↔ ¬ 𝐴 ≺ ω))
18521, 183, 184sylancr 694 . . . . . . . . . 10 (𝜑 → (ω ≼ 𝐴 ↔ ¬ 𝐴 ≺ ω))
186 infcda1 8959 . . . . . . . . . 10 (ω ≼ 𝐴 → (𝐴 +𝑐 1𝑜) ≈ 𝐴)
187185, 186syl6bir 244 . . . . . . . . 9 (𝜑 → (¬ 𝐴 ≺ ω → (𝐴 +𝑐 1𝑜) ≈ 𝐴))
188 ensym 7949 . . . . . . . . 9 ((𝐴 +𝑐 1𝑜) ≈ 𝐴𝐴 ≈ (𝐴 +𝑐 1𝑜))
189187, 188syl6 35 . . . . . . . 8 (𝜑 → (¬ 𝐴 ≺ ω → 𝐴 ≈ (𝐴 +𝑐 1𝑜)))
19018, 189mt3d 140 . . . . . . 7 (𝜑𝐴 ≺ ω)
191 2onn 7665 . . . . . . . 8 2𝑜 ∈ ω
192 nnsdom 8495 . . . . . . . 8 (2𝑜 ∈ ω → 2𝑜 ≺ ω)
193191, 192ax-mp 5 . . . . . . 7 2𝑜 ≺ ω
194 cdafi 8956 . . . . . . 7 ((𝐴 ≺ ω ∧ 2𝑜 ≺ ω) → (𝐴 +𝑐 2𝑜) ≺ ω)
195190, 193, 194sylancl 693 . . . . . 6 (𝜑 → (𝐴 +𝑐 2𝑜) ≺ ω)
196 isfinite 8493 . . . . . 6 ((𝐴 +𝑐 2𝑜) ∈ Fin ↔ (𝐴 +𝑐 2𝑜) ≺ ω)
197195, 196sylibr 224 . . . . 5 (𝜑 → (𝐴 +𝑐 2𝑜) ∈ Fin)
198 sssucid 5761 . . . . . . . . . 10 1𝑜 ⊆ suc 1𝑜
199 df-2o 7506 . . . . . . . . . 10 2𝑜 = suc 1𝑜
200198, 199sseqtr4i 3617 . . . . . . . . 9 1𝑜 ⊆ 2𝑜
201 xpss1 5189 . . . . . . . . 9 (1𝑜 ⊆ 2𝑜 → (1𝑜 × {1𝑜}) ⊆ (2𝑜 × {1𝑜}))
202200, 201ax-mp 5 . . . . . . . 8 (1𝑜 × {1𝑜}) ⊆ (2𝑜 × {1𝑜})
203 unss2 3762 . . . . . . . 8 ((1𝑜 × {1𝑜}) ⊆ (2𝑜 × {1𝑜}) → ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})) ⊆ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜})))
204202, 203mp1i 13 . . . . . . 7 (𝜑 → ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})) ⊆ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜})))
205 ssun2 3755 . . . . . . . . 9 (2𝑜 × {1𝑜}) ⊆ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜}))
206 1onn 7664 . . . . . . . . . . . . 13 1𝑜 ∈ ω
207206elexi 3199 . . . . . . . . . . . 12 1𝑜 ∈ V
208207sucid 5763 . . . . . . . . . . 11 1𝑜 ∈ suc 1𝑜
209208, 199eleqtrri 2697 . . . . . . . . . 10 1𝑜 ∈ 2𝑜
210207snid 4179 . . . . . . . . . 10 1𝑜 ∈ {1𝑜}
211 opelxpi 5108 . . . . . . . . . 10 ((1𝑜 ∈ 2𝑜 ∧ 1𝑜 ∈ {1𝑜}) → ⟨1𝑜, 1𝑜⟩ ∈ (2𝑜 × {1𝑜}))
212209, 210, 211mp2an 707 . . . . . . . . 9 ⟨1𝑜, 1𝑜⟩ ∈ (2𝑜 × {1𝑜})
213205, 212sselii 3580 . . . . . . . 8 ⟨1𝑜, 1𝑜⟩ ∈ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜}))
214 1n0 7520 . . . . . . . . . . . 12 1𝑜 ≠ ∅
215214neii 2792 . . . . . . . . . . 11 ¬ 1𝑜 = ∅
216 opelxp2 5111 . . . . . . . . . . . 12 (⟨1𝑜, 1𝑜⟩ ∈ (𝐴 × {∅}) → 1𝑜 ∈ {∅})
217 elsni 4165 . . . . . . . . . . . 12 (1𝑜 ∈ {∅} → 1𝑜 = ∅)
218216, 217syl 17 . . . . . . . . . . 11 (⟨1𝑜, 1𝑜⟩ ∈ (𝐴 × {∅}) → 1𝑜 = ∅)
219215, 218mto 188 . . . . . . . . . 10 ¬ ⟨1𝑜, 1𝑜⟩ ∈ (𝐴 × {∅})
220 nnord 7020 . . . . . . . . . . . 12 (1𝑜 ∈ ω → Ord 1𝑜)
221 ordirr 5700 . . . . . . . . . . . 12 (Ord 1𝑜 → ¬ 1𝑜 ∈ 1𝑜)
222206, 220, 221mp2b 10 . . . . . . . . . . 11 ¬ 1𝑜 ∈ 1𝑜
223 opelxp1 5110 . . . . . . . . . . 11 (⟨1𝑜, 1𝑜⟩ ∈ (1𝑜 × {1𝑜}) → 1𝑜 ∈ 1𝑜)
224222, 223mto 188 . . . . . . . . . 10 ¬ ⟨1𝑜, 1𝑜⟩ ∈ (1𝑜 × {1𝑜})
225219, 224pm3.2ni 898 . . . . . . . . 9 ¬ (⟨1𝑜, 1𝑜⟩ ∈ (𝐴 × {∅}) ∨ ⟨1𝑜, 1𝑜⟩ ∈ (1𝑜 × {1𝑜}))
226 elun 3731 . . . . . . . . 9 (⟨1𝑜, 1𝑜⟩ ∈ ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})) ↔ (⟨1𝑜, 1𝑜⟩ ∈ (𝐴 × {∅}) ∨ ⟨1𝑜, 1𝑜⟩ ∈ (1𝑜 × {1𝑜})))
227225, 226mtbir 313 . . . . . . . 8 ¬ ⟨1𝑜, 1𝑜⟩ ∈ ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜}))
228 ssnelpss 3696 . . . . . . . 8 (((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})) ⊆ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜})) → ((⟨1𝑜, 1𝑜⟩ ∈ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜})) ∧ ¬ ⟨1𝑜, 1𝑜⟩ ∈ ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜}))) → ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})) ⊊ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜}))))
229213, 227, 228mp2ani 713 . . . . . . 7 (((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})) ⊆ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜})) → ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})) ⊊ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜})))
230204, 229syl 17 . . . . . 6 (𝜑 → ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})) ⊊ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜})))
231 cdaval 8936 . . . . . . . 8 ((𝐴 ∈ V ∧ 1𝑜 ∈ ω) → (𝐴 +𝑐 1𝑜) = ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})))
2324, 206, 231sylancl 693 . . . . . . 7 (𝜑 → (𝐴 +𝑐 1𝑜) = ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})))
233 cdaval 8936 . . . . . . . 8 ((𝐴 ∈ V ∧ 2𝑜 ∈ ω) → (𝐴 +𝑐 2𝑜) = ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜})))
2344, 191, 233sylancl 693 . . . . . . 7 (𝜑 → (𝐴 +𝑐 2𝑜) = ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜})))
235232, 234psseq12d 3679 . . . . . 6 (𝜑 → ((𝐴 +𝑐 1𝑜) ⊊ (𝐴 +𝑐 2𝑜) ↔ ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})) ⊊ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜}))))
236230, 235mpbird 247 . . . . 5 (𝜑 → (𝐴 +𝑐 1𝑜) ⊊ (𝐴 +𝑐 2𝑜))
237 php3 8090 . . . . 5 (((𝐴 +𝑐 2𝑜) ∈ Fin ∧ (𝐴 +𝑐 1𝑜) ⊊ (𝐴 +𝑐 2𝑜)) → (𝐴 +𝑐 1𝑜) ≺ (𝐴 +𝑐 2𝑜))
238197, 236, 237syl2anc 692 . . . 4 (𝜑 → (𝐴 +𝑐 1𝑜) ≺ (𝐴 +𝑐 2𝑜))
239 canthp1lem1 9418 . . . . 5 (1𝑜𝐴 → (𝐴 +𝑐 2𝑜) ≼ 𝒫 𝐴)
2401, 239syl 17 . . . 4 (𝜑 → (𝐴 +𝑐 2𝑜) ≼ 𝒫 𝐴)
241 sdomdomtr 8037 . . . 4 (((𝐴 +𝑐 1𝑜) ≺ (𝐴 +𝑐 2𝑜) ∧ (𝐴 +𝑐 2𝑜) ≼ 𝒫 𝐴) → (𝐴 +𝑐 1𝑜) ≺ 𝒫 𝐴)
242238, 240, 241syl2anc 692 . . 3 (𝜑 → (𝐴 +𝑐 1𝑜) ≺ 𝒫 𝐴)
243 sdomnen 7928 . . 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 383  wa 384  w3a 1036   = wceq 1480  wex 1701  wcel 1987  wne 2790  wral 2907  Vcvv 3186  cdif 3552  cun 3553  cin 3554  wss 3555  wpss 3556  c0 3891  ifcif 4058  𝒫 cpw 4130  {csn 4148  cop 4154   cuni 4402   class class class wbr 4613  {copab 4672  cmpt 4673   We wwe 5032   × cxp 5072  ccnv 5073  dom cdm 5074  ran crn 5075  cres 5076  cima 5077  ccom 5078  Ord word 5681  Oncon0 5682  suc csuc 5684  Fun wfun 5841   Fn wfn 5842  wf 5843  1-1wf1 5844  ontowfo 5845  1-1-ontowf1o 5846  cfv 5847  (class class class)co 6604  ωcom 7012  1𝑜c1o 7498  2𝑜c2o 7499  cen 7896  cdom 7897  csdm 7898  Fincfn 7899  cardccrd 8705   +𝑐 ccda 8933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-inf2 8482
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-2o 7506  df-oadd 7509  df-er 7687  df-map 7804  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-oi 8359  df-card 8709  df-cda 8934
This theorem is referenced by:  canthp1  9420
  Copyright terms: Public domain W3C validator