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