Metamath Proof Explorer

Theorem pwfseqlem5

Description: Lemma for pwfseq . Although in some ways pwfseqlem4 is the "main" part of the proof, one last aspect which makes up a remark in the original text is by far the hardest part to formalize. The main proof relies on the existence of an injection K from the set of finite sequences on an infinite set x to x . Now this alone would not be difficult to prove; this is mostly the claim of fseqen . However, what is needed for the proof is acanonical injection on these sets, so we have to start from scratch pulling together explicit bijections from the lemmas.

If one attempts such a program, it will mostly go through, but there is one key step which is inherently nonconstructive, namely the proof of infxpen . The resolution is not obvious, but it turns out that reversing an infinite ordinal's Cantor normal form absorbs all the non-leading terms ( cnfcom3c ), which can be used to construct a pairing function explicitly using properties of the ordinal exponential ( infxpenc ). (Contributed by Mario Carneiro, 31-May-2015)

Ref Expression
Hypotheses pwfseqlem5.g 
|- ( ph -> G : ~P A -1-1-> U_ n e. _om ( A ^m n ) )
pwfseqlem5.x 
|- ( ph -> X C_ A )
pwfseqlem5.h 
|- ( ph -> H : _om -1-1-onto-> X )
pwfseqlem5.ps 
|- ( ps <-> ( ( t C_ A /\ r C_ ( t X. t ) /\ r We t ) /\ _om ~<_ t ) )
pwfseqlem5.n 
|- ( ph -> A. b e. ( har ` ~P A ) ( _om C_ b -> ( N ` b ) : ( b X. b ) -1-1-onto-> b ) )
pwfseqlem5.o 
|- O = OrdIso ( r , t )
pwfseqlem5.t 
|- T = ( u e. dom O , v e. dom O |-> <. ( O ` u ) , ( O ` v ) >. )
pwfseqlem5.p 
|- P = ( ( O o. ( N ` dom O ) ) o. `' T )
pwfseqlem5.s 
|- S = seqom ( ( k e. _V , f e. _V |-> ( x e. ( t ^m suc k ) |-> ( ( f ` ( x |` k ) ) P ( x ` k ) ) ) ) , { <. (/) , ( O ` (/) ) >. } )
pwfseqlem5.q 
|- Q = ( y e. U_ n e. _om ( t ^m n ) |-> <. dom y , ( ( S ` dom y ) ` y ) >. )
pwfseqlem5.i 
|- I = ( x e. _om , y e. t |-> <. ( O ` x ) , y >. )
pwfseqlem5.k 
|- K = ( ( P o. I ) o. Q )
Assertion pwfseqlem5 
|- -. ph

Proof

Step Hyp Ref Expression
1 pwfseqlem5.g 
 |-  ( ph -> G : ~P A -1-1-> U_ n e. _om ( A ^m n ) )
2 pwfseqlem5.x 
 |-  ( ph -> X C_ A )
3 pwfseqlem5.h 
 |-  ( ph -> H : _om -1-1-onto-> X )
4 pwfseqlem5.ps 
 |-  ( ps <-> ( ( t C_ A /\ r C_ ( t X. t ) /\ r We t ) /\ _om ~<_ t ) )
5 pwfseqlem5.n 
 |-  ( ph -> A. b e. ( har ` ~P A ) ( _om C_ b -> ( N ` b ) : ( b X. b ) -1-1-onto-> b ) )
6 pwfseqlem5.o 
 |-  O = OrdIso ( r , t )
7 pwfseqlem5.t 
 |-  T = ( u e. dom O , v e. dom O |-> <. ( O ` u ) , ( O ` v ) >. )
8 pwfseqlem5.p 
 |-  P = ( ( O o. ( N ` dom O ) ) o. `' T )
9 pwfseqlem5.s 
 |-  S = seqom ( ( k e. _V , f e. _V |-> ( x e. ( t ^m suc k ) |-> ( ( f ` ( x |` k ) ) P ( x ` k ) ) ) ) , { <. (/) , ( O ` (/) ) >. } )
10 pwfseqlem5.q 
 |-  Q = ( y e. U_ n e. _om ( t ^m n ) |-> <. dom y , ( ( S ` dom y ) ` y ) >. )
11 pwfseqlem5.i 
 |-  I = ( x e. _om , y e. t |-> <. ( O ` x ) , y >. )
12 pwfseqlem5.k 
 |-  K = ( ( P o. I ) o. Q )
13 vex 
 |-  t e. _V
14 simprl3 
 |-  ( ( ph /\ ( ( t C_ A /\ r C_ ( t X. t ) /\ r We t ) /\ _om ~<_ t ) ) -> r We t )
15 4 14 sylan2b 
 |-  ( ( ph /\ ps ) -> r We t )
16 6 oiiso 
 |-  ( ( t e. _V /\ r We t ) -> O Isom _E , r ( dom O , t ) )
17 13 15 16 sylancr 
 |-  ( ( ph /\ ps ) -> O Isom _E , r ( dom O , t ) )
18 isof1o 
 |-  ( O Isom _E , r ( dom O , t ) -> O : dom O -1-1-onto-> t )
19 17 18 syl 
 |-  ( ( ph /\ ps ) -> O : dom O -1-1-onto-> t )
20 cardom 
 |-  ( card ` _om ) = _om
21 simprr 
 |-  ( ( ph /\ ( ( t C_ A /\ r C_ ( t X. t ) /\ r We t ) /\ _om ~<_ t ) ) -> _om ~<_ t )
22 4 21 sylan2b 
 |-  ( ( ph /\ ps ) -> _om ~<_ t )
23 6 oien 
 |-  ( ( t e. _V /\ r We t ) -> dom O ~~ t )
24 13 15 23 sylancr 
 |-  ( ( ph /\ ps ) -> dom O ~~ t )
25 24 ensymd 
 |-  ( ( ph /\ ps ) -> t ~~ dom O )
26 domentr 
 |-  ( ( _om ~<_ t /\ t ~~ dom O ) -> _om ~<_ dom O )
27 22 25 26 syl2anc 
 |-  ( ( ph /\ ps ) -> _om ~<_ dom O )
28 omelon 
 |-  _om e. On
29 onenon 
 |-  ( _om e. On -> _om e. dom card )
30 28 29 ax-mp 
 |-  _om e. dom card
31 6 oion 
 |-  ( t e. _V -> dom O e. On )
32 31 elv 
 |-  dom O e. On
33 onenon 
 |-  ( dom O e. On -> dom O e. dom card )
34 32 33 mp1i 
 |-  ( ( ph /\ ps ) -> dom O e. dom card )
35 carddom2 
 |-  ( ( _om e. dom card /\ dom O e. dom card ) -> ( ( card ` _om ) C_ ( card ` dom O ) <-> _om ~<_ dom O ) )
36 30 34 35 sylancr 
 |-  ( ( ph /\ ps ) -> ( ( card ` _om ) C_ ( card ` dom O ) <-> _om ~<_ dom O ) )
37 27 36 mpbird 
 |-  ( ( ph /\ ps ) -> ( card ` _om ) C_ ( card ` dom O ) )
38 20 37 eqsstrrid 
 |-  ( ( ph /\ ps ) -> _om C_ ( card ` dom O ) )
39 cardonle 
 |-  ( dom O e. On -> ( card ` dom O ) C_ dom O )
40 32 39 mp1i 
 |-  ( ( ph /\ ps ) -> ( card ` dom O ) C_ dom O )
41 38 40 sstrd 
 |-  ( ( ph /\ ps ) -> _om C_ dom O )
42 sseq2 
 |-  ( b = dom O -> ( _om C_ b <-> _om C_ dom O ) )
43 fveq2 
 |-  ( b = dom O -> ( N ` b ) = ( N ` dom O ) )
44 f1oeq1 
 |-  ( ( N ` b ) = ( N ` dom O ) -> ( ( N ` b ) : ( b X. b ) -1-1-onto-> b <-> ( N ` dom O ) : ( b X. b ) -1-1-onto-> b ) )
45 43 44 syl 
 |-  ( b = dom O -> ( ( N ` b ) : ( b X. b ) -1-1-onto-> b <-> ( N ` dom O ) : ( b X. b ) -1-1-onto-> b ) )
46 xpeq12 
 |-  ( ( b = dom O /\ b = dom O ) -> ( b X. b ) = ( dom O X. dom O ) )
47 46 anidms 
 |-  ( b = dom O -> ( b X. b ) = ( dom O X. dom O ) )
48 47 f1oeq2d 
 |-  ( b = dom O -> ( ( N ` dom O ) : ( b X. b ) -1-1-onto-> b <-> ( N ` dom O ) : ( dom O X. dom O ) -1-1-onto-> b ) )
49 f1oeq3 
 |-  ( b = dom O -> ( ( N ` dom O ) : ( dom O X. dom O ) -1-1-onto-> b <-> ( N ` dom O ) : ( dom O X. dom O ) -1-1-onto-> dom O ) )
50 45 48 49 3bitrd 
 |-  ( b = dom O -> ( ( N ` b ) : ( b X. b ) -1-1-onto-> b <-> ( N ` dom O ) : ( dom O X. dom O ) -1-1-onto-> dom O ) )
51 42 50 imbi12d 
 |-  ( b = dom O -> ( ( _om C_ b -> ( N ` b ) : ( b X. b ) -1-1-onto-> b ) <-> ( _om C_ dom O -> ( N ` dom O ) : ( dom O X. dom O ) -1-1-onto-> dom O ) ) )
52 5 adantr 
 |-  ( ( ph /\ ps ) -> A. b e. ( har ` ~P A ) ( _om C_ b -> ( N ` b ) : ( b X. b ) -1-1-onto-> b ) )
53 32 a1i 
 |-  ( ( ph /\ ps ) -> dom O e. On )
54 1 adantr 
 |-  ( ( ph /\ ps ) -> G : ~P A -1-1-> U_ n e. _om ( A ^m n ) )
55 omex 
 |-  _om e. _V
56 ovex 
 |-  ( A ^m n ) e. _V
57 55 56 iunex 
 |-  U_ n e. _om ( A ^m n ) e. _V
58 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 )
59 54 57 58 sylancl 
 |-  ( ( ph /\ ps ) -> ~P A e. _V )
60 pwexb 
 |-  ( A e. _V <-> ~P A e. _V )
61 59 60 sylibr 
 |-  ( ( ph /\ ps ) -> A e. _V )
62 simprl1 
 |-  ( ( ph /\ ( ( t C_ A /\ r C_ ( t X. t ) /\ r We t ) /\ _om ~<_ t ) ) -> t C_ A )
63 4 62 sylan2b 
 |-  ( ( ph /\ ps ) -> t C_ A )
64 ssdomg 
 |-  ( A e. _V -> ( t C_ A -> t ~<_ A ) )
65 61 63 64 sylc 
 |-  ( ( ph /\ ps ) -> t ~<_ A )
66 canth2g 
 |-  ( A e. _V -> A ~< ~P A )
67 sdomdom 
 |-  ( A ~< ~P A -> A ~<_ ~P A )
68 61 66 67 3syl 
 |-  ( ( ph /\ ps ) -> A ~<_ ~P A )
69 domtr 
 |-  ( ( t ~<_ A /\ A ~<_ ~P A ) -> t ~<_ ~P A )
70 65 68 69 syl2anc 
 |-  ( ( ph /\ ps ) -> t ~<_ ~P A )
71 endomtr 
 |-  ( ( dom O ~~ t /\ t ~<_ ~P A ) -> dom O ~<_ ~P A )
72 24 70 71 syl2anc 
 |-  ( ( ph /\ ps ) -> dom O ~<_ ~P A )
73 elharval 
 |-  ( dom O e. ( har ` ~P A ) <-> ( dom O e. On /\ dom O ~<_ ~P A ) )
74 53 72 73 sylanbrc 
 |-  ( ( ph /\ ps ) -> dom O e. ( har ` ~P A ) )
75 51 52 74 rspcdva 
 |-  ( ( ph /\ ps ) -> ( _om C_ dom O -> ( N ` dom O ) : ( dom O X. dom O ) -1-1-onto-> dom O ) )
76 41 75 mpd 
 |-  ( ( ph /\ ps ) -> ( N ` dom O ) : ( dom O X. dom O ) -1-1-onto-> dom O )
77 f1oco 
 |-  ( ( O : dom O -1-1-onto-> t /\ ( N ` dom O ) : ( dom O X. dom O ) -1-1-onto-> dom O ) -> ( O o. ( N ` dom O ) ) : ( dom O X. dom O ) -1-1-onto-> t )
78 19 76 77 syl2anc 
 |-  ( ( ph /\ ps ) -> ( O o. ( N ` dom O ) ) : ( dom O X. dom O ) -1-1-onto-> t )
79 f1of 
 |-  ( O : dom O -1-1-onto-> t -> O : dom O --> t )
80 19 79 syl 
 |-  ( ( ph /\ ps ) -> O : dom O --> t )
81 80 feqmptd 
 |-  ( ( ph /\ ps ) -> O = ( u e. dom O |-> ( O ` u ) ) )
82 f1oeq1 
 |-  ( O = ( u e. dom O |-> ( O ` u ) ) -> ( O : dom O -1-1-onto-> t <-> ( u e. dom O |-> ( O ` u ) ) : dom O -1-1-onto-> t ) )
83 81 82 syl 
 |-  ( ( ph /\ ps ) -> ( O : dom O -1-1-onto-> t <-> ( u e. dom O |-> ( O ` u ) ) : dom O -1-1-onto-> t ) )
84 19 83 mpbid 
 |-  ( ( ph /\ ps ) -> ( u e. dom O |-> ( O ` u ) ) : dom O -1-1-onto-> t )
85 80 feqmptd 
 |-  ( ( ph /\ ps ) -> O = ( v e. dom O |-> ( O ` v ) ) )
86 f1oeq1 
 |-  ( O = ( v e. dom O |-> ( O ` v ) ) -> ( O : dom O -1-1-onto-> t <-> ( v e. dom O |-> ( O ` v ) ) : dom O -1-1-onto-> t ) )
87 85 86 syl 
 |-  ( ( ph /\ ps ) -> ( O : dom O -1-1-onto-> t <-> ( v e. dom O |-> ( O ` v ) ) : dom O -1-1-onto-> t ) )
88 19 87 mpbid 
 |-  ( ( ph /\ ps ) -> ( v e. dom O |-> ( O ` v ) ) : dom O -1-1-onto-> t )
89 84 88 xpf1o 
 |-  ( ( ph /\ ps ) -> ( u e. dom O , v e. dom O |-> <. ( O ` u ) , ( O ` v ) >. ) : ( dom O X. dom O ) -1-1-onto-> ( t X. t ) )
90 f1oeq1 
 |-  ( T = ( u e. dom O , v e. dom O |-> <. ( O ` u ) , ( O ` v ) >. ) -> ( T : ( dom O X. dom O ) -1-1-onto-> ( t X. t ) <-> ( u e. dom O , v e. dom O |-> <. ( O ` u ) , ( O ` v ) >. ) : ( dom O X. dom O ) -1-1-onto-> ( t X. t ) ) )
91 7 90 ax-mp 
 |-  ( T : ( dom O X. dom O ) -1-1-onto-> ( t X. t ) <-> ( u e. dom O , v e. dom O |-> <. ( O ` u ) , ( O ` v ) >. ) : ( dom O X. dom O ) -1-1-onto-> ( t X. t ) )
92 89 91 sylibr 
 |-  ( ( ph /\ ps ) -> T : ( dom O X. dom O ) -1-1-onto-> ( t X. t ) )
93 f1ocnv 
 |-  ( T : ( dom O X. dom O ) -1-1-onto-> ( t X. t ) -> `' T : ( t X. t ) -1-1-onto-> ( dom O X. dom O ) )
94 92 93 syl 
 |-  ( ( ph /\ ps ) -> `' T : ( t X. t ) -1-1-onto-> ( dom O X. dom O ) )
95 f1oco 
 |-  ( ( ( O o. ( N ` dom O ) ) : ( dom O X. dom O ) -1-1-onto-> t /\ `' T : ( t X. t ) -1-1-onto-> ( dom O X. dom O ) ) -> ( ( O o. ( N ` dom O ) ) o. `' T ) : ( t X. t ) -1-1-onto-> t )
96 78 94 95 syl2anc 
 |-  ( ( ph /\ ps ) -> ( ( O o. ( N ` dom O ) ) o. `' T ) : ( t X. t ) -1-1-onto-> t )
97 f1oeq1 
 |-  ( P = ( ( O o. ( N ` dom O ) ) o. `' T ) -> ( P : ( t X. t ) -1-1-onto-> t <-> ( ( O o. ( N ` dom O ) ) o. `' T ) : ( t X. t ) -1-1-onto-> t ) )
98 8 97 ax-mp 
 |-  ( P : ( t X. t ) -1-1-onto-> t <-> ( ( O o. ( N ` dom O ) ) o. `' T ) : ( t X. t ) -1-1-onto-> t )
99 96 98 sylibr 
 |-  ( ( ph /\ ps ) -> P : ( t X. t ) -1-1-onto-> t )
100 f1of1 
 |-  ( P : ( t X. t ) -1-1-onto-> t -> P : ( t X. t ) -1-1-> t )
101 99 100 syl 
 |-  ( ( ph /\ ps ) -> P : ( t X. t ) -1-1-> t )
102 f1of1 
 |-  ( O : dom O -1-1-onto-> t -> O : dom O -1-1-> t )
103 19 102 syl 
 |-  ( ( ph /\ ps ) -> O : dom O -1-1-> t )
104 f1ssres 
 |-  ( ( O : dom O -1-1-> t /\ _om C_ dom O ) -> ( O |` _om ) : _om -1-1-> t )
105 103 41 104 syl2anc 
 |-  ( ( ph /\ ps ) -> ( O |` _om ) : _om -1-1-> t )
106 f1f1orn 
 |-  ( ( O |` _om ) : _om -1-1-> t -> ( O |` _om ) : _om -1-1-onto-> ran ( O |` _om ) )
107 105 106 syl 
 |-  ( ( ph /\ ps ) -> ( O |` _om ) : _om -1-1-onto-> ran ( O |` _om ) )
108 80 41 feqresmpt 
 |-  ( ( ph /\ ps ) -> ( O |` _om ) = ( x e. _om |-> ( O ` x ) ) )
109 f1oeq1 
 |-  ( ( O |` _om ) = ( x e. _om |-> ( O ` x ) ) -> ( ( O |` _om ) : _om -1-1-onto-> ran ( O |` _om ) <-> ( x e. _om |-> ( O ` x ) ) : _om -1-1-onto-> ran ( O |` _om ) ) )
110 108 109 syl 
 |-  ( ( ph /\ ps ) -> ( ( O |` _om ) : _om -1-1-onto-> ran ( O |` _om ) <-> ( x e. _om |-> ( O ` x ) ) : _om -1-1-onto-> ran ( O |` _om ) ) )
111 107 110 mpbid 
 |-  ( ( ph /\ ps ) -> ( x e. _om |-> ( O ` x ) ) : _om -1-1-onto-> ran ( O |` _om ) )
112 mptresid 
 |-  ( _I |` t ) = ( y e. t |-> y )
113 112 eqcomi 
 |-  ( y e. t |-> y ) = ( _I |` t )
114 f1oi 
 |-  ( _I |` t ) : t -1-1-onto-> t
115 f1oeq1 
 |-  ( ( y e. t |-> y ) = ( _I |` t ) -> ( ( y e. t |-> y ) : t -1-1-onto-> t <-> ( _I |` t ) : t -1-1-onto-> t ) )
116 114 115 mpbiri 
 |-  ( ( y e. t |-> y ) = ( _I |` t ) -> ( y e. t |-> y ) : t -1-1-onto-> t )
117 113 116 mp1i 
 |-  ( ( ph /\ ps ) -> ( y e. t |-> y ) : t -1-1-onto-> t )
118 111 117 xpf1o 
 |-  ( ( ph /\ ps ) -> ( x e. _om , y e. t |-> <. ( O ` x ) , y >. ) : ( _om X. t ) -1-1-onto-> ( ran ( O |` _om ) X. t ) )
119 f1oeq1 
 |-  ( I = ( x e. _om , y e. t |-> <. ( O ` x ) , y >. ) -> ( I : ( _om X. t ) -1-1-onto-> ( ran ( O |` _om ) X. t ) <-> ( x e. _om , y e. t |-> <. ( O ` x ) , y >. ) : ( _om X. t ) -1-1-onto-> ( ran ( O |` _om ) X. t ) ) )
120 11 119 ax-mp 
 |-  ( I : ( _om X. t ) -1-1-onto-> ( ran ( O |` _om ) X. t ) <-> ( x e. _om , y e. t |-> <. ( O ` x ) , y >. ) : ( _om X. t ) -1-1-onto-> ( ran ( O |` _om ) X. t ) )
121 118 120 sylibr 
 |-  ( ( ph /\ ps ) -> I : ( _om X. t ) -1-1-onto-> ( ran ( O |` _om ) X. t ) )
122 f1of1 
 |-  ( I : ( _om X. t ) -1-1-onto-> ( ran ( O |` _om ) X. t ) -> I : ( _om X. t ) -1-1-> ( ran ( O |` _om ) X. t ) )
123 121 122 syl 
 |-  ( ( ph /\ ps ) -> I : ( _om X. t ) -1-1-> ( ran ( O |` _om ) X. t ) )
124 f1f 
 |-  ( ( O |` _om ) : _om -1-1-> t -> ( O |` _om ) : _om --> t )
125 frn 
 |-  ( ( O |` _om ) : _om --> t -> ran ( O |` _om ) C_ t )
126 xpss1 
 |-  ( ran ( O |` _om ) C_ t -> ( ran ( O |` _om ) X. t ) C_ ( t X. t ) )
127 105 124 125 126 4syl 
 |-  ( ( ph /\ ps ) -> ( ran ( O |` _om ) X. t ) C_ ( t X. t ) )
128 f1ss 
 |-  ( ( I : ( _om X. t ) -1-1-> ( ran ( O |` _om ) X. t ) /\ ( ran ( O |` _om ) X. t ) C_ ( t X. t ) ) -> I : ( _om X. t ) -1-1-> ( t X. t ) )
129 123 127 128 syl2anc 
 |-  ( ( ph /\ ps ) -> I : ( _om X. t ) -1-1-> ( t X. t ) )
130 f1co 
 |-  ( ( P : ( t X. t ) -1-1-> t /\ I : ( _om X. t ) -1-1-> ( t X. t ) ) -> ( P o. I ) : ( _om X. t ) -1-1-> t )
131 101 129 130 syl2anc 
 |-  ( ( ph /\ ps ) -> ( P o. I ) : ( _om X. t ) -1-1-> t )
132 13 a1i 
 |-  ( ( ph /\ ps ) -> t e. _V )
133 peano1 
 |-  (/) e. _om
134 133 a1i 
 |-  ( ( ph /\ ps ) -> (/) e. _om )
135 41 134 sseldd 
 |-  ( ( ph /\ ps ) -> (/) e. dom O )
136 80 135 ffvelrnd 
 |-  ( ( ph /\ ps ) -> ( O ` (/) ) e. t )
137 132 136 99 9 10 fseqenlem2 
 |-  ( ( ph /\ ps ) -> Q : U_ n e. _om ( t ^m n ) -1-1-> ( _om X. t ) )
138 f1co 
 |-  ( ( ( P o. I ) : ( _om X. t ) -1-1-> t /\ Q : U_ n e. _om ( t ^m n ) -1-1-> ( _om X. t ) ) -> ( ( P o. I ) o. Q ) : U_ n e. _om ( t ^m n ) -1-1-> t )
139 131 137 138 syl2anc 
 |-  ( ( ph /\ ps ) -> ( ( P o. I ) o. Q ) : U_ n e. _om ( t ^m n ) -1-1-> t )
140 f1eq1 
 |-  ( K = ( ( P o. I ) o. Q ) -> ( K : U_ n e. _om ( t ^m n ) -1-1-> t <-> ( ( P o. I ) o. Q ) : U_ n e. _om ( t ^m n ) -1-1-> t ) )
141 12 140 ax-mp 
 |-  ( K : U_ n e. _om ( t ^m n ) -1-1-> t <-> ( ( P o. I ) o. Q ) : U_ n e. _om ( t ^m n ) -1-1-> t )
142 139 141 sylibr 
 |-  ( ( ph /\ ps ) -> K : U_ n e. _om ( t ^m n ) -1-1-> t )
143 eqid 
 |-  ( G ` { i e. t | ( ( `' K ` i ) e. ran G /\ -. i e. ( `' G ` ( `' K ` i ) ) ) } ) = ( G ` { i e. t | ( ( `' K ` i ) e. ran G /\ -. i e. ( `' G ` ( `' K ` i ) ) ) } )
144 eqid 
 |-  ( t e. _V , r e. _V |-> if ( t e. Fin , ( H ` ( card ` t ) ) , ( ( G ` { i e. t | ( ( `' K ` i ) e. ran G /\ -. i e. ( `' G ` ( `' K ` i ) ) ) } ) ` |^| { z e. _om | -. ( ( G ` { i e. t | ( ( `' K ` i ) e. ran G /\ -. i e. ( `' G ` ( `' K ` i ) ) ) } ) ` z ) e. t } ) ) ) = ( t e. _V , r e. _V |-> if ( t e. Fin , ( H ` ( card ` t ) ) , ( ( G ` { i e. t | ( ( `' K ` i ) e. ran G /\ -. i e. ( `' G ` ( `' K ` i ) ) ) } ) ` |^| { z e. _om | -. ( ( G ` { i e. t | ( ( `' K ` i ) e. ran G /\ -. i e. ( `' G ` ( `' K ` i ) ) ) } ) ` z ) e. t } ) ) )
145 eqid 
 |-  { <. c , d >. | ( ( c C_ A /\ d C_ ( c X. c ) ) /\ ( d We c /\ A. m e. c [. ( `' d " { m } ) / j ]. ( j ( t e. _V , r e. _V |-> if ( t e. Fin , ( H ` ( card ` t ) ) , ( ( G ` { i e. t | ( ( `' K ` i ) e. ran G /\ -. i e. ( `' G ` ( `' K ` i ) ) ) } ) ` |^| { z e. _om | -. ( ( G ` { i e. t | ( ( `' K ` i ) e. ran G /\ -. i e. ( `' G ` ( `' K ` i ) ) ) } ) ` z ) e. t } ) ) ) ( d i^i ( j X. j ) ) ) = m ) ) } = { <. c , d >. | ( ( c C_ A /\ d C_ ( c X. c ) ) /\ ( d We c /\ A. m e. c [. ( `' d " { m } ) / j ]. ( j ( t e. _V , r e. _V |-> if ( t e. Fin , ( H ` ( card ` t ) ) , ( ( G ` { i e. t | ( ( `' K ` i ) e. ran G /\ -. i e. ( `' G ` ( `' K ` i ) ) ) } ) ` |^| { z e. _om | -. ( ( G ` { i e. t | ( ( `' K ` i ) e. ran G /\ -. i e. ( `' G ` ( `' K ` i ) ) ) } ) ` z ) e. t } ) ) ) ( d i^i ( j X. j ) ) ) = m ) ) }
146 145 fpwwe2cbv 
 |-  { <. c , d >. | ( ( c C_ A /\ d C_ ( c X. c ) ) /\ ( d We c /\ A. m e. c [. ( `' d " { m } ) / j ]. ( j ( t e. _V , r e. _V |-> if ( t e. Fin , ( H ` ( card ` t ) ) , ( ( G ` { i e. t | ( ( `' K ` i ) e. ran G /\ -. i e. ( `' G ` ( `' K ` i ) ) ) } ) ` |^| { z e. _om | -. ( ( G ` { i e. t | ( ( `' K ` i ) e. ran G /\ -. i e. ( `' G ` ( `' K ` i ) ) ) } ) ` z ) e. t } ) ) ) ( d i^i ( j X. j ) ) ) = m ) ) } = { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. b e. a [. ( `' s " { b } ) / w ]. ( w ( t e. _V , r e. _V |-> if ( t e. Fin , ( H ` ( card ` t ) ) , ( ( G ` { i e. t | ( ( `' K ` i ) e. ran G /\ -. i e. ( `' G ` ( `' K ` i ) ) ) } ) ` |^| { z e. _om | -. ( ( G ` { i e. t | ( ( `' K ` i ) e. ran G /\ -. i e. ( `' G ` ( `' K ` i ) ) ) } ) ` z ) e. t } ) ) ) ( s i^i ( w X. w ) ) ) = b ) ) }
147 eqid 
 |-  U. dom { <. c , d >. | ( ( c C_ A /\ d C_ ( c X. c ) ) /\ ( d We c /\ A. m e. c [. ( `' d " { m } ) / j ]. ( j ( t e. _V , r e. _V |-> if ( t e. Fin , ( H ` ( card ` t ) ) , ( ( G ` { i e. t | ( ( `' K ` i ) e. ran G /\ -. i e. ( `' G ` ( `' K ` i ) ) ) } ) ` |^| { z e. _om | -. ( ( G ` { i e. t | ( ( `' K ` i ) e. ran G /\ -. i e. ( `' G ` ( `' K ` i ) ) ) } ) ` z ) e. t } ) ) ) ( d i^i ( j X. j ) ) ) = m ) ) } = U. dom { <. c , d >. | ( ( c C_ A /\ d C_ ( c X. c ) ) /\ ( d We c /\ A. m e. c [. ( `' d " { m } ) / j ]. ( j ( t e. _V , r e. _V |-> if ( t e. Fin , ( H ` ( card ` t ) ) , ( ( G ` { i e. t | ( ( `' K ` i ) e. ran G /\ -. i e. ( `' G ` ( `' K ` i ) ) ) } ) ` |^| { z e. _om | -. ( ( G ` { i e. t | ( ( `' K ` i ) e. ran G /\ -. i e. ( `' G ` ( `' K ` i ) ) ) } ) ` z ) e. t } ) ) ) ( d i^i ( j X. j ) ) ) = m ) ) }
148 1 2 3 4 142 143 144 146 147 pwfseqlem4 
 |-  -. ph