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

Theorem canthp1lem2 9763
Description: Lemma for canthp1 9764. (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 8202 . . . . . . 7 Rel ≺
32brrelex2i 5366 . . . . . 6 (1𝑜𝐴𝐴 ∈ V)
41, 3syl 17 . . . . 5 (𝜑𝐴 ∈ V)
54pwexd 5056 . . . 4 (𝜑 → 𝒫 𝐴 ∈ V)
6 canthp1lem2.2 . . . 4 (𝜑𝐹:𝒫 𝐴1-1-onto→(𝐴 +𝑐 1𝑜))
7 f1oeng 8214 . . . 4 ((𝒫 𝐴 ∈ V ∧ 𝐹:𝒫 𝐴1-1-onto→(𝐴 +𝑐 1𝑜)) → 𝒫 𝐴 ≈ (𝐴 +𝑐 1𝑜))
85, 6, 7syl2anc 575 . . 3 (𝜑 → 𝒫 𝐴 ≈ (𝐴 +𝑐 1𝑜))
9 ensym 8244 . . 3 (𝒫 𝐴 ≈ (𝐴 +𝑐 1𝑜) → (𝐴 +𝑐 1𝑜) ≈ 𝒫 𝐴)
108, 9syl 17 . 2 (𝜑 → (𝐴 +𝑐 1𝑜) ≈ 𝒫 𝐴)
11 canth2g 8356 . . . . . . . . . . 11 (𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴)
124, 11syl 17 . . . . . . . . . 10 (𝜑𝐴 ≺ 𝒫 𝐴)
13 sdomen2 8347 . . . . . . . . . . 11 (𝒫 𝐴 ≈ (𝐴 +𝑐 1𝑜) → (𝐴 ≺ 𝒫 𝐴𝐴 ≺ (𝐴 +𝑐 1𝑜)))
148, 13syl 17 . . . . . . . . . 10 (𝜑 → (𝐴 ≺ 𝒫 𝐴𝐴 ≺ (𝐴 +𝑐 1𝑜)))
1512, 14mpbid 223 . . . . . . . . 9 (𝜑𝐴 ≺ (𝐴 +𝑐 1𝑜))
16 sdomnen 8224 . . . . . . . . 9 (𝐴 ≺ (𝐴 +𝑐 1𝑜) → ¬ 𝐴 ≈ (𝐴 +𝑐 1𝑜))
1715, 16syl 17 . . . . . . . 8 (𝜑 → ¬ 𝐴 ≈ (𝐴 +𝑐 1𝑜))
18 omelon 8793 . . . . . . . . . . . 12 ω ∈ On
19 onenon 9061 . . . . . . . . . . . 12 (ω ∈ On → ω ∈ dom card)
2018, 19ax-mp 5 . . . . . . . . . . 11 ω ∈ dom card
21 canthp1lem2.3 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐺:((𝐴 +𝑐 1𝑜) ∖ {(𝐹𝐴)})–1-1-onto𝐴)
22 dff1o3 6362 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝒫 𝐴1-1-onto→(𝐴 +𝑐 1𝑜) ↔ (𝐹:𝒫 𝐴onto→(𝐴 +𝑐 1𝑜) ∧ Fun 𝐹))
2322simprbi 486 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹:𝒫 𝐴1-1-onto→(𝐴 +𝑐 1𝑜) → Fun 𝐹)
246, 23syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → Fun 𝐹)
25 f1ofo 6363 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝒫 𝐴1-1-onto→(𝐴 +𝑐 1𝑜) → 𝐹:𝒫 𝐴onto→(𝐴 +𝑐 1𝑜))
266, 25syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐹:𝒫 𝐴onto→(𝐴 +𝑐 1𝑜))
27 f1ofn 6357 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝒫 𝐴1-1-onto→(𝐴 +𝑐 1𝑜) → 𝐹 Fn 𝒫 𝐴)
28 fnresdm 6214 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹 Fn 𝒫 𝐴 → (𝐹 ↾ 𝒫 𝐴) = 𝐹)
29 foeq1 6330 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹 ↾ 𝒫 𝐴) = 𝐹 → ((𝐹 ↾ 𝒫 𝐴):𝒫 𝐴onto→(𝐴 +𝑐 1𝑜) ↔ 𝐹:𝒫 𝐴onto→(𝐴 +𝑐 1𝑜)))
306, 27, 28, 294syl 19 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝐹 ↾ 𝒫 𝐴):𝒫 𝐴onto→(𝐴 +𝑐 1𝑜) ↔ 𝐹:𝒫 𝐴onto→(𝐴 +𝑐 1𝑜)))
3126, 30mpbird 248 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐹 ↾ 𝒫 𝐴):𝒫 𝐴onto→(𝐴 +𝑐 1𝑜))
32 fvex 6424 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹𝐴) ∈ V
33 f1osng 6396 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴 ∈ V ∧ (𝐹𝐴) ∈ V) → {⟨𝐴, (𝐹𝐴)⟩}:{𝐴}–1-1-onto→{(𝐹𝐴)})
344, 32, 33sylancl 576 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → {⟨𝐴, (𝐹𝐴)⟩}:{𝐴}–1-1-onto→{(𝐹𝐴)})
356, 27syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐹 Fn 𝒫 𝐴)
36 pwidg 4373 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐴 ∈ V → 𝐴 ∈ 𝒫 𝐴)
374, 36syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑𝐴 ∈ 𝒫 𝐴)
38 fnressn 6652 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹 Fn 𝒫 𝐴𝐴 ∈ 𝒫 𝐴) → (𝐹 ↾ {𝐴}) = {⟨𝐴, (𝐹𝐴)⟩})
3935, 37, 38syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐹 ↾ {𝐴}) = {⟨𝐴, (𝐹𝐴)⟩})
40 f1oeq1 6346 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹 ↾ {𝐴}) = {⟨𝐴, (𝐹𝐴)⟩} → ((𝐹 ↾ {𝐴}):{𝐴}–1-1-onto→{(𝐹𝐴)} ↔ {⟨𝐴, (𝐹𝐴)⟩}:{𝐴}–1-1-onto→{(𝐹𝐴)}))
4139, 40syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝐹 ↾ {𝐴}):{𝐴}–1-1-onto→{(𝐹𝐴)} ↔ {⟨𝐴, (𝐹𝐴)⟩}:{𝐴}–1-1-onto→{(𝐹𝐴)}))
4234, 41mpbird 248 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (𝐹 ↾ {𝐴}):{𝐴}–1-1-onto→{(𝐹𝐴)})
43 f1ofo 6363 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹 ↾ {𝐴}):{𝐴}–1-1-onto→{(𝐹𝐴)} → (𝐹 ↾ {𝐴}):{𝐴}–onto→{(𝐹𝐴)})
4442, 43syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝐹 ↾ {𝐴}):{𝐴}–onto→{(𝐹𝐴)})
45 resdif 6376 . . . . . . . . . . . . . . . . . . . . 21 ((Fun 𝐹 ∧ (𝐹 ↾ 𝒫 𝐴):𝒫 𝐴onto→(𝐴 +𝑐 1𝑜) ∧ (𝐹 ↾ {𝐴}):{𝐴}–onto→{(𝐹𝐴)}) → (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→((𝐴 +𝑐 1𝑜) ∖ {(𝐹𝐴)}))
4624, 31, 44, 45syl3anc 1483 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→((𝐴 +𝑐 1𝑜) ∖ {(𝐹𝐴)}))
47 f1oco 6378 . . . . . . . . . . . . . . . . . . . 20 ((𝐺:((𝐴 +𝑐 1𝑜) ∖ {(𝐹𝐴)})–1-1-onto𝐴 ∧ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto→((𝐴 +𝑐 1𝑜) ∖ {(𝐹𝐴)})) → (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴)
4821, 46, 47syl2anc 575 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴)
49 resco 5860 . . . . . . . . . . . . . . . . . . . 20 ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) = (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴})))
50 f1oeq1 6346 . . . . . . . . . . . . . . . . . . . 20 (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) = (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴 ↔ (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴))
5149, 50ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴 ↔ (𝐺 ∘ (𝐹 ↾ (𝒫 𝐴 ∖ {𝐴}))):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴)
5248, 51sylibr 225 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴)
53 f1of 6356 . . . . . . . . . . . . . . . . . 18 (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴 → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})⟶𝐴)
5452, 53syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})⟶𝐴)
55 0elpw 5033 . . . . . . . . . . . . . . . . . . . . 21 ∅ ∈ 𝒫 𝐴
5655a1i 11 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ 𝑥 = 𝐴) → ∅ ∈ 𝒫 𝐴)
57 sdom0 8334 . . . . . . . . . . . . . . . . . . . . . . . 24 ¬ 1𝑜 ≺ ∅
58 breq2 4855 . . . . . . . . . . . . . . . . . . . . . . . 24 (∅ = 𝐴 → (1𝑜 ≺ ∅ ↔ 1𝑜𝐴))
5957, 58mtbii 317 . . . . . . . . . . . . . . . . . . . . . . 23 (∅ = 𝐴 → ¬ 1𝑜𝐴)
6059necon2ai 3014 . . . . . . . . . . . . . . . . . . . . . 22 (1𝑜𝐴 → ∅ ≠ 𝐴)
611, 60syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ∅ ≠ 𝐴)
6261ad2antrr 708 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ 𝑥 = 𝐴) → ∅ ≠ 𝐴)
63 eldifsn 4515 . . . . . . . . . . . . . . . . . . . 20 (∅ ∈ (𝒫 𝐴 ∖ {𝐴}) ↔ (∅ ∈ 𝒫 𝐴 ∧ ∅ ≠ 𝐴))
6456, 62, 63sylanbrc 574 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ 𝑥 = 𝐴) → ∅ ∈ (𝒫 𝐴 ∖ {𝐴}))
65 simplr 776 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → 𝑥 ∈ 𝒫 𝐴)
66 simpr 473 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → ¬ 𝑥 = 𝐴)
6766neqned 2992 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → 𝑥𝐴)
68 eldifsn 4515 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝒫 𝐴 ∖ {𝐴}) ↔ (𝑥 ∈ 𝒫 𝐴𝑥𝐴))
6965, 67, 68sylanbrc 574 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑥 ∈ 𝒫 𝐴) ∧ ¬ 𝑥 = 𝐴) → 𝑥 ∈ (𝒫 𝐴 ∖ {𝐴}))
7064, 69ifclda 4320 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑥 ∈ 𝒫 𝐴) → if(𝑥 = 𝐴, ∅, 𝑥) ∈ (𝒫 𝐴 ∖ {𝐴}))
7170fmpttd 6610 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)):𝒫 𝐴⟶(𝒫 𝐴 ∖ {𝐴}))
72 fco 6276 . . . . . . . . . . . . . . . . 17 ((((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})⟶𝐴 ∧ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)):𝒫 𝐴⟶(𝒫 𝐴 ∖ {𝐴})) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))):𝒫 𝐴𝐴)
7354, 71, 72syl2anc 575 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))):𝒫 𝐴𝐴)
7471frnd 6266 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ran (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)) ⊆ (𝒫 𝐴 ∖ {𝐴}))
75 cores 5859 . . . . . . . . . . . . . . . . . . 19 (ran (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)) ⊆ (𝒫 𝐴 ∖ {𝐴}) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))) = ((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))))
7674, 75syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))) = ((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))))
77 canthp1lem2.4 . . . . . . . . . . . . . . . . . 18 𝐻 = ((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))
7876, 77syl6eqr 2865 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))) = 𝐻)
7978feq1d 6244 . . . . . . . . . . . . . . . 16 (𝜑 → ((((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))):𝒫 𝐴𝐴𝐻:𝒫 𝐴𝐴))
8073, 79mpbid 223 . . . . . . . . . . . . . . 15 (𝜑𝐻:𝒫 𝐴𝐴)
81 inss1 4036 . . . . . . . . . . . . . . . 16 (𝒫 𝐴 ∩ dom card) ⊆ 𝒫 𝐴
8281a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → (𝒫 𝐴 ∩ dom card) ⊆ 𝒫 𝐴)
83 canthp1lem2.5 . . . . . . . . . . . . . . . 16 𝑊 = {⟨𝑥, 𝑟⟩ ∣ ((𝑥𝐴𝑟 ⊆ (𝑥 × 𝑥)) ∧ (𝑟 We 𝑥 ∧ ∀𝑦𝑥 (𝐻‘(𝑟 “ {𝑦})) = 𝑦))}
84 canthp1lem2.6 . . . . . . . . . . . . . . . 16 𝐵 = dom 𝑊
85 eqid 2813 . . . . . . . . . . . . . . . 16 ((𝑊𝐵) “ {(𝐻𝐵)}) = ((𝑊𝐵) “ {(𝐻𝐵)})
8683, 84, 85canth4 9757 . . . . . . . . . . . . . . 15 ((𝐴 ∈ V ∧ 𝐻:𝒫 𝐴𝐴 ∧ (𝒫 𝐴 ∩ dom card) ⊆ 𝒫 𝐴) → (𝐵𝐴 ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ⊊ 𝐵 ∧ (𝐻𝐵) = (𝐻‘((𝑊𝐵) “ {(𝐻𝐵)}))))
874, 80, 82, 86syl3anc 1483 . . . . . . . . . . . . . 14 (𝜑 → (𝐵𝐴 ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ⊊ 𝐵 ∧ (𝐻𝐵) = (𝐻‘((𝑊𝐵) “ {(𝐻𝐵)}))))
8887simp1d 1165 . . . . . . . . . . . . 13 (𝜑𝐵𝐴)
8987simp2d 1166 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑊𝐵) “ {(𝐻𝐵)}) ⊊ 𝐵)
9089pssned 3910 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑊𝐵) “ {(𝐻𝐵)}) ≠ 𝐵)
9190necomd 3040 . . . . . . . . . . . . . . 15 (𝜑𝐵 ≠ ((𝑊𝐵) “ {(𝐻𝐵)}))
9287simp3d 1167 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝐻𝐵) = (𝐻‘((𝑊𝐵) “ {(𝐻𝐵)})))
9377fveq1i 6412 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐻𝐵) = (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘𝐵)
9477fveq1i 6412 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐻‘((𝑊𝐵) “ {(𝐻𝐵)})) = (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘((𝑊𝐵) “ {(𝐻𝐵)}))
9592, 93, 943eqtr3g 2870 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘𝐵) = (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘((𝑊𝐵) “ {(𝐻𝐵)})))
96 elpw2g 5026 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∈ V → (𝐵 ∈ 𝒫 𝐴𝐵𝐴))
974, 96syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (𝐵 ∈ 𝒫 𝐴𝐵𝐴))
9888, 97mpbird 248 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐵 ∈ 𝒫 𝐴)
99 fvco3 6499 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)):𝒫 𝐴⟶(𝒫 𝐴 ∖ {𝐴}) ∧ 𝐵 ∈ 𝒫 𝐴) → (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘𝐵) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)))
10071, 98, 99syl2anc 575 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘𝐵) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)))
10189pssssd 3909 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → ((𝑊𝐵) “ {(𝐻𝐵)}) ⊆ 𝐵)
102101, 88sstrd 3815 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → ((𝑊𝐵) “ {(𝐻𝐵)}) ⊆ 𝐴)
103 elpw2g 5026 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∈ V → (((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴 ↔ ((𝑊𝐵) “ {(𝐻𝐵)}) ⊆ 𝐴))
1044, 103syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴 ↔ ((𝑊𝐵) “ {(𝐻𝐵)}) ⊆ 𝐴))
105102, 104mpbird 248 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴)
106 fvco3 6499 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)):𝒫 𝐴⟶(𝒫 𝐴 ∖ {𝐴}) ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴) → (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘((𝑊𝐵) “ {(𝐻𝐵)})) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)}))))
10771, 105, 106syl2anc 575 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (((𝐺𝐹) ∘ (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)))‘((𝑊𝐵) “ {(𝐻𝐵)})) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)}))))
10895, 100, 1073eqtr3d 2855 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)}))))
109108adantr 468 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐵𝐴) → ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)) = ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)}))))
110 ifcl 4330 . . . . . . . . . . . . . . . . . . . . . . . 24 ((∅ ∈ 𝒫 𝐴𝐵 ∈ 𝒫 𝐴) → if(𝐵 = 𝐴, ∅, 𝐵) ∈ 𝒫 𝐴)
11155, 98, 110sylancr 577 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → if(𝐵 = 𝐴, ∅, 𝐵) ∈ 𝒫 𝐴)
112 eqeq1 2817 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝐵 → (𝑥 = 𝐴𝐵 = 𝐴))
113 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 𝐵𝑥 = 𝐵)
114112, 113ifbieq2d 4311 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝐵 → if(𝑥 = 𝐴, ∅, 𝑥) = if(𝐵 = 𝐴, ∅, 𝐵))
115 eqid 2813 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥)) = (𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))
116114, 115fvmptg 6504 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐵 ∈ 𝒫 𝐴 ∧ if(𝐵 = 𝐴, ∅, 𝐵) ∈ 𝒫 𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵) = if(𝐵 = 𝐴, ∅, 𝐵))
11798, 111, 116syl2anc 575 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵) = if(𝐵 = 𝐴, ∅, 𝐵))
118 pssne 3908 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐵𝐴𝐵𝐴)
119118neneqd 2990 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐵𝐴 → ¬ 𝐵 = 𝐴)
120119iffalsed 4297 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵𝐴 → if(𝐵 = 𝐴, ∅, 𝐵) = 𝐵)
121117, 120sylan9eq 2867 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐵𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵) = 𝐵)
122121fveq2d 6415 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐵𝐴) → ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘𝐵)) = ((𝐺𝐹)‘𝐵))
123 ifcl 4330 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((∅ ∈ 𝒫 𝐴 ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴) → if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})) ∈ 𝒫 𝐴)
12455, 105, 123sylancr 577 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})) ∈ 𝒫 𝐴)
125 eqeq1 2817 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = ((𝑊𝐵) “ {(𝐻𝐵)}) → (𝑥 = 𝐴 ↔ ((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴))
126 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = ((𝑊𝐵) “ {(𝐻𝐵)}) → 𝑥 = ((𝑊𝐵) “ {(𝐻𝐵)}))
127125, 126ifbieq2d 4311 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = ((𝑊𝐵) “ {(𝐻𝐵)}) → if(𝑥 = 𝐴, ∅, 𝑥) = if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})))
128127, 115fvmptg 6504 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴 ∧ if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})) ∈ 𝒫 𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)})) = if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})))
129105, 124, 128syl2anc 575 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)})) = if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})))
130129adantr 468 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝐵𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)})) = if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})))
131 sspsstr 3917 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝑊𝐵) “ {(𝐻𝐵)}) ⊆ 𝐵𝐵𝐴) → ((𝑊𝐵) “ {(𝐻𝐵)}) ⊊ 𝐴)
132101, 131sylan 571 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝐵𝐴) → ((𝑊𝐵) “ {(𝐻𝐵)}) ⊊ 𝐴)
133132pssned 3910 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝐵𝐴) → ((𝑊𝐵) “ {(𝐻𝐵)}) ≠ 𝐴)
134133neneqd 2990 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝐵𝐴) → ¬ ((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴)
135134iffalsed 4297 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝐵𝐴) → if(((𝑊𝐵) “ {(𝐻𝐵)}) = 𝐴, ∅, ((𝑊𝐵) “ {(𝐻𝐵)})) = ((𝑊𝐵) “ {(𝐻𝐵)}))
136130, 135eqtrd 2847 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐵𝐴) → ((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)})) = ((𝑊𝐵) “ {(𝐻𝐵)}))
137136fveq2d 6415 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐵𝐴) → ((𝐺𝐹)‘((𝑥 ∈ 𝒫 𝐴 ↦ if(𝑥 = 𝐴, ∅, 𝑥))‘((𝑊𝐵) “ {(𝐻𝐵)}))) = ((𝐺𝐹)‘((𝑊𝐵) “ {(𝐻𝐵)})))
138109, 122, 1373eqtr3d 2855 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐵𝐴) → ((𝐺𝐹)‘𝐵) = ((𝐺𝐹)‘((𝑊𝐵) “ {(𝐻𝐵)})))
13998, 118anim12i 602 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐵𝐴) → (𝐵 ∈ 𝒫 𝐴𝐵𝐴))
140 eldifsn 4515 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 ∈ (𝒫 𝐴 ∖ {𝐴}) ↔ (𝐵 ∈ 𝒫 𝐴𝐵𝐴))
141139, 140sylibr 225 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐵𝐴) → 𝐵 ∈ (𝒫 𝐴 ∖ {𝐴}))
142 fvres 6430 . . . . . . . . . . . . . . . . . . . 20 (𝐵 ∈ (𝒫 𝐴 ∖ {𝐴}) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = ((𝐺𝐹)‘𝐵))
143141, 142syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐵𝐴) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = ((𝐺𝐹)‘𝐵))
144105adantr 468 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝐵𝐴) → ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴)
145 eldifsn 4515 . . . . . . . . . . . . . . . . . . . . 21 (((𝑊𝐵) “ {(𝐻𝐵)}) ∈ (𝒫 𝐴 ∖ {𝐴}) ↔ (((𝑊𝐵) “ {(𝐻𝐵)}) ∈ 𝒫 𝐴 ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ≠ 𝐴))
146144, 133, 145sylanbrc 574 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝐵𝐴) → ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ (𝒫 𝐴 ∖ {𝐴}))
147 fvres 6430 . . . . . . . . . . . . . . . . . . . 20 (((𝑊𝐵) “ {(𝐻𝐵)}) ∈ (𝒫 𝐴 ∖ {𝐴}) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘((𝑊𝐵) “ {(𝐻𝐵)})) = ((𝐺𝐹)‘((𝑊𝐵) “ {(𝐻𝐵)})))
148146, 147syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐵𝐴) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘((𝑊𝐵) “ {(𝐻𝐵)})) = ((𝐺𝐹)‘((𝑊𝐵) “ {(𝐻𝐵)})))
149138, 143, 1483eqtr4d 2857 . . . . . . . . . . . . . . . . . 18 ((𝜑𝐵𝐴) → (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘((𝑊𝐵) “ {(𝐻𝐵)})))
150 f1of1 6355 . . . . . . . . . . . . . . . . . . . . 21 (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1-onto𝐴 → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1𝐴)
15152, 150syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1𝐴)
152151adantr 468 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝐵𝐴) → ((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1𝐴)
153 f1fveq 6746 . . . . . . . . . . . . . . . . . . 19 ((((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴})):(𝒫 𝐴 ∖ {𝐴})–1-1𝐴 ∧ (𝐵 ∈ (𝒫 𝐴 ∖ {𝐴}) ∧ ((𝑊𝐵) “ {(𝐻𝐵)}) ∈ (𝒫 𝐴 ∖ {𝐴}))) → ((((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘((𝑊𝐵) “ {(𝐻𝐵)})) ↔ 𝐵 = ((𝑊𝐵) “ {(𝐻𝐵)})))
154152, 141, 146, 153syl12anc 856 . . . . . . . . . . . . . . . . . 18 ((𝜑𝐵𝐴) → ((((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘𝐵) = (((𝐺𝐹) ↾ (𝒫 𝐴 ∖ {𝐴}))‘((𝑊𝐵) “ {(𝐻𝐵)})) ↔ 𝐵 = ((𝑊𝐵) “ {(𝐻𝐵)})))
155149, 154mpbid 223 . . . . . . . . . . . . . . . . 17 ((𝜑𝐵𝐴) → 𝐵 = ((𝑊𝐵) “ {(𝐻𝐵)}))
156155ex 399 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵𝐴𝐵 = ((𝑊𝐵) “ {(𝐻𝐵)})))
157156necon3ad 2998 . . . . . . . . . . . . . . 15 (𝜑 → (𝐵 ≠ ((𝑊𝐵) “ {(𝐻𝐵)}) → ¬ 𝐵𝐴))
15891, 157mpd 15 . . . . . . . . . . . . . 14 (𝜑 → ¬ 𝐵𝐴)
159 npss 3922 . . . . . . . . . . . . . 14 𝐵𝐴 ↔ (𝐵𝐴𝐵 = 𝐴))
160158, 159sylib 209 . . . . . . . . . . . . 13 (𝜑 → (𝐵𝐴𝐵 = 𝐴))
16188, 160mpd 15 . . . . . . . . . . . 12 (𝜑𝐵 = 𝐴)
162 eqid 2813 . . . . . . . . . . . . . . . . . . . 20 𝐵 = 𝐵
163 eqid 2813 . . . . . . . . . . . . . . . . . . . 20 (𝑊𝐵) = (𝑊𝐵)
164162, 163pm3.2i 458 . . . . . . . . . . . . . . . . . . 19 (𝐵 = 𝐵 ∧ (𝑊𝐵) = (𝑊𝐵))
16581sseli 3801 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝒫 𝐴 ∩ dom card) → 𝑥 ∈ 𝒫 𝐴)
166 ffvelrn 6582 . . . . . . . . . . . . . . . . . . . . 21 ((𝐻:𝒫 𝐴𝐴𝑥 ∈ 𝒫 𝐴) → (𝐻𝑥) ∈ 𝐴)
16780, 165, 166syl2an 585 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑥 ∈ (𝒫 𝐴 ∩ dom card)) → (𝐻𝑥) ∈ 𝐴)
16883, 4, 167, 84fpwwe 9756 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐵𝑊(𝑊𝐵) ∧ (𝐻𝐵) ∈ 𝐵) ↔ (𝐵 = 𝐵 ∧ (𝑊𝐵) = (𝑊𝐵))))
169164, 168mpbiri 249 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐵𝑊(𝑊𝐵) ∧ (𝐻𝐵) ∈ 𝐵))
170169simpld 484 . . . . . . . . . . . . . . . . 17 (𝜑𝐵𝑊(𝑊𝐵))
17183, 4fpwwelem 9755 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵𝑊(𝑊𝐵) ↔ ((𝐵𝐴 ∧ (𝑊𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊𝐵) We 𝐵 ∧ ∀𝑦𝐵 (𝐻‘((𝑊𝐵) “ {𝑦})) = 𝑦))))
172170, 171mpbid 223 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵𝐴 ∧ (𝑊𝐵) ⊆ (𝐵 × 𝐵)) ∧ ((𝑊𝐵) We 𝐵 ∧ ∀𝑦𝐵 (𝐻‘((𝑊𝐵) “ {𝑦})) = 𝑦)))
173172simprd 485 . . . . . . . . . . . . . . 15 (𝜑 → ((𝑊𝐵) We 𝐵 ∧ ∀𝑦𝐵 (𝐻‘((𝑊𝐵) “ {𝑦})) = 𝑦))
174173simpld 484 . . . . . . . . . . . . . 14 (𝜑 → (𝑊𝐵) We 𝐵)
175 fvex 6424 . . . . . . . . . . . . . . 15 (𝑊𝐵) ∈ V
176 weeq1 5306 . . . . . . . . . . . . . . 15 (𝑟 = (𝑊𝐵) → (𝑟 We 𝐵 ↔ (𝑊𝐵) We 𝐵))
177175, 176spcev 3500 . . . . . . . . . . . . . 14 ((𝑊𝐵) We 𝐵 → ∃𝑟 𝑟 We 𝐵)
178174, 177syl 17 . . . . . . . . . . . . 13 (𝜑 → ∃𝑟 𝑟 We 𝐵)
179 ween 9144 . . . . . . . . . . . . 13 (𝐵 ∈ dom card ↔ ∃𝑟 𝑟 We 𝐵)
180178, 179sylibr 225 . . . . . . . . . . . 12 (𝜑𝐵 ∈ dom card)
181161, 180eqeltrrd 2893 . . . . . . . . . . 11 (𝜑𝐴 ∈ dom card)
182 domtri2 9101 . . . . . . . . . . 11 ((ω ∈ dom card ∧ 𝐴 ∈ dom card) → (ω ≼ 𝐴 ↔ ¬ 𝐴 ≺ ω))
18320, 181, 182sylancr 577 . . . . . . . . . 10 (𝜑 → (ω ≼ 𝐴 ↔ ¬ 𝐴 ≺ ω))
184 infcda1 9303 . . . . . . . . . 10 (ω ≼ 𝐴 → (𝐴 +𝑐 1𝑜) ≈ 𝐴)
185183, 184syl6bir 245 . . . . . . . . 9 (𝜑 → (¬ 𝐴 ≺ ω → (𝐴 +𝑐 1𝑜) ≈ 𝐴))
186 ensym 8244 . . . . . . . . 9 ((𝐴 +𝑐 1𝑜) ≈ 𝐴𝐴 ≈ (𝐴 +𝑐 1𝑜))
187185, 186syl6 35 . . . . . . . 8 (𝜑 → (¬ 𝐴 ≺ ω → 𝐴 ≈ (𝐴 +𝑐 1𝑜)))
18817, 187mt3d 142 . . . . . . 7 (𝜑𝐴 ≺ ω)
189 2onn 7960 . . . . . . . 8 2𝑜 ∈ ω
190 nnsdom 8801 . . . . . . . 8 (2𝑜 ∈ ω → 2𝑜 ≺ ω)
191189, 190ax-mp 5 . . . . . . 7 2𝑜 ≺ ω
192 cdafi 9300 . . . . . . 7 ((𝐴 ≺ ω ∧ 2𝑜 ≺ ω) → (𝐴 +𝑐 2𝑜) ≺ ω)
193188, 191, 192sylancl 576 . . . . . 6 (𝜑 → (𝐴 +𝑐 2𝑜) ≺ ω)
194 isfinite 8799 . . . . . 6 ((𝐴 +𝑐 2𝑜) ∈ Fin ↔ (𝐴 +𝑐 2𝑜) ≺ ω)
195193, 194sylibr 225 . . . . 5 (𝜑 → (𝐴 +𝑐 2𝑜) ∈ Fin)
196 sssucid 6021 . . . . . . . . . 10 1𝑜 ⊆ suc 1𝑜
197 df-2o 7800 . . . . . . . . . 10 2𝑜 = suc 1𝑜
198196, 197sseqtr4i 3842 . . . . . . . . 9 1𝑜 ⊆ 2𝑜
199 xpss1 5336 . . . . . . . . 9 (1𝑜 ⊆ 2𝑜 → (1𝑜 × {1𝑜}) ⊆ (2𝑜 × {1𝑜}))
200198, 199ax-mp 5 . . . . . . . 8 (1𝑜 × {1𝑜}) ⊆ (2𝑜 × {1𝑜})
201 unss2 3990 . . . . . . . 8 ((1𝑜 × {1𝑜}) ⊆ (2𝑜 × {1𝑜}) → ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})) ⊆ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜})))
202200, 201mp1i 13 . . . . . . 7 (𝜑 → ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})) ⊆ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜})))
203 ssun2 3983 . . . . . . . . 9 (2𝑜 × {1𝑜}) ⊆ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜}))
204 1onn 7959 . . . . . . . . . . . . 13 1𝑜 ∈ ω
205204elexi 3414 . . . . . . . . . . . 12 1𝑜 ∈ V
206205sucid 6023 . . . . . . . . . . 11 1𝑜 ∈ suc 1𝑜
207206, 197eleqtrri 2891 . . . . . . . . . 10 1𝑜 ∈ 2𝑜
208205snid 4409 . . . . . . . . . 10 1𝑜 ∈ {1𝑜}
209 opelxpi 5355 . . . . . . . . . 10 ((1𝑜 ∈ 2𝑜 ∧ 1𝑜 ∈ {1𝑜}) → ⟨1𝑜, 1𝑜⟩ ∈ (2𝑜 × {1𝑜}))
210207, 208, 209mp2an 675 . . . . . . . . 9 ⟨1𝑜, 1𝑜⟩ ∈ (2𝑜 × {1𝑜})
211203, 210sselii 3802 . . . . . . . 8 ⟨1𝑜, 1𝑜⟩ ∈ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜}))
212 1n0 7815 . . . . . . . . . . . 12 1𝑜 ≠ ∅
213212neii 2987 . . . . . . . . . . 11 ¬ 1𝑜 = ∅
214 opelxp2 5358 . . . . . . . . . . . 12 (⟨1𝑜, 1𝑜⟩ ∈ (𝐴 × {∅}) → 1𝑜 ∈ {∅})
215 elsni 4394 . . . . . . . . . . . 12 (1𝑜 ∈ {∅} → 1𝑜 = ∅)
216214, 215syl 17 . . . . . . . . . . 11 (⟨1𝑜, 1𝑜⟩ ∈ (𝐴 × {∅}) → 1𝑜 = ∅)
217213, 216mto 188 . . . . . . . . . 10 ¬ ⟨1𝑜, 1𝑜⟩ ∈ (𝐴 × {∅})
218 nnord 7306 . . . . . . . . . . . 12 (1𝑜 ∈ ω → Ord 1𝑜)
219 ordirr 5961 . . . . . . . . . . . 12 (Ord 1𝑜 → ¬ 1𝑜 ∈ 1𝑜)
220204, 218, 219mp2b 10 . . . . . . . . . . 11 ¬ 1𝑜 ∈ 1𝑜
221 opelxp1 5357 . . . . . . . . . . 11 (⟨1𝑜, 1𝑜⟩ ∈ (1𝑜 × {1𝑜}) → 1𝑜 ∈ 1𝑜)
222220, 221mto 188 . . . . . . . . . 10 ¬ ⟨1𝑜, 1𝑜⟩ ∈ (1𝑜 × {1𝑜})
223217, 222pm3.2ni 896 . . . . . . . . 9 ¬ (⟨1𝑜, 1𝑜⟩ ∈ (𝐴 × {∅}) ∨ ⟨1𝑜, 1𝑜⟩ ∈ (1𝑜 × {1𝑜}))
224 elun 3959 . . . . . . . . 9 (⟨1𝑜, 1𝑜⟩ ∈ ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})) ↔ (⟨1𝑜, 1𝑜⟩ ∈ (𝐴 × {∅}) ∨ ⟨1𝑜, 1𝑜⟩ ∈ (1𝑜 × {1𝑜})))
225223, 224mtbir 314 . . . . . . . 8 ¬ ⟨1𝑜, 1𝑜⟩ ∈ ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜}))
226 ssnelpss 3923 . . . . . . . 8 (((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})) ⊆ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜})) → ((⟨1𝑜, 1𝑜⟩ ∈ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜})) ∧ ¬ ⟨1𝑜, 1𝑜⟩ ∈ ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜}))) → ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})) ⊊ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜}))))
227211, 225, 226mp2ani 681 . . . . . . 7 (((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})) ⊆ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜})) → ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})) ⊊ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜})))
228202, 227syl 17 . . . . . 6 (𝜑 → ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})) ⊊ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜})))
229 cdaval 9280 . . . . . . . 8 ((𝐴 ∈ V ∧ 1𝑜 ∈ ω) → (𝐴 +𝑐 1𝑜) = ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})))
2304, 204, 229sylancl 576 . . . . . . 7 (𝜑 → (𝐴 +𝑐 1𝑜) = ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})))
231 cdaval 9280 . . . . . . . 8 ((𝐴 ∈ V ∧ 2𝑜 ∈ ω) → (𝐴 +𝑐 2𝑜) = ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜})))
2324, 189, 231sylancl 576 . . . . . . 7 (𝜑 → (𝐴 +𝑐 2𝑜) = ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜})))
233230, 232psseq12d 3906 . . . . . 6 (𝜑 → ((𝐴 +𝑐 1𝑜) ⊊ (𝐴 +𝑐 2𝑜) ↔ ((𝐴 × {∅}) ∪ (1𝑜 × {1𝑜})) ⊊ ((𝐴 × {∅}) ∪ (2𝑜 × {1𝑜}))))
234228, 233mpbird 248 . . . . 5 (𝜑 → (𝐴 +𝑐 1𝑜) ⊊ (𝐴 +𝑐 2𝑜))
235 php3 8388 . . . . 5 (((𝐴 +𝑐 2𝑜) ∈ Fin ∧ (𝐴 +𝑐 1𝑜) ⊊ (𝐴 +𝑐 2𝑜)) → (𝐴 +𝑐 1𝑜) ≺ (𝐴 +𝑐 2𝑜))
236195, 234, 235syl2anc 575 . . . 4 (𝜑 → (𝐴 +𝑐 1𝑜) ≺ (𝐴 +𝑐 2𝑜))
237 canthp1lem1 9762 . . . . 5 (1𝑜𝐴 → (𝐴 +𝑐 2𝑜) ≼ 𝒫 𝐴)
2381, 237syl 17 . . . 4 (𝜑 → (𝐴 +𝑐 2𝑜) ≼ 𝒫 𝐴)
239 sdomdomtr 8335 . . . 4 (((𝐴 +𝑐 1𝑜) ≺ (𝐴 +𝑐 2𝑜) ∧ (𝐴 +𝑐 2𝑜) ≼ 𝒫 𝐴) → (𝐴 +𝑐 1𝑜) ≺ 𝒫 𝐴)
240236, 238, 239syl2anc 575 . . 3 (𝜑 → (𝐴 +𝑐 1𝑜) ≺ 𝒫 𝐴)
241 sdomnen 8224 . . 3 ((𝐴 +𝑐 1𝑜) ≺ 𝒫 𝐴 → ¬ (𝐴 +𝑐 1𝑜) ≈ 𝒫 𝐴)
242240, 241syl 17 . 2 (𝜑 → ¬ (𝐴 +𝑐 1𝑜) ≈ 𝒫 𝐴)
24310, 242pm2.65i 185 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865  w3a 1100   = wceq 1637  wex 1859  wcel 2157  wne 2985  wral 3103  Vcvv 3398  cdif 3773  cun 3774  cin 3775  wss 3776  wpss 3777  c0 4123  ifcif 4286  𝒫 cpw 4358  {csn 4377  cop 4383   cuni 4637   class class class wbr 4851  {copab 4913  cmpt 4930   We wwe 5276   × cxp 5316  ccnv 5317  dom cdm 5318  ran crn 5319  cres 5320  cima 5321  ccom 5322  Ord word 5942  Oncon0 5943  suc csuc 5945  Fun wfun 6098   Fn wfn 6099  wf 6100  1-1wf1 6101  ontowfo 6102  1-1-ontowf1o 6103  cfv 6104  (class class class)co 6877  ωcom 7298  1𝑜c1o 7792  2𝑜c2o 7793  cen 8192  cdom 8193  csdm 8194  Fincfn 8195  cardccrd 9047   +𝑐 ccda 9277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-rep 4971  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182  ax-inf2 8788
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-ral 3108  df-rex 3109  df-reu 3110  df-rmo 3111  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-pss 3792  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-tp 4382  df-op 4384  df-uni 4638  df-int 4677  df-iun 4721  df-br 4852  df-opab 4914  df-mpt 4931  df-tr 4954  df-id 5226  df-eprel 5231  df-po 5239  df-so 5240  df-fr 5277  df-se 5278  df-we 5279  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-pred 5900  df-ord 5946  df-on 5947  df-lim 5948  df-suc 5949  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-fv 6112  df-isom 6113  df-riota 6838  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-om 7299  df-1st 7401  df-2nd 7402  df-wrecs 7645  df-recs 7707  df-rdg 7745  df-1o 7799  df-2o 7800  df-oadd 7803  df-er 7982  df-map 8097  df-en 8196  df-dom 8197  df-sdom 8198  df-fin 8199  df-oi 8657  df-card 9051  df-cda 9278
This theorem is referenced by:  canthp1  9764
  Copyright terms: Public domain W3C validator