Metamath Proof Explorer

Theorem canthp1lem2

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

Ref Expression
Hypotheses canthp1lem2.1 
|- ( ph -> 1o ~< A )
canthp1lem2.2 
|- ( ph -> F : ~P A -1-1-onto-> ( A |_| 1o ) )
canthp1lem2.3 
|- ( ph -> G : ( ( A |_| 1o ) \ { ( F ` A ) } ) -1-1-onto-> A )
canthp1lem2.4 
|- H = ( ( G o. F ) o. ( x e. ~P A |-> if ( x = A , (/) , x ) ) )
canthp1lem2.5 
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( H ` ( `' r " { y } ) ) = y ) ) }
canthp1lem2.6 
|- B = U. dom W
Assertion canthp1lem2 
|- -. ph

Proof

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