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) (Proof shortened by Matthew House, 10-Sep-2025)

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 simpld 
 |-  ( ph -> Z W ( W ` Z ) )
24 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 ) ) ) )
25 23 24 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 ) ) )
26 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 ) )
27 26 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 ) )
28 27 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 ) )
29 25 28 syl 
 |-  ( ph -> ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) /\ ( W ` Z ) We Z ) )
30 22 simprd 
 |-  ( ph -> ( Z F ( W ` Z ) ) e. Z )
31 25 simpld 
 |-  ( ph -> ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) ) )
32 31 simpld 
 |-  ( ph -> Z C_ A )
33 19 32 ssexd 
 |-  ( ph -> Z e. _V )
34 fvexd 
 |-  ( ph -> ( W ` Z ) e. _V )
35 simpl 
 |-  ( ( a = Z /\ s = ( W ` Z ) ) -> a = Z )
36 35 sseq1d 
 |-  ( ( a = Z /\ s = ( W ` Z ) ) -> ( a C_ A <-> Z C_ A ) )
37 simpr 
 |-  ( ( a = Z /\ s = ( W ` Z ) ) -> s = ( W ` Z ) )
38 35 sqxpeqd 
 |-  ( ( a = Z /\ s = ( W ` Z ) ) -> ( a X. a ) = ( Z X. Z ) )
39 37 38 sseq12d 
 |-  ( ( a = Z /\ s = ( W ` Z ) ) -> ( s C_ ( a X. a ) <-> ( W ` Z ) C_ ( Z X. Z ) ) )
40 37 35 weeq12d 
 |-  ( ( a = Z /\ s = ( W ` Z ) ) -> ( s We a <-> ( W ` Z ) We Z ) )
41 36 39 40 3anbi123d 
 |-  ( ( a = Z /\ s = ( W ` Z ) ) -> ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) <-> ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) /\ ( W ` Z ) We Z ) ) )
42 oveq12 
 |-  ( ( a = Z /\ s = ( W ` Z ) ) -> ( a F s ) = ( Z F ( W ` Z ) ) )
43 42 35 eleq12d 
 |-  ( ( a = Z /\ s = ( W ` Z ) ) -> ( ( a F s ) e. a <-> ( Z F ( W ` Z ) ) e. Z ) )
44 35 breq1d 
 |-  ( ( a = Z /\ s = ( W ` Z ) ) -> ( a ~< _om <-> Z ~< _om ) )
45 43 44 imbi12d 
 |-  ( ( a = Z /\ s = ( W ` Z ) ) -> ( ( ( a F s ) e. a -> a ~< _om ) <-> ( ( Z F ( W ` Z ) ) e. Z -> Z ~< _om ) ) )
46 41 45 imbi12d 
 |-  ( ( a = Z /\ s = ( W ` Z ) ) -> ( ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) -> ( ( a F s ) e. a -> a ~< _om ) ) <-> ( ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) /\ ( W ` Z ) We Z ) -> ( ( Z F ( W ` Z ) ) e. Z -> Z ~< _om ) ) ) )
47 omelon 
 |-  _om e. On
48 onenon 
 |-  ( _om e. On -> _om e. dom card )
49 47 48 ax-mp 
 |-  _om e. dom card
50 simpr3 
 |-  ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> s We a )
51 50 19.8ad 
 |-  ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> E. s s We a )
52 ween 
 |-  ( a e. dom card <-> E. s s We a )
53 51 52 sylibr 
 |-  ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> a e. dom card )
54 domtri2 
 |-  ( ( _om e. dom card /\ a e. dom card ) -> ( _om ~<_ a <-> -. a ~< _om ) )
55 49 53 54 sylancr 
 |-  ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( _om ~<_ a <-> -. a ~< _om ) )
56 nfv 
 |-  F/ r ( ph /\ ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) )
57 nfcv 
 |-  F/_ r a
58 nfmpo2 
 |-  F/_ r ( x e. _V , r e. _V |-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) )
59 7 58 nfcxfr 
 |-  F/_ r F
60 nfcv 
 |-  F/_ r s
61 57 59 60 nfov 
 |-  F/_ r ( a F s )
62 61 nfel1 
 |-  F/ r ( a F s ) e. ( A \ a )
63 56 62 nfim 
 |-  F/ r ( ( ph /\ ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) ) -> ( a F s ) e. ( A \ a ) )
64 sseq1 
 |-  ( r = s -> ( r C_ ( a X. a ) <-> s C_ ( a X. a ) ) )
65 weeq1 
 |-  ( r = s -> ( r We a <-> s We a ) )
66 64 65 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 ) ) )
67 66 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 ) ) )
68 67 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 ) ) ) )
69 oveq2 
 |-  ( r = s -> ( a F r ) = ( a F s ) )
70 69 eleq1d 
 |-  ( r = s -> ( ( a F r ) e. ( A \ a ) <-> ( a F s ) e. ( A \ a ) ) )
71 68 70 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 ) ) ) )
72 nfv 
 |-  F/ x ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) )
73 nfcv 
 |-  F/_ x a
74 nfmpo1 
 |-  F/_ x ( x e. _V , r e. _V |-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) )
75 7 74 nfcxfr 
 |-  F/_ x F
76 nfcv 
 |-  F/_ x r
77 73 75 76 nfov 
 |-  F/_ x ( a F r )
78 77 nfel1 
 |-  F/ x ( a F r ) e. ( A \ a )
79 72 78 nfim 
 |-  F/ x ( ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) -> ( a F r ) e. ( A \ a ) )
80 sseq1 
 |-  ( x = a -> ( x C_ A <-> a C_ A ) )
81 xpeq12 
 |-  ( ( x = a /\ x = a ) -> ( x X. x ) = ( a X. a ) )
82 81 anidms 
 |-  ( x = a -> ( x X. x ) = ( a X. a ) )
83 82 sseq2d 
 |-  ( x = a -> ( r C_ ( x X. x ) <-> r C_ ( a X. a ) ) )
84 weeq2 
 |-  ( x = a -> ( r We x <-> r We a ) )
85 80 83 84 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 ) ) )
86 breq2 
 |-  ( x = a -> ( _om ~<_ x <-> _om ~<_ a ) )
87 85 86 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 ) ) )
88 4 87 bitrid 
 |-  ( x = a -> ( ps <-> ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) )
89 88 anbi2d 
 |-  ( x = a -> ( ( ph /\ ps ) <-> ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) ) )
90 oveq1 
 |-  ( x = a -> ( x F r ) = ( a F r ) )
91 difeq2 
 |-  ( x = a -> ( A \ x ) = ( A \ a ) )
92 90 91 eleq12d 
 |-  ( x = a -> ( ( x F r ) e. ( A \ x ) <-> ( a F r ) e. ( A \ a ) ) )
93 89 92 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 ) ) ) )
94 1 2 3 4 5 6 7 pwfseqlem3 
 |-  ( ( ph /\ ps ) -> ( x F r ) e. ( A \ x ) )
95 79 93 94 chvarfv 
 |-  ( ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) -> ( a F r ) e. ( A \ a ) )
96 63 71 95 chvarfv 
 |-  ( ( ph /\ ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) ) -> ( a F s ) e. ( A \ a ) )
97 96 eldifbd 
 |-  ( ( ph /\ ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) ) -> -. ( a F s ) e. a )
98 97 expr 
 |-  ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( _om ~<_ a -> -. ( a F s ) e. a ) )
99 55 98 sylbird 
 |-  ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( -. a ~< _om -> -. ( a F s ) e. a ) )
100 99 con4d 
 |-  ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( ( a F s ) e. a -> a ~< _om ) )
101 100 ex 
 |-  ( ph -> ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) -> ( ( a F s ) e. a -> a ~< _om ) ) )
102 33 34 46 101 vtocl2d 
 |-  ( ph -> ( ( Z C_ A /\ ( W ` Z ) C_ ( Z X. Z ) /\ ( W ` Z ) We Z ) -> ( ( Z F ( W ` Z ) ) e. Z -> Z ~< _om ) ) )
103 29 30 102 mp2d 
 |-  ( ph -> Z ~< _om )
104 isfinite 
 |-  ( Z e. Fin <-> Z ~< _om )
105 103 104 sylibr 
 |-  ( ph -> Z e. Fin )
106 fvex 
 |-  ( W ` Z ) e. _V
107 1 2 3 4 5 6 7 pwfseqlem2 
 |-  ( ( Z e. Fin /\ ( W ` Z ) e. _V ) -> ( Z F ( W ` Z ) ) = ( H ` ( card ` Z ) ) )
108 105 106 107 sylancl 
 |-  ( ph -> ( Z F ( W ` Z ) ) = ( H ` ( card ` Z ) ) )
109 108 30 eqeltrrd 
 |-  ( ph -> ( H ` ( card ` Z ) ) e. Z )
110 8 19 23 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 ) ) )
111 109 110 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 ) ) )
112 cnvimass 
 |-  ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C_ dom ( W ` Z )
113 31 simprd 
 |-  ( ph -> ( W ` Z ) C_ ( Z X. Z ) )
114 dmss 
 |-  ( ( W ` Z ) C_ ( Z X. Z ) -> dom ( W ` Z ) C_ dom ( Z X. Z ) )
115 113 114 syl 
 |-  ( ph -> dom ( W ` Z ) C_ dom ( Z X. Z ) )
116 dmxpss 
 |-  dom ( Z X. Z ) C_ Z
117 115 116 sstrdi 
 |-  ( ph -> dom ( W ` Z ) C_ Z )
118 112 117 sstrid 
 |-  ( ph -> ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C_ Z )
119 105 118 ssfid 
 |-  ( ph -> ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) e. Fin )
120 106 inex1 
 |-  ( ( W ` Z ) i^i ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) X. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) e. _V
121 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 ) ) } ) ) ) )
122 119 120 121 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 ) ) } ) ) ) )
123 111 122 eqtr3d 
 |-  ( ph -> ( H ` ( card ` Z ) ) = ( H ` ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) )
124 f1of1 
 |-  ( H : _om -1-1-onto-> X -> H : _om -1-1-> X )
125 3 124 syl 
 |-  ( ph -> H : _om -1-1-> X )
126 ficardom 
 |-  ( Z e. Fin -> ( card ` Z ) e. _om )
127 105 126 syl 
 |-  ( ph -> ( card ` Z ) e. _om )
128 ficardom 
 |-  ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) e. Fin -> ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) e. _om )
129 119 128 syl 
 |-  ( ph -> ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) e. _om )
130 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 ) ) } ) ) ) )
131 125 127 129 130 syl12anc 
 |-  ( ph -> ( ( H ` ( card ` Z ) ) = ( H ` ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) <-> ( card ` Z ) = ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) ) )
132 123 131 mpbid 
 |-  ( ph -> ( card ` Z ) = ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) )
133 132 eqcomd 
 |-  ( ph -> ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) = ( card ` Z ) )
134 finnum 
 |-  ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) e. Fin -> ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) e. dom card )
135 119 134 syl 
 |-  ( ph -> ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) e. dom card )
136 finnum 
 |-  ( Z e. Fin -> Z e. dom card )
137 105 136 syl 
 |-  ( ph -> Z e. dom card )
138 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 ) )
139 135 137 138 syl2anc 
 |-  ( ph -> ( ( card ` ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ) = ( card ` Z ) <-> ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~~ Z ) )
140 133 139 mpbid 
 |-  ( ph -> ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~~ Z )
141 dfpss2 
 |-  ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C. Z <-> ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C_ Z /\ -. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) = Z ) )
142 141 baib 
 |-  ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C_ Z -> ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C. Z <-> -. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) = Z ) )
143 118 142 syl 
 |-  ( ph -> ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C. Z <-> -. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) = Z ) )
144 php3 
 |-  ( ( Z e. Fin /\ ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C. Z ) -> ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~< Z )
145 sdomnen 
 |-  ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~< Z -> -. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~~ Z )
146 144 145 syl 
 |-  ( ( Z e. Fin /\ ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C. Z ) -> -. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~~ Z )
147 146 ex 
 |-  ( Z e. Fin -> ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C. Z -> -. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~~ Z ) )
148 105 147 syl 
 |-  ( ph -> ( ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) C. Z -> -. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~~ Z ) )
149 143 148 sylbird 
 |-  ( ph -> ( -. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) = Z -> -. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) ~~ Z ) )
150 140 149 mt4d 
 |-  ( ph -> ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) = Z )
151 109 150 eleqtrrd 
 |-  ( ph -> ( H ` ( card ` Z ) ) e. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) )
152 fvex 
 |-  ( H ` ( card ` Z ) ) e. _V
153 152 eliniseg 
 |-  ( ( H ` ( card ` Z ) ) e. _V -> ( ( H ` ( card ` Z ) ) e. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) <-> ( H ` ( card ` Z ) ) ( W ` Z ) ( H ` ( card ` Z ) ) ) )
154 152 153 ax-mp 
 |-  ( ( H ` ( card ` Z ) ) e. ( `' ( W ` Z ) " { ( H ` ( card ` Z ) ) } ) <-> ( H ` ( card ` Z ) ) ( W ` Z ) ( H ` ( card ` Z ) ) )
155 151 154 sylib 
 |-  ( ph -> ( H ` ( card ` Z ) ) ( W ` Z ) ( H ` ( card ` Z ) ) )
156 25 simprd 
 |-  ( ph -> ( ( W ` Z ) We Z /\ A. b e. Z [. ( `' ( W ` Z ) " { b } ) / v ]. ( v F ( ( W ` Z ) i^i ( v X. v ) ) ) = b ) )
157 156 simpld 
 |-  ( ph -> ( W ` Z ) We Z )
158 weso 
 |-  ( ( W ` Z ) We Z -> ( W ` Z ) Or Z )
159 157 158 syl 
 |-  ( ph -> ( W ` Z ) Or Z )
160 sonr 
 |-  ( ( ( W ` Z ) Or Z /\ ( H ` ( card ` Z ) ) e. Z ) -> -. ( H ` ( card ` Z ) ) ( W ` Z ) ( H ` ( card ` Z ) ) )
161 159 109 160 syl2anc 
 |-  ( ph -> -. ( H ` ( card ` Z ) ) ( W ` Z ) ( H ` ( card ` Z ) ) )
162 155 161 pm2.65i 
 |-  -. ph