Metamath Proof Explorer


Theorem canthp1lem2

Description: Lemma for canthp1 . (Contributed by Mario Carneiro, 18-May-2015)

Ref Expression
Hypotheses 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 canthp1lem2 ¬ 𝜑

Proof

Step Hyp Ref Expression
1 canthp1lem2.1 ( 𝜑 → 1o𝐴 )
2 canthp1lem2.2 ( 𝜑𝐹 : 𝒫 𝐴1-1-onto→ ( 𝐴 ⊔ 1o ) )
3 canthp1lem2.3 ( 𝜑𝐺 : ( ( 𝐴 ⊔ 1o ) ∖ { ( 𝐹𝐴 ) } ) –1-1-onto𝐴 )
4 canthp1lem2.4 𝐻 = ( ( 𝐺𝐹 ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) )
5 canthp1lem2.5 𝑊 = { ⟨ 𝑥 , 𝑟 ⟩ ∣ ( ( 𝑥𝐴𝑟 ⊆ ( 𝑥 × 𝑥 ) ) ∧ ( 𝑟 We 𝑥 ∧ ∀ 𝑦𝑥 ( 𝐻 ‘ ( 𝑟 “ { 𝑦 } ) ) = 𝑦 ) ) }
6 canthp1lem2.6 𝐵 = dom 𝑊
7 relsdom Rel ≺
8 7 brrelex2i ( 1o𝐴𝐴 ∈ V )
9 1 8 syl ( 𝜑𝐴 ∈ V )
10 9 pwexd ( 𝜑 → 𝒫 𝐴 ∈ V )
11 f1oeng ( ( 𝒫 𝐴 ∈ V ∧ 𝐹 : 𝒫 𝐴1-1-onto→ ( 𝐴 ⊔ 1o ) ) → 𝒫 𝐴 ≈ ( 𝐴 ⊔ 1o ) )
12 10 2 11 syl2anc ( 𝜑 → 𝒫 𝐴 ≈ ( 𝐴 ⊔ 1o ) )
13 12 ensymd ( 𝜑 → ( 𝐴 ⊔ 1o ) ≈ 𝒫 𝐴 )
14 canth2g ( 𝐴 ∈ V → 𝐴 ≺ 𝒫 𝐴 )
15 9 14 syl ( 𝜑𝐴 ≺ 𝒫 𝐴 )
16 sdomen2 ( 𝒫 𝐴 ≈ ( 𝐴 ⊔ 1o ) → ( 𝐴 ≺ 𝒫 𝐴𝐴 ≺ ( 𝐴 ⊔ 1o ) ) )
17 12 16 syl ( 𝜑 → ( 𝐴 ≺ 𝒫 𝐴𝐴 ≺ ( 𝐴 ⊔ 1o ) ) )
18 15 17 mpbid ( 𝜑𝐴 ≺ ( 𝐴 ⊔ 1o ) )
19 sdomnen ( 𝐴 ≺ ( 𝐴 ⊔ 1o ) → ¬ 𝐴 ≈ ( 𝐴 ⊔ 1o ) )
20 18 19 syl ( 𝜑 → ¬ 𝐴 ≈ ( 𝐴 ⊔ 1o ) )
21 omelon ω ∈ On
22 onenon ( ω ∈ On → ω ∈ dom card )
23 21 22 ax-mp ω ∈ dom card
24 dff1o3 ( 𝐹 : 𝒫 𝐴1-1-onto→ ( 𝐴 ⊔ 1o ) ↔ ( 𝐹 : 𝒫 𝐴onto→ ( 𝐴 ⊔ 1o ) ∧ Fun 𝐹 ) )
25 24 simprbi ( 𝐹 : 𝒫 𝐴1-1-onto→ ( 𝐴 ⊔ 1o ) → Fun 𝐹 )
26 2 25 syl ( 𝜑 → Fun 𝐹 )
27 f1ofo ( 𝐹 : 𝒫 𝐴1-1-onto→ ( 𝐴 ⊔ 1o ) → 𝐹 : 𝒫 𝐴onto→ ( 𝐴 ⊔ 1o ) )
28 2 27 syl ( 𝜑𝐹 : 𝒫 𝐴onto→ ( 𝐴 ⊔ 1o ) )
29 f1ofn ( 𝐹 : 𝒫 𝐴1-1-onto→ ( 𝐴 ⊔ 1o ) → 𝐹 Fn 𝒫 𝐴 )
30 fnresdm ( 𝐹 Fn 𝒫 𝐴 → ( 𝐹 ↾ 𝒫 𝐴 ) = 𝐹 )
31 foeq1 ( ( 𝐹 ↾ 𝒫 𝐴 ) = 𝐹 → ( ( 𝐹 ↾ 𝒫 𝐴 ) : 𝒫 𝐴onto→ ( 𝐴 ⊔ 1o ) ↔ 𝐹 : 𝒫 𝐴onto→ ( 𝐴 ⊔ 1o ) ) )
32 2 29 30 31 4syl ( 𝜑 → ( ( 𝐹 ↾ 𝒫 𝐴 ) : 𝒫 𝐴onto→ ( 𝐴 ⊔ 1o ) ↔ 𝐹 : 𝒫 𝐴onto→ ( 𝐴 ⊔ 1o ) ) )
33 28 32 mpbird ( 𝜑 → ( 𝐹 ↾ 𝒫 𝐴 ) : 𝒫 𝐴onto→ ( 𝐴 ⊔ 1o ) )
34 fvex ( 𝐹𝐴 ) ∈ V
35 f1osng ( ( 𝐴 ∈ V ∧ ( 𝐹𝐴 ) ∈ V ) → { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } : { 𝐴 } –1-1-onto→ { ( 𝐹𝐴 ) } )
36 9 34 35 sylancl ( 𝜑 → { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } : { 𝐴 } –1-1-onto→ { ( 𝐹𝐴 ) } )
37 2 29 syl ( 𝜑𝐹 Fn 𝒫 𝐴 )
38 pwidg ( 𝐴 ∈ V → 𝐴 ∈ 𝒫 𝐴 )
39 9 38 syl ( 𝜑𝐴 ∈ 𝒫 𝐴 )
40 fnressn ( ( 𝐹 Fn 𝒫 𝐴𝐴 ∈ 𝒫 𝐴 ) → ( 𝐹 ↾ { 𝐴 } ) = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } )
41 37 39 40 syl2anc ( 𝜑 → ( 𝐹 ↾ { 𝐴 } ) = { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } )
42 41 f1oeq1d ( 𝜑 → ( ( 𝐹 ↾ { 𝐴 } ) : { 𝐴 } –1-1-onto→ { ( 𝐹𝐴 ) } ↔ { ⟨ 𝐴 , ( 𝐹𝐴 ) ⟩ } : { 𝐴 } –1-1-onto→ { ( 𝐹𝐴 ) } ) )
43 36 42 mpbird ( 𝜑 → ( 𝐹 ↾ { 𝐴 } ) : { 𝐴 } –1-1-onto→ { ( 𝐹𝐴 ) } )
44 f1ofo ( ( 𝐹 ↾ { 𝐴 } ) : { 𝐴 } –1-1-onto→ { ( 𝐹𝐴 ) } → ( 𝐹 ↾ { 𝐴 } ) : { 𝐴 } –onto→ { ( 𝐹𝐴 ) } )
45 43 44 syl ( 𝜑 → ( 𝐹 ↾ { 𝐴 } ) : { 𝐴 } –onto→ { ( 𝐹𝐴 ) } )
46 resdif ( ( Fun 𝐹 ∧ ( 𝐹 ↾ 𝒫 𝐴 ) : 𝒫 𝐴onto→ ( 𝐴 ⊔ 1o ) ∧ ( 𝐹 ↾ { 𝐴 } ) : { 𝐴 } –onto→ { ( 𝐹𝐴 ) } ) → ( 𝐹 ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1-onto→ ( ( 𝐴 ⊔ 1o ) ∖ { ( 𝐹𝐴 ) } ) )
47 26 33 45 46 syl3anc ( 𝜑 → ( 𝐹 ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1-onto→ ( ( 𝐴 ⊔ 1o ) ∖ { ( 𝐹𝐴 ) } ) )
48 f1oco ( ( 𝐺 : ( ( 𝐴 ⊔ 1o ) ∖ { ( 𝐹𝐴 ) } ) –1-1-onto𝐴 ∧ ( 𝐹 ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1-onto→ ( ( 𝐴 ⊔ 1o ) ∖ { ( 𝐹𝐴 ) } ) ) → ( 𝐺 ∘ ( 𝐹 ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1-onto𝐴 )
49 3 47 48 syl2anc ( 𝜑 → ( 𝐺 ∘ ( 𝐹 ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1-onto𝐴 )
50 resco ( ( 𝐺𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) = ( 𝐺 ∘ ( 𝐹 ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) )
51 f1oeq1 ( ( ( 𝐺𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) = ( 𝐺 ∘ ( 𝐹 ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ) → ( ( ( 𝐺𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1-onto𝐴 ↔ ( 𝐺 ∘ ( 𝐹 ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1-onto𝐴 ) )
52 50 51 ax-mp ( ( ( 𝐺𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1-onto𝐴 ↔ ( 𝐺 ∘ ( 𝐹 ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1-onto𝐴 )
53 49 52 sylibr ( 𝜑 → ( ( 𝐺𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1-onto𝐴 )
54 f1of ( ( ( 𝐺𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1-onto𝐴 → ( ( 𝐺𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) ⟶ 𝐴 )
55 53 54 syl ( 𝜑 → ( ( 𝐺𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) ⟶ 𝐴 )
56 0elpw ∅ ∈ 𝒫 𝐴
57 56 a1i ( ( ( 𝜑𝑥 ∈ 𝒫 𝐴 ) ∧ 𝑥 = 𝐴 ) → ∅ ∈ 𝒫 𝐴 )
58 sdom0 ¬ 1o ≺ ∅
59 breq2 ( ∅ = 𝐴 → ( 1o ≺ ∅ ↔ 1o𝐴 ) )
60 58 59 mtbii ( ∅ = 𝐴 → ¬ 1o𝐴 )
61 60 necon2ai ( 1o𝐴 → ∅ ≠ 𝐴 )
62 1 61 syl ( 𝜑 → ∅ ≠ 𝐴 )
63 62 ad2antrr ( ( ( 𝜑𝑥 ∈ 𝒫 𝐴 ) ∧ 𝑥 = 𝐴 ) → ∅ ≠ 𝐴 )
64 eldifsn ( ∅ ∈ ( 𝒫 𝐴 ∖ { 𝐴 } ) ↔ ( ∅ ∈ 𝒫 𝐴 ∧ ∅ ≠ 𝐴 ) )
65 57 63 64 sylanbrc ( ( ( 𝜑𝑥 ∈ 𝒫 𝐴 ) ∧ 𝑥 = 𝐴 ) → ∅ ∈ ( 𝒫 𝐴 ∖ { 𝐴 } ) )
66 simplr ( ( ( 𝜑𝑥 ∈ 𝒫 𝐴 ) ∧ ¬ 𝑥 = 𝐴 ) → 𝑥 ∈ 𝒫 𝐴 )
67 simpr ( ( ( 𝜑𝑥 ∈ 𝒫 𝐴 ) ∧ ¬ 𝑥 = 𝐴 ) → ¬ 𝑥 = 𝐴 )
68 67 neqned ( ( ( 𝜑𝑥 ∈ 𝒫 𝐴 ) ∧ ¬ 𝑥 = 𝐴 ) → 𝑥𝐴 )
69 eldifsn ( 𝑥 ∈ ( 𝒫 𝐴 ∖ { 𝐴 } ) ↔ ( 𝑥 ∈ 𝒫 𝐴𝑥𝐴 ) )
70 66 68 69 sylanbrc ( ( ( 𝜑𝑥 ∈ 𝒫 𝐴 ) ∧ ¬ 𝑥 = 𝐴 ) → 𝑥 ∈ ( 𝒫 𝐴 ∖ { 𝐴 } ) )
71 65 70 ifclda ( ( 𝜑𝑥 ∈ 𝒫 𝐴 ) → if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ∈ ( 𝒫 𝐴 ∖ { 𝐴 } ) )
72 71 fmpttd ( 𝜑 → ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) : 𝒫 𝐴 ⟶ ( 𝒫 𝐴 ∖ { 𝐴 } ) )
73 55 72 fcod ( 𝜑 → ( ( ( 𝐺𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ) : 𝒫 𝐴𝐴 )
74 72 frnd ( 𝜑 → ran ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ⊆ ( 𝒫 𝐴 ∖ { 𝐴 } ) )
75 cores ( ran ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ⊆ ( 𝒫 𝐴 ∖ { 𝐴 } ) → ( ( ( 𝐺𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ) = ( ( 𝐺𝐹 ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ) )
76 74 75 syl ( 𝜑 → ( ( ( 𝐺𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ) = ( ( 𝐺𝐹 ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ) )
77 76 4 eqtr4di ( 𝜑 → ( ( ( 𝐺𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ) = 𝐻 )
78 77 feq1d ( 𝜑 → ( ( ( ( 𝐺𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ) : 𝒫 𝐴𝐴𝐻 : 𝒫 𝐴𝐴 ) )
79 73 78 mpbid ( 𝜑𝐻 : 𝒫 𝐴𝐴 )
80 inss1 ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝒫 𝐴
81 80 a1i ( 𝜑 → ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝒫 𝐴 )
82 eqid ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) = ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } )
83 5 6 82 canth4 ( ( 𝐴 ∈ V ∧ 𝐻 : 𝒫 𝐴𝐴 ∧ ( 𝒫 𝐴 ∩ dom card ) ⊆ 𝒫 𝐴 ) → ( 𝐵𝐴 ∧ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ⊊ 𝐵 ∧ ( 𝐻𝐵 ) = ( 𝐻 ‘ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) ) )
84 9 79 81 83 syl3anc ( 𝜑 → ( 𝐵𝐴 ∧ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ⊊ 𝐵 ∧ ( 𝐻𝐵 ) = ( 𝐻 ‘ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) ) )
85 84 simp1d ( 𝜑𝐵𝐴 )
86 84 simp2d ( 𝜑 → ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ⊊ 𝐵 )
87 86 pssned ( 𝜑 → ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ≠ 𝐵 )
88 87 necomd ( 𝜑𝐵 ≠ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) )
89 84 simp3d ( 𝜑 → ( 𝐻𝐵 ) = ( 𝐻 ‘ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) )
90 4 fveq1i ( 𝐻𝐵 ) = ( ( ( 𝐺𝐹 ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ) ‘ 𝐵 )
91 4 fveq1i ( 𝐻 ‘ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) = ( ( ( 𝐺𝐹 ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ) ‘ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) )
92 89 90 91 3eqtr3g ( 𝜑 → ( ( ( 𝐺𝐹 ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ) ‘ 𝐵 ) = ( ( ( 𝐺𝐹 ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ) ‘ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) )
93 9 85 sselpwd ( 𝜑𝐵 ∈ 𝒫 𝐴 )
94 72 93 fvco3d ( 𝜑 → ( ( ( 𝐺𝐹 ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ) ‘ 𝐵 ) = ( ( 𝐺𝐹 ) ‘ ( ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ‘ 𝐵 ) ) )
95 86 pssssd ( 𝜑 → ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ⊆ 𝐵 )
96 95 85 sstrd ( 𝜑 → ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ⊆ 𝐴 )
97 9 96 sselpwd ( 𝜑 → ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ∈ 𝒫 𝐴 )
98 72 97 fvco3d ( 𝜑 → ( ( ( 𝐺𝐹 ) ∘ ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ) ‘ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) = ( ( 𝐺𝐹 ) ‘ ( ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ‘ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) ) )
99 92 94 98 3eqtr3d ( 𝜑 → ( ( 𝐺𝐹 ) ‘ ( ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ‘ 𝐵 ) ) = ( ( 𝐺𝐹 ) ‘ ( ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ‘ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) ) )
100 99 adantr ( ( 𝜑𝐵𝐴 ) → ( ( 𝐺𝐹 ) ‘ ( ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ‘ 𝐵 ) ) = ( ( 𝐺𝐹 ) ‘ ( ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ‘ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) ) )
101 eqid ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) = ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) )
102 eqeq1 ( 𝑥 = 𝐵 → ( 𝑥 = 𝐴𝐵 = 𝐴 ) )
103 id ( 𝑥 = 𝐵𝑥 = 𝐵 )
104 102 103 ifbieq2d ( 𝑥 = 𝐵 → if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) = if ( 𝐵 = 𝐴 , ∅ , 𝐵 ) )
105 ifcl ( ( ∅ ∈ 𝒫 𝐴𝐵 ∈ 𝒫 𝐴 ) → if ( 𝐵 = 𝐴 , ∅ , 𝐵 ) ∈ 𝒫 𝐴 )
106 56 93 105 sylancr ( 𝜑 → if ( 𝐵 = 𝐴 , ∅ , 𝐵 ) ∈ 𝒫 𝐴 )
107 101 104 93 106 fvmptd3 ( 𝜑 → ( ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ‘ 𝐵 ) = if ( 𝐵 = 𝐴 , ∅ , 𝐵 ) )
108 pssne ( 𝐵𝐴𝐵𝐴 )
109 108 neneqd ( 𝐵𝐴 → ¬ 𝐵 = 𝐴 )
110 109 iffalsed ( 𝐵𝐴 → if ( 𝐵 = 𝐴 , ∅ , 𝐵 ) = 𝐵 )
111 107 110 sylan9eq ( ( 𝜑𝐵𝐴 ) → ( ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ‘ 𝐵 ) = 𝐵 )
112 111 fveq2d ( ( 𝜑𝐵𝐴 ) → ( ( 𝐺𝐹 ) ‘ ( ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ‘ 𝐵 ) ) = ( ( 𝐺𝐹 ) ‘ 𝐵 ) )
113 eqeq1 ( 𝑥 = ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) → ( 𝑥 = 𝐴 ↔ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) = 𝐴 ) )
114 id ( 𝑥 = ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) → 𝑥 = ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) )
115 113 114 ifbieq2d ( 𝑥 = ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) → if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) = if ( ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) = 𝐴 , ∅ , ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) )
116 ifcl ( ( ∅ ∈ 𝒫 𝐴 ∧ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ∈ 𝒫 𝐴 ) → if ( ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) = 𝐴 , ∅ , ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) ∈ 𝒫 𝐴 )
117 56 97 116 sylancr ( 𝜑 → if ( ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) = 𝐴 , ∅ , ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) ∈ 𝒫 𝐴 )
118 101 115 97 117 fvmptd3 ( 𝜑 → ( ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ‘ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) = if ( ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) = 𝐴 , ∅ , ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) )
119 118 adantr ( ( 𝜑𝐵𝐴 ) → ( ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ‘ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) = if ( ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) = 𝐴 , ∅ , ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) )
120 sspsstr ( ( ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ⊆ 𝐵𝐵𝐴 ) → ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ⊊ 𝐴 )
121 95 120 sylan ( ( 𝜑𝐵𝐴 ) → ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ⊊ 𝐴 )
122 121 pssned ( ( 𝜑𝐵𝐴 ) → ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ≠ 𝐴 )
123 122 neneqd ( ( 𝜑𝐵𝐴 ) → ¬ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) = 𝐴 )
124 123 iffalsed ( ( 𝜑𝐵𝐴 ) → if ( ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) = 𝐴 , ∅ , ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) = ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) )
125 119 124 eqtrd ( ( 𝜑𝐵𝐴 ) → ( ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ‘ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) = ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) )
126 125 fveq2d ( ( 𝜑𝐵𝐴 ) → ( ( 𝐺𝐹 ) ‘ ( ( 𝑥 ∈ 𝒫 𝐴 ↦ if ( 𝑥 = 𝐴 , ∅ , 𝑥 ) ) ‘ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) ) = ( ( 𝐺𝐹 ) ‘ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) )
127 100 112 126 3eqtr3d ( ( 𝜑𝐵𝐴 ) → ( ( 𝐺𝐹 ) ‘ 𝐵 ) = ( ( 𝐺𝐹 ) ‘ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) )
128 93 108 anim12i ( ( 𝜑𝐵𝐴 ) → ( 𝐵 ∈ 𝒫 𝐴𝐵𝐴 ) )
129 eldifsn ( 𝐵 ∈ ( 𝒫 𝐴 ∖ { 𝐴 } ) ↔ ( 𝐵 ∈ 𝒫 𝐴𝐵𝐴 ) )
130 128 129 sylibr ( ( 𝜑𝐵𝐴 ) → 𝐵 ∈ ( 𝒫 𝐴 ∖ { 𝐴 } ) )
131 130 fvresd ( ( 𝜑𝐵𝐴 ) → ( ( ( 𝐺𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ‘ 𝐵 ) = ( ( 𝐺𝐹 ) ‘ 𝐵 ) )
132 97 adantr ( ( 𝜑𝐵𝐴 ) → ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ∈ 𝒫 𝐴 )
133 eldifsn ( ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ∈ ( 𝒫 𝐴 ∖ { 𝐴 } ) ↔ ( ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ∈ 𝒫 𝐴 ∧ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ≠ 𝐴 ) )
134 132 122 133 sylanbrc ( ( 𝜑𝐵𝐴 ) → ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ∈ ( 𝒫 𝐴 ∖ { 𝐴 } ) )
135 134 fvresd ( ( 𝜑𝐵𝐴 ) → ( ( ( 𝐺𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ‘ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) = ( ( 𝐺𝐹 ) ‘ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) )
136 127 131 135 3eqtr4d ( ( 𝜑𝐵𝐴 ) → ( ( ( 𝐺𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ‘ 𝐵 ) = ( ( ( 𝐺𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ‘ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) )
137 f1of1 ( ( ( 𝐺𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1-onto𝐴 → ( ( 𝐺𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1𝐴 )
138 53 137 syl ( 𝜑 → ( ( 𝐺𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1𝐴 )
139 138 adantr ( ( 𝜑𝐵𝐴 ) → ( ( 𝐺𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1𝐴 )
140 f1fveq ( ( ( ( 𝐺𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) : ( 𝒫 𝐴 ∖ { 𝐴 } ) –1-1𝐴 ∧ ( 𝐵 ∈ ( 𝒫 𝐴 ∖ { 𝐴 } ) ∧ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ∈ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ) → ( ( ( ( 𝐺𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ‘ 𝐵 ) = ( ( ( 𝐺𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ‘ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) ↔ 𝐵 = ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) )
141 139 130 134 140 syl12anc ( ( 𝜑𝐵𝐴 ) → ( ( ( ( 𝐺𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ‘ 𝐵 ) = ( ( ( 𝐺𝐹 ) ↾ ( 𝒫 𝐴 ∖ { 𝐴 } ) ) ‘ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) ↔ 𝐵 = ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) )
142 136 141 mpbid ( ( 𝜑𝐵𝐴 ) → 𝐵 = ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) )
143 142 ex ( 𝜑 → ( 𝐵𝐴𝐵 = ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) ) )
144 143 necon3ad ( 𝜑 → ( 𝐵 ≠ ( ( 𝑊𝐵 ) “ { ( 𝐻𝐵 ) } ) → ¬ 𝐵𝐴 ) )
145 88 144 mpd ( 𝜑 → ¬ 𝐵𝐴 )
146 npss ( ¬ 𝐵𝐴 ↔ ( 𝐵𝐴𝐵 = 𝐴 ) )
147 145 146 sylib ( 𝜑 → ( 𝐵𝐴𝐵 = 𝐴 ) )
148 85 147 mpd ( 𝜑𝐵 = 𝐴 )
149 eqid 𝐵 = 𝐵
150 eqid ( 𝑊𝐵 ) = ( 𝑊𝐵 )
151 149 150 pm3.2i ( 𝐵 = 𝐵 ∧ ( 𝑊𝐵 ) = ( 𝑊𝐵 ) )
152 elinel1 ( 𝑥 ∈ ( 𝒫 𝐴 ∩ dom card ) → 𝑥 ∈ 𝒫 𝐴 )
153 ffvelrn ( ( 𝐻 : 𝒫 𝐴𝐴𝑥 ∈ 𝒫 𝐴 ) → ( 𝐻𝑥 ) ∈ 𝐴 )
154 79 152 153 syl2an ( ( 𝜑𝑥 ∈ ( 𝒫 𝐴 ∩ dom card ) ) → ( 𝐻𝑥 ) ∈ 𝐴 )
155 5 9 154 6 fpwwe ( 𝜑 → ( ( 𝐵 𝑊 ( 𝑊𝐵 ) ∧ ( 𝐻𝐵 ) ∈ 𝐵 ) ↔ ( 𝐵 = 𝐵 ∧ ( 𝑊𝐵 ) = ( 𝑊𝐵 ) ) ) )
156 151 155 mpbiri ( 𝜑 → ( 𝐵 𝑊 ( 𝑊𝐵 ) ∧ ( 𝐻𝐵 ) ∈ 𝐵 ) )
157 156 simpld ( 𝜑𝐵 𝑊 ( 𝑊𝐵 ) )
158 5 9 fpwwelem ( 𝜑 → ( 𝐵 𝑊 ( 𝑊𝐵 ) ↔ ( ( 𝐵𝐴 ∧ ( 𝑊𝐵 ) ⊆ ( 𝐵 × 𝐵 ) ) ∧ ( ( 𝑊𝐵 ) We 𝐵 ∧ ∀ 𝑦𝐵 ( 𝐻 ‘ ( ( 𝑊𝐵 ) “ { 𝑦 } ) ) = 𝑦 ) ) ) )
159 157 158 mpbid ( 𝜑 → ( ( 𝐵𝐴 ∧ ( 𝑊𝐵 ) ⊆ ( 𝐵 × 𝐵 ) ) ∧ ( ( 𝑊𝐵 ) We 𝐵 ∧ ∀ 𝑦𝐵 ( 𝐻 ‘ ( ( 𝑊𝐵 ) “ { 𝑦 } ) ) = 𝑦 ) ) )
160 159 simprld ( 𝜑 → ( 𝑊𝐵 ) We 𝐵 )
161 fvex ( 𝑊𝐵 ) ∈ V
162 weeq1 ( 𝑟 = ( 𝑊𝐵 ) → ( 𝑟 We 𝐵 ↔ ( 𝑊𝐵 ) We 𝐵 ) )
163 161 162 spcev ( ( 𝑊𝐵 ) We 𝐵 → ∃ 𝑟 𝑟 We 𝐵 )
164 160 163 syl ( 𝜑 → ∃ 𝑟 𝑟 We 𝐵 )
165 ween ( 𝐵 ∈ dom card ↔ ∃ 𝑟 𝑟 We 𝐵 )
166 164 165 sylibr ( 𝜑𝐵 ∈ dom card )
167 148 166 eqeltrrd ( 𝜑𝐴 ∈ dom card )
168 domtri2 ( ( ω ∈ dom card ∧ 𝐴 ∈ dom card ) → ( ω ≼ 𝐴 ↔ ¬ 𝐴 ≺ ω ) )
169 23 167 168 sylancr ( 𝜑 → ( ω ≼ 𝐴 ↔ ¬ 𝐴 ≺ ω ) )
170 infdju1 ( ω ≼ 𝐴 → ( 𝐴 ⊔ 1o ) ≈ 𝐴 )
171 169 170 syl6bir ( 𝜑 → ( ¬ 𝐴 ≺ ω → ( 𝐴 ⊔ 1o ) ≈ 𝐴 ) )
172 ensym ( ( 𝐴 ⊔ 1o ) ≈ 𝐴𝐴 ≈ ( 𝐴 ⊔ 1o ) )
173 171 172 syl6 ( 𝜑 → ( ¬ 𝐴 ≺ ω → 𝐴 ≈ ( 𝐴 ⊔ 1o ) ) )
174 20 173 mt3d ( 𝜑𝐴 ≺ ω )
175 2onn 2o ∈ ω
176 nnsdom ( 2o ∈ ω → 2o ≺ ω )
177 175 176 ax-mp 2o ≺ ω
178 djufi ( ( 𝐴 ≺ ω ∧ 2o ≺ ω ) → ( 𝐴 ⊔ 2o ) ≺ ω )
179 174 177 178 sylancl ( 𝜑 → ( 𝐴 ⊔ 2o ) ≺ ω )
180 isfinite ( ( 𝐴 ⊔ 2o ) ∈ Fin ↔ ( 𝐴 ⊔ 2o ) ≺ ω )
181 179 180 sylibr ( 𝜑 → ( 𝐴 ⊔ 2o ) ∈ Fin )
182 sssucid 1o ⊆ suc 1o
183 df-2o 2o = suc 1o
184 182 183 sseqtrri 1o ⊆ 2o
185 xpss2 ( 1o ⊆ 2o → ( { 1o } × 1o ) ⊆ ( { 1o } × 2o ) )
186 184 185 ax-mp ( { 1o } × 1o ) ⊆ ( { 1o } × 2o )
187 unss2 ( ( { 1o } × 1o ) ⊆ ( { 1o } × 2o ) → ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) ) ⊆ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 2o ) ) )
188 186 187 mp1i ( 𝜑 → ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) ) ⊆ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 2o ) ) )
189 ssun2 ( { 1o } × 2o ) ⊆ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 2o ) )
190 1oex 1o ∈ V
191 190 snid 1o ∈ { 1o }
192 190 sucid 1o ∈ suc 1o
193 192 183 eleqtrri 1o ∈ 2o
194 opelxpi ( ( 1o ∈ { 1o } ∧ 1o ∈ 2o ) → ⟨ 1o , 1o ⟩ ∈ ( { 1o } × 2o ) )
195 191 193 194 mp2an ⟨ 1o , 1o ⟩ ∈ ( { 1o } × 2o )
196 189 195 sselii ⟨ 1o , 1o ⟩ ∈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 2o ) )
197 1n0 1o ≠ ∅
198 197 neii ¬ 1o = ∅
199 opelxp1 ( ⟨ 1o , 1o ⟩ ∈ ( { ∅ } × 𝐴 ) → 1o ∈ { ∅ } )
200 elsni ( 1o ∈ { ∅ } → 1o = ∅ )
201 199 200 syl ( ⟨ 1o , 1o ⟩ ∈ ( { ∅ } × 𝐴 ) → 1o = ∅ )
202 198 201 mto ¬ ⟨ 1o , 1o ⟩ ∈ ( { ∅ } × 𝐴 )
203 1onn 1o ∈ ω
204 nnord ( 1o ∈ ω → Ord 1o )
205 ordirr ( Ord 1o → ¬ 1o ∈ 1o )
206 203 204 205 mp2b ¬ 1o ∈ 1o
207 opelxp2 ( ⟨ 1o , 1o ⟩ ∈ ( { 1o } × 1o ) → 1o ∈ 1o )
208 206 207 mto ¬ ⟨ 1o , 1o ⟩ ∈ ( { 1o } × 1o )
209 202 208 pm3.2ni ¬ ( ⟨ 1o , 1o ⟩ ∈ ( { ∅ } × 𝐴 ) ∨ ⟨ 1o , 1o ⟩ ∈ ( { 1o } × 1o ) )
210 elun ( ⟨ 1o , 1o ⟩ ∈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) ) ↔ ( ⟨ 1o , 1o ⟩ ∈ ( { ∅ } × 𝐴 ) ∨ ⟨ 1o , 1o ⟩ ∈ ( { 1o } × 1o ) ) )
211 209 210 mtbir ¬ ⟨ 1o , 1o ⟩ ∈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) )
212 ssnelpss ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) ) ⊆ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 2o ) ) → ( ( ⟨ 1o , 1o ⟩ ∈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 2o ) ) ∧ ¬ ⟨ 1o , 1o ⟩ ∈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) ) ) → ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) ) ⊊ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 2o ) ) ) )
213 196 211 212 mp2ani ( ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) ) ⊆ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 2o ) ) → ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) ) ⊊ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 2o ) ) )
214 188 213 syl ( 𝜑 → ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) ) ⊊ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 2o ) ) )
215 df-dju ( 𝐴 ⊔ 1o ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) )
216 df-dju ( 𝐴 ⊔ 2o ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 2o ) )
217 215 216 psseq12i ( ( 𝐴 ⊔ 1o ) ⊊ ( 𝐴 ⊔ 2o ) ↔ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 1o ) ) ⊊ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 2o ) ) )
218 214 217 sylibr ( 𝜑 → ( 𝐴 ⊔ 1o ) ⊊ ( 𝐴 ⊔ 2o ) )
219 php3 ( ( ( 𝐴 ⊔ 2o ) ∈ Fin ∧ ( 𝐴 ⊔ 1o ) ⊊ ( 𝐴 ⊔ 2o ) ) → ( 𝐴 ⊔ 1o ) ≺ ( 𝐴 ⊔ 2o ) )
220 181 218 219 syl2anc ( 𝜑 → ( 𝐴 ⊔ 1o ) ≺ ( 𝐴 ⊔ 2o ) )
221 canthp1lem1 ( 1o𝐴 → ( 𝐴 ⊔ 2o ) ≼ 𝒫 𝐴 )
222 1 221 syl ( 𝜑 → ( 𝐴 ⊔ 2o ) ≼ 𝒫 𝐴 )
223 sdomdomtr ( ( ( 𝐴 ⊔ 1o ) ≺ ( 𝐴 ⊔ 2o ) ∧ ( 𝐴 ⊔ 2o ) ≼ 𝒫 𝐴 ) → ( 𝐴 ⊔ 1o ) ≺ 𝒫 𝐴 )
224 220 222 223 syl2anc ( 𝜑 → ( 𝐴 ⊔ 1o ) ≺ 𝒫 𝐴 )
225 sdomnen ( ( 𝐴 ⊔ 1o ) ≺ 𝒫 𝐴 → ¬ ( 𝐴 ⊔ 1o ) ≈ 𝒫 𝐴 )
226 224 225 syl ( 𝜑 → ¬ ( 𝐴 ⊔ 1o ) ≈ 𝒫 𝐴 )
227 13 226 pm2.65i ¬ 𝜑