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 43 f1oeq1d 
 |-  ( b = dom O -> ( ( N ` b ) : ( b X. b ) -1-1-onto-> b <-> ( N ` dom O ) : ( b X. b ) -1-1-onto-> b ) )
45 xpeq12 
 |-  ( ( b = dom O /\ b = dom O ) -> ( b X. b ) = ( dom O X. dom O ) )
46 45 anidms 
 |-  ( b = dom O -> ( b X. b ) = ( dom O X. dom O ) )
47 46 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 ) )
48 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 ) )
49 44 47 48 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 ) )
50 42 49 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 ) ) )
51 5 adantr 
 |-  ( ( ph /\ ps ) -> A. b e. ( har ` ~P A ) ( _om C_ b -> ( N ` b ) : ( b X. b ) -1-1-onto-> b ) )
52 32 a1i 
 |-  ( ( ph /\ ps ) -> dom O e. On )
53 1 adantr 
 |-  ( ( ph /\ ps ) -> G : ~P A -1-1-> U_ n e. _om ( A ^m n ) )
54 omex 
 |-  _om e. _V
55 ovex 
 |-  ( A ^m n ) e. _V
56 54 55 iunex 
 |-  U_ n e. _om ( A ^m n ) e. _V
57 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 )
58 53 56 57 sylancl 
 |-  ( ( ph /\ ps ) -> ~P A e. _V )
59 pwexb 
 |-  ( A e. _V <-> ~P A e. _V )
60 58 59 sylibr 
 |-  ( ( ph /\ ps ) -> A e. _V )
61 simprl1 
 |-  ( ( ph /\ ( ( t C_ A /\ r C_ ( t X. t ) /\ r We t ) /\ _om ~<_ t ) ) -> t C_ A )
62 4 61 sylan2b 
 |-  ( ( ph /\ ps ) -> t C_ A )
63 ssdomg 
 |-  ( A e. _V -> ( t C_ A -> t ~<_ A ) )
64 60 62 63 sylc 
 |-  ( ( ph /\ ps ) -> t ~<_ A )
65 canth2g 
 |-  ( A e. _V -> A ~< ~P A )
66 sdomdom 
 |-  ( A ~< ~P A -> A ~<_ ~P A )
67 60 65 66 3syl 
 |-  ( ( ph /\ ps ) -> A ~<_ ~P A )
68 domtr 
 |-  ( ( t ~<_ A /\ A ~<_ ~P A ) -> t ~<_ ~P A )
69 64 67 68 syl2anc 
 |-  ( ( ph /\ ps ) -> t ~<_ ~P A )
70 endomtr 
 |-  ( ( dom O ~~ t /\ t ~<_ ~P A ) -> dom O ~<_ ~P A )
71 24 69 70 syl2anc 
 |-  ( ( ph /\ ps ) -> dom O ~<_ ~P A )
72 elharval 
 |-  ( dom O e. ( har ` ~P A ) <-> ( dom O e. On /\ dom O ~<_ ~P A ) )
73 52 71 72 sylanbrc 
 |-  ( ( ph /\ ps ) -> dom O e. ( har ` ~P A ) )
74 50 51 73 rspcdva 
 |-  ( ( ph /\ ps ) -> ( _om C_ dom O -> ( N ` dom O ) : ( dom O X. dom O ) -1-1-onto-> dom O ) )
75 41 74 mpd 
 |-  ( ( ph /\ ps ) -> ( N ` dom O ) : ( dom O X. dom O ) -1-1-onto-> dom O )
76 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 )
77 19 75 76 syl2anc 
 |-  ( ( ph /\ ps ) -> ( O o. ( N ` dom O ) ) : ( dom O X. dom O ) -1-1-onto-> t )
78 f1of 
 |-  ( O : dom O -1-1-onto-> t -> O : dom O --> t )
79 19 78 syl 
 |-  ( ( ph /\ ps ) -> O : dom O --> t )
80 79 feqmptd 
 |-  ( ( ph /\ ps ) -> O = ( u e. dom O |-> ( O ` u ) ) )
81 80 f1oeq1d 
 |-  ( ( ph /\ ps ) -> ( O : dom O -1-1-onto-> t <-> ( u e. dom O |-> ( O ` u ) ) : dom O -1-1-onto-> t ) )
82 19 81 mpbid 
 |-  ( ( ph /\ ps ) -> ( u e. dom O |-> ( O ` u ) ) : dom O -1-1-onto-> t )
83 79 feqmptd 
 |-  ( ( ph /\ ps ) -> O = ( v e. dom O |-> ( O ` v ) ) )
84 83 f1oeq1d 
 |-  ( ( ph /\ ps ) -> ( O : dom O -1-1-onto-> t <-> ( v e. dom O |-> ( O ` v ) ) : dom O -1-1-onto-> t ) )
85 19 84 mpbid 
 |-  ( ( ph /\ ps ) -> ( v e. dom O |-> ( O ` v ) ) : dom O -1-1-onto-> t )
86 82 85 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 ) )
87 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 ) ) )
88 7 87 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 ) )
89 86 88 sylibr 
 |-  ( ( ph /\ ps ) -> T : ( dom O X. dom O ) -1-1-onto-> ( t X. t ) )
90 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 ) )
91 89 90 syl 
 |-  ( ( ph /\ ps ) -> `' T : ( t X. t ) -1-1-onto-> ( dom O X. dom O ) )
92 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 )
93 77 91 92 syl2anc 
 |-  ( ( ph /\ ps ) -> ( ( O o. ( N ` dom O ) ) o. `' T ) : ( t X. t ) -1-1-onto-> t )
94 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 ) )
95 8 94 ax-mp 
 |-  ( P : ( t X. t ) -1-1-onto-> t <-> ( ( O o. ( N ` dom O ) ) o. `' T ) : ( t X. t ) -1-1-onto-> t )
96 93 95 sylibr 
 |-  ( ( ph /\ ps ) -> P : ( t X. t ) -1-1-onto-> t )
97 f1of1 
 |-  ( P : ( t X. t ) -1-1-onto-> t -> P : ( t X. t ) -1-1-> t )
98 96 97 syl 
 |-  ( ( ph /\ ps ) -> P : ( t X. t ) -1-1-> t )
99 f1of1 
 |-  ( O : dom O -1-1-onto-> t -> O : dom O -1-1-> t )
100 19 99 syl 
 |-  ( ( ph /\ ps ) -> O : dom O -1-1-> t )
101 f1ssres 
 |-  ( ( O : dom O -1-1-> t /\ _om C_ dom O ) -> ( O |` _om ) : _om -1-1-> t )
102 100 41 101 syl2anc 
 |-  ( ( ph /\ ps ) -> ( O |` _om ) : _om -1-1-> t )
103 f1f1orn 
 |-  ( ( O |` _om ) : _om -1-1-> t -> ( O |` _om ) : _om -1-1-onto-> ran ( O |` _om ) )
104 102 103 syl 
 |-  ( ( ph /\ ps ) -> ( O |` _om ) : _om -1-1-onto-> ran ( O |` _om ) )
105 79 41 feqresmpt 
 |-  ( ( ph /\ ps ) -> ( O |` _om ) = ( x e. _om |-> ( O ` x ) ) )
106 105 f1oeq1d 
 |-  ( ( ph /\ ps ) -> ( ( O |` _om ) : _om -1-1-onto-> ran ( O |` _om ) <-> ( x e. _om |-> ( O ` x ) ) : _om -1-1-onto-> ran ( O |` _om ) ) )
107 104 106 mpbid 
 |-  ( ( ph /\ ps ) -> ( x e. _om |-> ( O ` x ) ) : _om -1-1-onto-> ran ( O |` _om ) )
108 mptresid 
 |-  ( _I |` t ) = ( y e. t |-> y )
109 108 eqcomi 
 |-  ( y e. t |-> y ) = ( _I |` t )
110 f1oi 
 |-  ( _I |` t ) : t -1-1-onto-> t
111 f1oeq1 
 |-  ( ( y e. t |-> y ) = ( _I |` t ) -> ( ( y e. t |-> y ) : t -1-1-onto-> t <-> ( _I |` t ) : t -1-1-onto-> t ) )
112 110 111 mpbiri 
 |-  ( ( y e. t |-> y ) = ( _I |` t ) -> ( y e. t |-> y ) : t -1-1-onto-> t )
113 109 112 mp1i 
 |-  ( ( ph /\ ps ) -> ( y e. t |-> y ) : t -1-1-onto-> t )
114 107 113 xpf1o 
 |-  ( ( ph /\ ps ) -> ( x e. _om , y e. t |-> <. ( O ` x ) , y >. ) : ( _om X. t ) -1-1-onto-> ( ran ( O |` _om ) X. t ) )
115 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 ) ) )
116 11 115 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 ) )
117 114 116 sylibr 
 |-  ( ( ph /\ ps ) -> I : ( _om X. t ) -1-1-onto-> ( ran ( O |` _om ) X. t ) )
118 f1of1 
 |-  ( I : ( _om X. t ) -1-1-onto-> ( ran ( O |` _om ) X. t ) -> I : ( _om X. t ) -1-1-> ( ran ( O |` _om ) X. t ) )
119 117 118 syl 
 |-  ( ( ph /\ ps ) -> I : ( _om X. t ) -1-1-> ( ran ( O |` _om ) X. t ) )
120 f1f 
 |-  ( ( O |` _om ) : _om -1-1-> t -> ( O |` _om ) : _om --> t )
121 frn 
 |-  ( ( O |` _om ) : _om --> t -> ran ( O |` _om ) C_ t )
122 xpss1 
 |-  ( ran ( O |` _om ) C_ t -> ( ran ( O |` _om ) X. t ) C_ ( t X. t ) )
123 102 120 121 122 4syl 
 |-  ( ( ph /\ ps ) -> ( ran ( O |` _om ) X. t ) C_ ( t X. t ) )
124 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 ) )
125 119 123 124 syl2anc 
 |-  ( ( ph /\ ps ) -> I : ( _om X. t ) -1-1-> ( t X. t ) )
126 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 )
127 98 125 126 syl2anc 
 |-  ( ( ph /\ ps ) -> ( P o. I ) : ( _om X. t ) -1-1-> t )
128 13 a1i 
 |-  ( ( ph /\ ps ) -> t e. _V )
129 peano1 
 |-  (/) e. _om
130 129 a1i 
 |-  ( ( ph /\ ps ) -> (/) e. _om )
131 41 130 sseldd 
 |-  ( ( ph /\ ps ) -> (/) e. dom O )
132 79 131 ffvelrnd 
 |-  ( ( ph /\ ps ) -> ( O ` (/) ) e. t )
133 128 132 96 9 10 fseqenlem2 
 |-  ( ( ph /\ ps ) -> Q : U_ n e. _om ( t ^m n ) -1-1-> ( _om X. t ) )
134 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 )
135 127 133 134 syl2anc 
 |-  ( ( ph /\ ps ) -> ( ( P o. I ) o. Q ) : U_ n e. _om ( t ^m n ) -1-1-> t )
136 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 ) )
137 12 136 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 )
138 135 137 sylibr 
 |-  ( ( ph /\ ps ) -> K : U_ n e. _om ( t ^m n ) -1-1-> t )
139 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 ) ) ) } )
140 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 } ) ) )
141 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 ) ) }
142 141 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 ) ) }
143 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 ) ) }
144 1 2 3 4 138 139 140 142 143 pwfseqlem4 
 |-  -. ph