Metamath Proof Explorer

Theorem pwfseqlem4

Description: Lemma for pwfseq . Derive a final contradiction from the function F in pwfseqlem3 . Applying fpwwe2 to it, we get a certain maximal well-ordered subset Z , but the defining property ( Z F ( WZ ) ) e. Z contradicts our assumption on F , so we are reduced to the case of Z finite. This too is a contradiction, though, because Z and its preimage under ( WZ ) are distinct sets of the same cardinality and in a subset relation, which is impossible for finite sets. (Contributed by Mario Carneiro, 31-May-2015)

Ref Expression
Hypotheses pwfseqlem4.g 
|- ( ph -> G : ~P A -1-1-> U_ n e. _om ( A ^m n ) )
pwfseqlem4.x 
|- ( ph -> X C_ A )
pwfseqlem4.h 
|- ( ph -> H : _om -1-1-onto-> X )
pwfseqlem4.ps 
|- ( ps <-> ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) /\ _om ~<_ x ) )
pwfseqlem4.k 
|- ( ( ph /\ ps ) -> K : U_ n e. _om ( x ^m n ) -1-1-> x )
pwfseqlem4.d 
|- D = ( G ` { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } )
pwfseqlem4.f 
|- F = ( x e. _V , r e. _V |-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) )
pwfseqlem4.w 
|- W = { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. b e. a [. ( `' s " { b } ) / v ]. ( v F ( s i^i ( v X. v ) ) ) = b ) ) }
pwfseqlem4.z 
|- Z = U. dom W
Assertion pwfseqlem4 
|- -. ph

Proof

Step Hyp Ref Expression
1 pwfseqlem4.g 
 |-  ( ph -> G : ~P A -1-1-> U_ n e. _om ( A ^m n ) )
2 pwfseqlem4.x 
 |-  ( ph -> X C_ A )
3 pwfseqlem4.h 
 |-  ( ph -> H : _om -1-1-onto-> X )
4 pwfseqlem4.ps 
 |-  ( ps <-> ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) /\ _om ~<_ x ) )
5 pwfseqlem4.k 
 |-  ( ( ph /\ ps ) -> K : U_ n e. _om ( x ^m n ) -1-1-> x )
6 pwfseqlem4.d 
 |-  D = ( G ` { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } )
7 pwfseqlem4.f 
 |-  F = ( x e. _V , r e. _V |-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) )
8 pwfseqlem4.w 
 |-  W = { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. b e. a [. ( `' s " { b } ) / v ]. ( v F ( s i^i ( v X. v ) ) ) = b ) ) }
9 pwfseqlem4.z 
 |-  Z = U. dom W
10 eqid 
 |-  Z = Z
11 eqid 
 |-  ( W ` Z ) = ( W ` Z )
12 10 11 pm3.2i 
 |-  ( Z = Z /\ ( W ` Z ) = ( W ` Z ) )
13 omex 
 |-  _om e. _V
14 ovex 
 |-  ( A ^m n ) e. _V
15 13 14 iunex 
 |-  U_ n e. _om ( A ^m n ) e. _V
16 f1dmex 
 |-  ( ( G : ~P A -1-1-> U_ n e. _om ( A ^m n ) /\ U_ n e. _om ( A ^m n ) e. _V ) -> ~P A e. _V )
17 1 15 16 sylancl 
 |-  ( ph -> ~P A e. _V )
18 pwexb 
 |-  ( A e. _V <-> ~P A e. _V )
19 17 18 sylibr 
 |-  ( ph -> A e. _V )
20 1 2 3 4 5 6 7 pwfseqlem4a 
 |-  ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( a F s ) e. A )
21 8 19 20 9 fpwwe2 
 |-  ( ph -> ( ( Z W ( W ` Z ) /\ ( Z F ( W ` Z ) ) e. Z ) <-> ( Z = Z /\ ( W ` Z ) = ( W ` Z ) ) ) )
22 12 21 mpbiri 
 |-  ( ph -> ( Z W ( W ` Z ) /\ ( Z F ( W ` Z ) ) e. Z ) )
23 22 simprd 
 |-  ( ph -> ( Z F ( W ` Z ) ) e. Z )
24 22 simpld 
 |-  ( ph -> Z W ( W ` Z ) )
25 8 19 fpwwe2lem2 
 |-  ( ph -> ( Z W ( W ` Z ) <-> ( ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) ) /\ ( ( W ` Z ) We Z /\ A. b e. Z [. ( `' ( W ` Z ) " { b } ) / v ]. ( v F ( ( W ` Z ) i^i ( v X. v ) ) ) = b ) ) ) )
26 24 25 mpbid 
 |-  ( ph -> ( ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) ) /\ ( ( W ` Z ) We Z /\ A. b e. Z [. ( `' ( W ` Z ) " { b } ) / v ]. ( v F ( ( W ` Z ) i^i ( v X. v ) ) ) = b ) ) )
27 26 simpld 
 |-  ( ph -> ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) ) )
28 27 simpld 
 |-  ( ph -> Z C_ A )
29 19 28 ssexd 
 |-  ( ph -> Z e. _V )
30 sseq1 
 |-  ( a = Z -> ( a C_ A <-> Z C_ A ) )
31 id 
 |-  ( a = Z -> a = Z )
32 31 sqxpeqd 
 |-  ( a = Z -> ( a X. a ) = ( Z X. Z ) )
33 32 sseq2d 
 |-  ( a = Z -> ( ( W ` Z ) C_ ( a X. a ) <-> ( W ` Z ) C_ ( Z X. Z ) ) )
34 weeq2 
 |-  ( a = Z -> ( ( W ` Z ) We a <-> ( W ` Z ) We Z ) )
35 30 33 34 3anbi123d 
 |-  ( a = Z -> ( ( a C_ A /\ ( W ` Z ) C_ ( a X. a ) /\ ( W ` Z ) We a ) <-> ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) /\ ( W ` Z ) We Z ) ) )
36 35 anbi2d 
 |-  ( a = Z -> ( ( ph /\ ( a C_ A /\ ( W ` Z ) C_ ( a X. a ) /\ ( W ` Z ) We a ) ) <-> ( ph /\ ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) /\ ( W ` Z ) We Z ) ) ) )
37 id 
 |-  ( ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) /\ ( W ` Z ) We Z ) -> ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) /\ ( W ` Z ) We Z ) )
38 37 3expa 
 |-  ( ( ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) ) /\ ( W ` Z ) We Z ) -> ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) /\ ( W ` Z ) We Z ) )
39 38 adantrr 
 |-  ( ( ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) ) /\ ( ( W ` Z ) We Z /\ A. b e. Z [. ( `' ( W ` Z ) " { b } ) / v ]. ( v F ( ( W ` Z ) i^i ( v X. v ) ) ) = b ) ) -> ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) /\ ( W ` Z ) We Z ) )
40 26 39 syl 
 |-  ( ph -> ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) /\ ( W ` Z ) We Z ) )
41 40 pm4.71i 
 |-  ( ph <-> ( ph /\ ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) /\ ( W ` Z ) We Z ) ) )
42 36 41 bitr4di 
 |-  ( a = Z -> ( ( ph /\ ( a C_ A /\ ( W ` Z ) C_ ( a X. a ) /\ ( W ` Z ) We a ) ) <-> ph ) )
43 oveq1 
 |-  ( a = Z -> ( a F ( W ` Z ) ) = ( Z F ( W ` Z ) ) )
44 43 31 eleq12d 
 |-  ( a = Z -> ( ( a F ( W ` Z ) ) e. a <-> ( Z F ( W ` Z ) ) e. Z ) )
45 breq1 
 |-  ( a = Z -> ( a ~< _om <-> Z ~< _om ) )
46 44 45 imbi12d 
 |-  ( a = Z -> ( ( ( a F ( W ` Z ) ) e. a -> a ~< _om ) <-> ( ( Z F ( W ` Z ) ) e. Z -> Z ~< _om ) ) )
47 42 46 imbi12d 
 |-  ( a = Z -> ( ( ( ph /\ ( a C_ A /\ ( W ` Z ) C_ ( a X. a ) /\ ( W ` Z ) We a ) ) -> ( ( a F ( W ` Z ) ) e. a -> a ~< _om ) ) <-> ( ph -> ( ( Z F ( W ` Z ) ) e. Z -> Z ~< _om ) ) ) )
48 fvex 
 |-  ( W ` Z ) e. _V
49 sseq1 
 |-  ( s = ( W ` Z ) -> ( s C_ ( a X. a ) <-> ( W ` Z ) C_ ( a X. a ) ) )
50 weeq1 
 |-  ( s = ( W ` Z ) -> ( s We a <-> ( W ` Z ) We a ) )
51 49 50 3anbi23d 
 |-  ( s = ( W ` Z ) -> ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) <-> ( a C_ A /\ ( W ` Z ) C_ ( a X. a ) /\ ( W ` Z ) We a ) ) )
52 51 anbi2d 
 |-  ( s = ( W ` Z ) -> ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) <-> ( ph /\ ( a C_ A /\ ( W ` Z ) C_ ( a X. a ) /\ ( W ` Z ) We a ) ) ) )
53 oveq2 
 |-  ( s = ( W ` Z ) -> ( a F s ) = ( a F ( W ` Z ) ) )
54 53 eleq1d 
 |-  ( s = ( W ` Z ) -> ( ( a F s ) e. a <-> ( a F ( W ` Z ) ) e. a ) )
55 54 imbi1d 
 |-  ( s = ( W ` Z ) -> ( ( ( a F s ) e. a -> a ~< _om ) <-> ( ( a F ( W ` Z ) ) e. a -> a ~< _om ) ) )
56 52 55 imbi12d 
 |-  ( s = ( W ` Z ) -> ( ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( ( a F s ) e. a -> a ~< _om ) ) <-> ( ( ph /\ ( a C_ A /\ ( W ` Z ) C_ ( a X. a ) /\ ( W ` Z ) We a ) ) -> ( ( a F ( W ` Z ) ) e. a -> a ~< _om ) ) ) )
57 omelon 
 |-  _om e. On
58 onenon 
 |-  ( _om e. On -> _om e. dom card )
59 57 58 ax-mp 
 |-  _om e. dom card
60 simpr3 
 |-  ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> s We a )
61 60 19.8ad 
 |-  ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> E. s s We a )
62 ween 
 |-  ( a e. dom card <-> E. s s We a )
63 61 62 sylibr 
 |-  ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> a e. dom card )
64 domtri2 
 |-  ( ( _om e. dom card /\ a e. dom card ) -> ( _om ~<_ a <-> -. a ~< _om ) )
65 59 63 64 sylancr 
 |-  ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( _om ~<_ a <-> -. a ~< _om ) )
66 nfv 
 |-  F/ r ( ph /\ ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) )
67 nfcv 
 |-  F/_ r a
68 nfmpo2 
 |-  F/_ r ( x e. _V , r e. _V |-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) )
69 7 68 nfcxfr 
 |-  F/_ r F
70 nfcv 
 |-  F/_ r s
71 67 69 70 nfov 
 |-  F/_ r ( a F s )
72 71 nfel1 
 |-  F/ r ( a F s ) e. ( A \ a )
73 66 72 nfim 
 |-  F/ r ( ( ph /\ ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) ) -> ( a F s ) e. ( A \ a ) )
74 sseq1 
 |-  ( r = s -> ( r C_ ( a X. a ) <-> s C_ ( a X. a ) ) )
75 weeq1 
 |-  ( r = s -> ( r We a <-> s We a ) )
76 74 75 3anbi23d 
 |-  ( r = s -> ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) <-> ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) )
77 76 anbi1d 
 |-  ( r = s -> ( ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) <-> ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) ) )
78 77 anbi2d 
 |-  ( r = s -> ( ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) <-> ( ph /\ ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) ) ) )
79 oveq2 
 |-  ( r = s -> ( a F r ) = ( a F s ) )
80 79 eleq1d 
 |-  ( r = s -> ( ( a F r ) e. ( A \ a ) <-> ( a F s ) e. ( A \ a ) ) )
81 78 80 imbi12d 
 |-  ( r = s -> ( ( ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) -> ( a F r ) e. ( A \ a ) ) <-> ( ( ph /\ ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) ) -> ( a F s ) e. ( A \ a ) ) ) )
82 nfv 
 |-  F/ x ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) )
83 nfcv 
 |-  F/_ x a
84 nfmpo1 
 |-  F/_ x ( x e. _V , r e. _V |-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) )
85 7 84 nfcxfr 
 |-  F/_ x F
86 nfcv 
 |-  F/_ x r
87 83 85 86 nfov 
 |-  F/_ x ( a F r )
88 87 nfel1 
 |-  F/ x ( a F r ) e. ( A \ a )
89 82 88 nfim 
 |-  F/ x ( ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) -> ( a F r ) e. ( A \ a ) )
90 sseq1 
 |-  ( x = a -> ( x C_ A <-> a C_ A ) )
91 xpeq12 
 |-  ( ( x = a /\ x = a ) -> ( x X. x ) = ( a X. a ) )
92 91 anidms 
 |-  ( x = a -> ( x X. x ) = ( a X. a ) )
93 92 sseq2d 
 |-  ( x = a -> ( r C_ ( x X. x ) <-> r C_ ( a X. a ) ) )
94 weeq2 
 |-  ( x = a -> ( r We x <-> r We a ) )
95 90 93 94 3anbi123d 
 |-  ( x = a -> ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) <-> ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) ) )
96 breq2 
 |-  ( x = a -> ( _om ~<_ x <-> _om ~<_ a ) )
97 95 96 anbi12d 
 |-  ( x = a -> ( ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) /\ _om ~<_ x ) <-> ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) )
98 4 97 bitrid 
 |-  ( x = a -> ( ps <-> ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) )
99 98 anbi2d 
 |-  ( x = a -> ( ( ph /\ ps ) <-> ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) ) )
100 oveq1 
 |-  ( x = a -> ( x F r ) = ( a F r ) )
101 difeq2 
 |-  ( x = a -> ( A \ x ) = ( A \ a ) )
102 100 101 eleq12d 
 |-  ( x = a -> ( ( x F r ) e. ( A \ x ) <-> ( a F r ) e. ( A \ a ) ) )
103 99 102 imbi12d 
 |-  ( x = a -> ( ( ( ph /\ ps ) -> ( x F r ) e. ( A \ x ) ) <-> ( ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) -> ( a F r ) e. ( A \ a ) ) ) )
104 1 2 3 4 5 6 7 pwfseqlem3 
 |-  ( ( ph /\ ps ) -> ( x F r ) e. ( A \ x ) )
105 89 103 104 chvarfv 
 |-  ( ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) -> ( a F r ) e. ( A \ a ) )
106 73 81 105 chvarfv 
 |-  ( ( ph /\ ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) ) -> ( a F s ) e. ( A \ a ) )
107 106 eldifbd 
 |-  ( ( ph /\ ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) ) -> -. ( a F s ) e. a )
108 107 expr 
 |-  ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( _om ~<_ a -> -. ( a F s ) e. a ) )
109 65 108 sylbird 
 |-  ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( -. a ~< _om -> -. ( a F s ) e. a ) )
110 109 con4d 
 |-  ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( ( a F s ) e. a -> a ~< _om ) )
111 48 56 110 vtocl 
 |-  ( ( ph /\ ( a C_ A /\ ( W ` Z ) C_ ( a X. a ) /\ ( W ` Z ) We a ) ) -> ( ( a F ( W ` Z ) ) e. a -> a ~< _om ) )
112 47 111 vtoclg 
 |-  ( Z e. _V -> ( ph -> ( ( Z F ( W ` Z ) ) e. Z -> Z ~< _om ) ) )
113 29 112 mpcom 
 |-  ( ph -> ( ( Z F ( W ` Z ) ) e. Z -> Z ~< _om ) )
114 23 113 mpd 
 |-  ( ph -> Z ~< _om )
115 isfinite 
 |-  ( Z e. Fin <-> Z ~< _om )
116 114 115 sylibr 
 |-  ( ph -> Z e. Fin )
117 1 2 3 4 5 6 7 pwfseqlem2 
 |-  ( ( Z e. Fin /\ ( W ` Z ) e. _V ) -> ( Z F ( W ` Z ) ) = ( H ` ( card ` Z ) ) )
118 116 48 117 sylancl 
 |-  ( ph -> ( Z F ( W ` Z ) ) = ( H ` ( card ` Z ) ) )
119 118 23 eqeltrrd 
 |-  ( ph -> ( H ` ( card ` Z ) ) e. Z )
120 8 19 24 fpwwe2lem3 
 |-  ( ( ph /\ ( H ` ( card ` Z ) ) e. Z ) -> ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) F ( ( W ` Z ) i^i ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) X. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) ) = ( H ` ( card ` Z ) ) )
121 119 120 mpdan 
 |-  ( ph -> ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) F ( ( W ` Z ) i^i ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) X. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) ) = ( H ` ( card ` Z ) ) )
122 cnvimass 
 |-  ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C_ dom ( W ` Z )
123 27 simprd 
 |-  ( ph -> ( W ` Z ) C_ ( Z X. Z ) )
124 dmss 
 |-  ( ( W ` Z ) C_ ( Z X. Z ) -> dom ( W ` Z ) C_ dom ( Z X. Z ) )
125 123 124 syl 
 |-  ( ph -> dom ( W ` Z ) C_ dom ( Z X. Z ) )
126 dmxpss 
 |-  dom ( Z X. Z ) C_ Z
127 125 126 sstrdi 
 |-  ( ph -> dom ( W ` Z ) C_ Z )
128 122 127 sstrid 
 |-  ( ph -> ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C_ Z )
129 116 128 ssfid 
 |-  ( ph -> ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) e. Fin )
130 48 inex1 
 |-  ( ( W ` Z ) i^i ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) X. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) e. _V
131 1 2 3 4 5 6 7 pwfseqlem2 
 |-  ( ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) e. Fin /\ ( ( W ` Z ) i^i ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) X. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) e. _V ) -> ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) F ( ( W ` Z ) i^i ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) X. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) ) = ( H ` ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) )
132 129 130 131 sylancl 
 |-  ( ph -> ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) F ( ( W ` Z ) i^i ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) X. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) ) = ( H ` ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) )
133 121 132 eqtr3d 
 |-  ( ph -> ( H ` ( card ` Z ) ) = ( H ` ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) )
134 f1of1 
 |-  ( H : _om -1-1-onto-> X -> H : _om -1-1-> X )
135 3 134 syl 
 |-  ( ph -> H : _om -1-1-> X )
136 ficardom 
 |-  ( Z e. Fin -> ( card ` Z ) e. _om )
137 116 136 syl 
 |-  ( ph -> ( card ` Z ) e. _om )
138 ficardom 
 |-  ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) e. Fin -> ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) e. _om )
139 129 138 syl 
 |-  ( ph -> ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) e. _om )
140 f1fveq 
 |-  ( ( H : _om -1-1-> X /\ ( ( card ` Z ) e. _om /\ ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) e. _om ) ) -> ( ( H ` ( card ` Z ) ) = ( H ` ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) <-> ( card ` Z ) = ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) )
141 135 137 139 140 syl12anc 
 |-  ( ph -> ( ( H ` ( card ` Z ) ) = ( H ` ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) <-> ( card ` Z ) = ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) )
142 133 141 mpbid 
 |-  ( ph -> ( card ` Z ) = ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) )
143 142 eqcomd 
 |-  ( ph -> ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) = ( card ` Z ) )
144 finnum 
 |-  ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) e. Fin -> ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) e. dom card )
145 129 144 syl 
 |-  ( ph -> ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) e. dom card )
146 finnum 
 |-  ( Z e. Fin -> Z e. dom card )
147 116 146 syl 
 |-  ( ph -> Z e. dom card )
148 carden2 
 |-  ( ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) e. dom card /\ Z e. dom card ) -> ( ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) = ( card ` Z ) <-> ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~~ Z ) )
149 145 147 148 syl2anc 
 |-  ( ph -> ( ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) = ( card ` Z ) <-> ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~~ Z ) )
150 143 149 mpbid 
 |-  ( ph -> ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~~ Z )
151 dfpss2 
 |-  ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C. Z <-> ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C_ Z /\ -. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) = Z ) )
152 151 baib 
 |-  ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C_ Z -> ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C. Z <-> -. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) = Z ) )
153 128 152 syl 
 |-  ( ph -> ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C. Z <-> -. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) = Z ) )
154 php3 
 |-  ( ( Z e. Fin /\ ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C. Z ) -> ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~< Z )
155 sdomnen 
 |-  ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~< Z -> -. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~~ Z )
156 154 155 syl 
 |-  ( ( Z e. Fin /\ ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C. Z ) -> -. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~~ Z )
157 156 ex 
 |-  ( Z e. Fin -> ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C. Z -> -. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~~ Z ) )
158 116 157 syl 
 |-  ( ph -> ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C. Z -> -. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~~ Z ) )
159 153 158 sylbird 
 |-  ( ph -> ( -. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) = Z -> -. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~~ Z ) )
160 150 159 mt4d 
 |-  ( ph -> ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) = Z )
161 119 160 eleqtrrd 
 |-  ( ph -> ( H ` ( card ` Z ) ) e. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) )
162 fvex 
 |-  ( H ` ( card ` Z ) ) e. _V
163 162 eliniseg 
 |-  ( ( H ` ( card ` Z ) ) e. _V -> ( ( H ` ( card ` Z ) ) e. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) <-> ( H ` ( card ` Z ) ) ( W ` Z ) ( H ` ( card ` Z ) ) ) )
164 162 163 ax-mp 
 |-  ( ( H ` ( card ` Z ) ) e. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) <-> ( H ` ( card ` Z ) ) ( W ` Z ) ( H ` ( card ` Z ) ) )
165 161 164 sylib 
 |-  ( ph -> ( H ` ( card ` Z ) ) ( W ` Z ) ( H ` ( card ` Z ) ) )
166 26 simprd 
 |-  ( ph -> ( ( W ` Z ) We Z /\ A. b e. Z [. ( `' ( W ` Z ) " { b } ) / v ]. ( v F ( ( W ` Z ) i^i ( v X. v ) ) ) = b ) )
167 166 simpld 
 |-  ( ph -> ( W ` Z ) We Z )
168 weso 
 |-  ( ( W ` Z ) We Z -> ( W ` Z ) Or Z )
169 167 168 syl 
 |-  ( ph -> ( W ` Z ) Or Z )
170 sonr 
 |-  ( ( ( W ` Z ) Or Z /\ ( H ` ( card ` Z ) ) e. Z ) -> -. ( H ` ( card ` Z ) ) ( W ` Z ) ( H ` ( card ` Z ) ) )
171 169 119 170 syl2anc 
 |-  ( ph -> -. ( H ` ( card ` Z ) ) ( W ` Z ) ( H ` ( card ` Z ) ) )
172 165 171 pm2.65i 
 |-  -. ph