This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cantnf

Description: The Cantor Normal Form theorem. The function ( A CNF B ) , which maps a finitely supported function from B to A to the sum ( ( A ^o f ( a 1 ) ) o. a 1 ) +o ( ( A ^o f ( a 2 ) ) o. a 2 ) +o ... over all indices a < B such that f ( a ) is nonzero, is an order isomorphism from the ordering T of finitely supported functions to the set ( A ^o B ) under the natural order. Setting A = _om and letting B be arbitrarily large, the surjectivity of this function implies that every ordinal has a Cantor normal form (and injectivity, together with coherence cantnfres , implies that such a representation is unique). (Contributed by Mario Carneiro, 28-May-2015)

Ref Expression
Hypotheses cantnfs.s 
|- S = dom ( A CNF B )
cantnfs.a 
|- ( ph -> A e. On )
cantnfs.b 
|- ( ph -> B e. On )
oemapval.t 
|- T = { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) }
Assertion cantnf 
|- ( ph -> ( A CNF B ) Isom T , _E ( S , ( A ^o B ) ) )

Proof

Step Hyp Ref Expression
1 cantnfs.s 
 |-  S = dom ( A CNF B )
2 cantnfs.a 
 |-  ( ph -> A e. On )
3 cantnfs.b 
 |-  ( ph -> B e. On )
4 oemapval.t 
 |-  T = { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) }
5 1 2 3 4 oemapso 
 |-  ( ph -> T Or S )
6 oecl 
 |-  ( ( A e. On /\ B e. On ) -> ( A ^o B ) e. On )
7 2 3 6 syl2anc 
 |-  ( ph -> ( A ^o B ) e. On )
8 eloni 
 |-  ( ( A ^o B ) e. On -> Ord ( A ^o B ) )
9 7 8 syl 
 |-  ( ph -> Ord ( A ^o B ) )
10 ordwe 
 |-  ( Ord ( A ^o B ) -> _E We ( A ^o B ) )
11 weso 
 |-  ( _E We ( A ^o B ) -> _E Or ( A ^o B ) )
12 sopo 
 |-  ( _E Or ( A ^o B ) -> _E Po ( A ^o B ) )
13 9 10 11 12 4syl 
 |-  ( ph -> _E Po ( A ^o B ) )
14 1 2 3 cantnff 
 |-  ( ph -> ( A CNF B ) : S --> ( A ^o B ) )
15 14 frnd 
 |-  ( ph -> ran ( A CNF B ) C_ ( A ^o B ) )
16 onss 
 |-  ( ( A ^o B ) e. On -> ( A ^o B ) C_ On )
17 7 16 syl 
 |-  ( ph -> ( A ^o B ) C_ On )
18 17 sseld 
 |-  ( ph -> ( t e. ( A ^o B ) -> t e. On ) )
19 eleq1w 
 |-  ( t = y -> ( t e. ( A ^o B ) <-> y e. ( A ^o B ) ) )
20 eleq1w 
 |-  ( t = y -> ( t e. ran ( A CNF B ) <-> y e. ran ( A CNF B ) ) )
21 19 20 imbi12d 
 |-  ( t = y -> ( ( t e. ( A ^o B ) -> t e. ran ( A CNF B ) ) <-> ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) ) )
22 21 imbi2d 
 |-  ( t = y -> ( ( ph -> ( t e. ( A ^o B ) -> t e. ran ( A CNF B ) ) ) <-> ( ph -> ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) ) ) )
23 r19.21v 
 |-  ( A. y e. t ( ph -> ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) ) <-> ( ph -> A. y e. t ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) ) )
24 ordelss 
 |-  ( ( Ord ( A ^o B ) /\ t e. ( A ^o B ) ) -> t C_ ( A ^o B ) )
25 9 24 sylan 
 |-  ( ( ph /\ t e. ( A ^o B ) ) -> t C_ ( A ^o B ) )
26 25 sselda 
 |-  ( ( ( ph /\ t e. ( A ^o B ) ) /\ y e. t ) -> y e. ( A ^o B ) )
27 pm5.5 
 |-  ( y e. ( A ^o B ) -> ( ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) <-> y e. ran ( A CNF B ) ) )
28 26 27 syl 
 |-  ( ( ( ph /\ t e. ( A ^o B ) ) /\ y e. t ) -> ( ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) <-> y e. ran ( A CNF B ) ) )
29 28 ralbidva 
 |-  ( ( ph /\ t e. ( A ^o B ) ) -> ( A. y e. t ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) <-> A. y e. t y e. ran ( A CNF B ) ) )
30 dfss3 
 |-  ( t C_ ran ( A CNF B ) <-> A. y e. t y e. ran ( A CNF B ) )
31 29 30 bitr4di 
 |-  ( ( ph /\ t e. ( A ^o B ) ) -> ( A. y e. t ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) <-> t C_ ran ( A CNF B ) ) )
32 eleq1 
 |-  ( t = (/) -> ( t e. ran ( A CNF B ) <-> (/) e. ran ( A CNF B ) ) )
33 2 adantr 
 |-  ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> A e. On )
34 33 adantr 
 |-  ( ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) /\ t =/= (/) ) -> A e. On )
35 3 adantr 
 |-  ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> B e. On )
36 35 adantr 
 |-  ( ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) /\ t =/= (/) ) -> B e. On )
37 simplrl 
 |-  ( ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) /\ t =/= (/) ) -> t e. ( A ^o B ) )
38 simplrr 
 |-  ( ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) /\ t =/= (/) ) -> t C_ ran ( A CNF B ) )
39 7 adantr 
 |-  ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( A ^o B ) e. On )
40 simprl 
 |-  ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> t e. ( A ^o B ) )
41 onelon 
 |-  ( ( ( A ^o B ) e. On /\ t e. ( A ^o B ) ) -> t e. On )
42 39 40 41 syl2anc 
 |-  ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> t e. On )
43 on0eln0 
 |-  ( t e. On -> ( (/) e. t <-> t =/= (/) ) )
44 42 43 syl 
 |-  ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( (/) e. t <-> t =/= (/) ) )
45 44 biimpar 
 |-  ( ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) /\ t =/= (/) ) -> (/) e. t )
46 eqid 
 |-  U. |^| { c e. On | t e. ( A ^o c ) } = U. |^| { c e. On | t e. ( A ^o c ) }
47 eqid 
 |-  ( iota d E. a e. On E. b e. ( A ^o U. |^| { c e. On | t e. ( A ^o c ) } ) ( d = <. a , b >. /\ ( ( ( A ^o U. |^| { c e. On | t e. ( A ^o c ) } ) .o a ) +o b ) = t ) ) = ( iota d E. a e. On E. b e. ( A ^o U. |^| { c e. On | t e. ( A ^o c ) } ) ( d = <. a , b >. /\ ( ( ( A ^o U. |^| { c e. On | t e. ( A ^o c ) } ) .o a ) +o b ) = t ) )
48 eqid 
 |-  ( 1st ` ( iota d E. a e. On E. b e. ( A ^o U. |^| { c e. On | t e. ( A ^o c ) } ) ( d = <. a , b >. /\ ( ( ( A ^o U. |^| { c e. On | t e. ( A ^o c ) } ) .o a ) +o b ) = t ) ) ) = ( 1st ` ( iota d E. a e. On E. b e. ( A ^o U. |^| { c e. On | t e. ( A ^o c ) } ) ( d = <. a , b >. /\ ( ( ( A ^o U. |^| { c e. On | t e. ( A ^o c ) } ) .o a ) +o b ) = t ) ) )
49 eqid 
 |-  ( 2nd ` ( iota d E. a e. On E. b e. ( A ^o U. |^| { c e. On | t e. ( A ^o c ) } ) ( d = <. a , b >. /\ ( ( ( A ^o U. |^| { c e. On | t e. ( A ^o c ) } ) .o a ) +o b ) = t ) ) ) = ( 2nd ` ( iota d E. a e. On E. b e. ( A ^o U. |^| { c e. On | t e. ( A ^o c ) } ) ( d = <. a , b >. /\ ( ( ( A ^o U. |^| { c e. On | t e. ( A ^o c ) } ) .o a ) +o b ) = t ) ) )
50 1 34 36 4 37 38 45 46 47 48 49 cantnflem4 
 |-  ( ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) /\ t =/= (/) ) -> t e. ran ( A CNF B ) )
51 fczsupp0 
 |-  ( ( B X. { (/) } ) supp (/) ) = (/)
52 51 eqcomi 
 |-  (/) = ( ( B X. { (/) } ) supp (/) )
53 oieq2 
 |-  ( (/) = ( ( B X. { (/) } ) supp (/) ) -> OrdIso ( _E , (/) ) = OrdIso ( _E , ( ( B X. { (/) } ) supp (/) ) ) )
54 52 53 ax-mp 
 |-  OrdIso ( _E , (/) ) = OrdIso ( _E , ( ( B X. { (/) } ) supp (/) ) )
55 ne0i 
 |-  ( t e. ( A ^o B ) -> ( A ^o B ) =/= (/) )
56 55 ad2antrl 
 |-  ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( A ^o B ) =/= (/) )
57 oveq1 
 |-  ( A = (/) -> ( A ^o B ) = ( (/) ^o B ) )
58 57 neeq1d 
 |-  ( A = (/) -> ( ( A ^o B ) =/= (/) <-> ( (/) ^o B ) =/= (/) ) )
59 56 58 syl5ibcom 
 |-  ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( A = (/) -> ( (/) ^o B ) =/= (/) ) )
60 59 necon2d 
 |-  ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( ( (/) ^o B ) = (/) -> A =/= (/) ) )
61 on0eln0 
 |-  ( B e. On -> ( (/) e. B <-> B =/= (/) ) )
62 oe0m1 
 |-  ( B e. On -> ( (/) e. B <-> ( (/) ^o B ) = (/) ) )
63 61 62 bitr3d 
 |-  ( B e. On -> ( B =/= (/) <-> ( (/) ^o B ) = (/) ) )
64 35 63 syl 
 |-  ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( B =/= (/) <-> ( (/) ^o B ) = (/) ) )
65 on0eln0 
 |-  ( A e. On -> ( (/) e. A <-> A =/= (/) ) )
66 33 65 syl 
 |-  ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( (/) e. A <-> A =/= (/) ) )
67 60 64 66 3imtr4d 
 |-  ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( B =/= (/) -> (/) e. A ) )
68 ne0i 
 |-  ( y e. B -> B =/= (/) )
69 67 68 impel 
 |-  ( ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) /\ y e. B ) -> (/) e. A )
70 fconstmpt 
 |-  ( B X. { (/) } ) = ( y e. B |-> (/) )
71 69 70 fmptd 
 |-  ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( B X. { (/) } ) : B --> A )
72 0ex 
 |-  (/) e. _V
73 72 a1i 
 |-  ( ph -> (/) e. _V )
74 3 73 fczfsuppd 
 |-  ( ph -> ( B X. { (/) } ) finSupp (/) )
75 74 adantr 
 |-  ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( B X. { (/) } ) finSupp (/) )
76 1 2 3 cantnfs 
 |-  ( ph -> ( ( B X. { (/) } ) e. S <-> ( ( B X. { (/) } ) : B --> A /\ ( B X. { (/) } ) finSupp (/) ) ) )
77 76 adantr 
 |-  ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( ( B X. { (/) } ) e. S <-> ( ( B X. { (/) } ) : B --> A /\ ( B X. { (/) } ) finSupp (/) ) ) )
78 71 75 77 mpbir2and 
 |-  ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( B X. { (/) } ) e. S )
79 eqid 
 |-  seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , (/) ) ` k ) ) .o ( ( B X. { (/) } ) ` ( OrdIso ( _E , (/) ) ` k ) ) ) +o z ) ) , (/) ) = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , (/) ) ` k ) ) .o ( ( B X. { (/) } ) ` ( OrdIso ( _E , (/) ) ` k ) ) ) +o z ) ) , (/) )
80 1 33 35 54 78 79 cantnfval 
 |-  ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( ( A CNF B ) ` ( B X. { (/) } ) ) = ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , (/) ) ` k ) ) .o ( ( B X. { (/) } ) ` ( OrdIso ( _E , (/) ) ` k ) ) ) +o z ) ) , (/) ) ` dom OrdIso ( _E , (/) ) ) )
81 we0 
 |-  _E We (/)
82 eqid 
 |-  OrdIso ( _E , (/) ) = OrdIso ( _E , (/) )
83 82 oien 
 |-  ( ( (/) e. _V /\ _E We (/) ) -> dom OrdIso ( _E , (/) ) ~~ (/) )
84 72 81 83 mp2an 
 |-  dom OrdIso ( _E , (/) ) ~~ (/)
85 en0 
 |-  ( dom OrdIso ( _E , (/) ) ~~ (/) <-> dom OrdIso ( _E , (/) ) = (/) )
86 84 85 mpbi 
 |-  dom OrdIso ( _E , (/) ) = (/)
87 86 fveq2i 
 |-  ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , (/) ) ` k ) ) .o ( ( B X. { (/) } ) ` ( OrdIso ( _E , (/) ) ` k ) ) ) +o z ) ) , (/) ) ` dom OrdIso ( _E , (/) ) ) = ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , (/) ) ` k ) ) .o ( ( B X. { (/) } ) ` ( OrdIso ( _E , (/) ) ` k ) ) ) +o z ) ) , (/) ) ` (/) )
88 79 seqom0g 
 |-  ( (/) e. _V -> ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , (/) ) ` k ) ) .o ( ( B X. { (/) } ) ` ( OrdIso ( _E , (/) ) ` k ) ) ) +o z ) ) , (/) ) ` (/) ) = (/) )
89 72 88 ax-mp 
 |-  ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , (/) ) ` k ) ) .o ( ( B X. { (/) } ) ` ( OrdIso ( _E , (/) ) ` k ) ) ) +o z ) ) , (/) ) ` (/) ) = (/)
90 87 89 eqtri 
 |-  ( seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( OrdIso ( _E , (/) ) ` k ) ) .o ( ( B X. { (/) } ) ` ( OrdIso ( _E , (/) ) ` k ) ) ) +o z ) ) , (/) ) ` dom OrdIso ( _E , (/) ) ) = (/)
91 80 90 eqtrdi 
 |-  ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( ( A CNF B ) ` ( B X. { (/) } ) ) = (/) )
92 14 adantr 
 |-  ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( A CNF B ) : S --> ( A ^o B ) )
93 92 ffnd 
 |-  ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( A CNF B ) Fn S )
94 fnfvelrn 
 |-  ( ( ( A CNF B ) Fn S /\ ( B X. { (/) } ) e. S ) -> ( ( A CNF B ) ` ( B X. { (/) } ) ) e. ran ( A CNF B ) )
95 93 78 94 syl2anc 
 |-  ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( ( A CNF B ) ` ( B X. { (/) } ) ) e. ran ( A CNF B ) )
96 91 95 eqeltrrd 
 |-  ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> (/) e. ran ( A CNF B ) )
97 32 50 96 pm2.61ne 
 |-  ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> t e. ran ( A CNF B ) )
98 97 expr 
 |-  ( ( ph /\ t e. ( A ^o B ) ) -> ( t C_ ran ( A CNF B ) -> t e. ran ( A CNF B ) ) )
99 31 98 sylbid 
 |-  ( ( ph /\ t e. ( A ^o B ) ) -> ( A. y e. t ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) -> t e. ran ( A CNF B ) ) )
100 99 ex 
 |-  ( ph -> ( t e. ( A ^o B ) -> ( A. y e. t ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) -> t e. ran ( A CNF B ) ) ) )
101 100 com23 
 |-  ( ph -> ( A. y e. t ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) -> ( t e. ( A ^o B ) -> t e. ran ( A CNF B ) ) ) )
102 101 a2i 
 |-  ( ( ph -> A. y e. t ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) ) -> ( ph -> ( t e. ( A ^o B ) -> t e. ran ( A CNF B ) ) ) )
103 102 a1i 
 |-  ( t e. On -> ( ( ph -> A. y e. t ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) ) -> ( ph -> ( t e. ( A ^o B ) -> t e. ran ( A CNF B ) ) ) ) )
104 23 103 biimtrid 
 |-  ( t e. On -> ( A. y e. t ( ph -> ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) ) -> ( ph -> ( t e. ( A ^o B ) -> t e. ran ( A CNF B ) ) ) ) )
105 22 104 tfis2 
 |-  ( t e. On -> ( ph -> ( t e. ( A ^o B ) -> t e. ran ( A CNF B ) ) ) )
106 105 com3l 
 |-  ( ph -> ( t e. ( A ^o B ) -> ( t e. On -> t e. ran ( A CNF B ) ) ) )
107 18 106 mpdd 
 |-  ( ph -> ( t e. ( A ^o B ) -> t e. ran ( A CNF B ) ) )
108 107 ssrdv 
 |-  ( ph -> ( A ^o B ) C_ ran ( A CNF B ) )
109 15 108 eqssd 
 |-  ( ph -> ran ( A CNF B ) = ( A ^o B ) )
110 dffo2 
 |-  ( ( A CNF B ) : S -onto-> ( A ^o B ) <-> ( ( A CNF B ) : S --> ( A ^o B ) /\ ran ( A CNF B ) = ( A ^o B ) ) )
111 14 109 110 sylanbrc 
 |-  ( ph -> ( A CNF B ) : S -onto-> ( A ^o B ) )
112 2 adantr 
 |-  ( ( ph /\ ( ( f e. S /\ g e. S ) /\ f T g ) ) -> A e. On )
113 3 adantr 
 |-  ( ( ph /\ ( ( f e. S /\ g e. S ) /\ f T g ) ) -> B e. On )
114 fveq2 
 |-  ( z = t -> ( x ` z ) = ( x ` t ) )
115 fveq2 
 |-  ( z = t -> ( y ` z ) = ( y ` t ) )
116 114 115 eleq12d 
 |-  ( z = t -> ( ( x ` z ) e. ( y ` z ) <-> ( x ` t ) e. ( y ` t ) ) )
117 eleq1w 
 |-  ( z = t -> ( z e. w <-> t e. w ) )
118 117 imbi1d 
 |-  ( z = t -> ( ( z e. w -> ( x ` w ) = ( y ` w ) ) <-> ( t e. w -> ( x ` w ) = ( y ` w ) ) ) )
119 118 ralbidv 
 |-  ( z = t -> ( A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) <-> A. w e. B ( t e. w -> ( x ` w ) = ( y ` w ) ) ) )
120 116 119 anbi12d 
 |-  ( z = t -> ( ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) <-> ( ( x ` t ) e. ( y ` t ) /\ A. w e. B ( t e. w -> ( x ` w ) = ( y ` w ) ) ) ) )
121 120 cbvrexvw 
 |-  ( E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) <-> E. t e. B ( ( x ` t ) e. ( y ` t ) /\ A. w e. B ( t e. w -> ( x ` w ) = ( y ` w ) ) ) )
122 fveq1 
 |-  ( x = u -> ( x ` t ) = ( u ` t ) )
123 fveq1 
 |-  ( y = v -> ( y ` t ) = ( v ` t ) )
124 eleq12 
 |-  ( ( ( x ` t ) = ( u ` t ) /\ ( y ` t ) = ( v ` t ) ) -> ( ( x ` t ) e. ( y ` t ) <-> ( u ` t ) e. ( v ` t ) ) )
125 122 123 124 syl2an 
 |-  ( ( x = u /\ y = v ) -> ( ( x ` t ) e. ( y ` t ) <-> ( u ` t ) e. ( v ` t ) ) )
126 fveq1 
 |-  ( x = u -> ( x ` w ) = ( u ` w ) )
127 fveq1 
 |-  ( y = v -> ( y ` w ) = ( v ` w ) )
128 126 127 eqeqan12d 
 |-  ( ( x = u /\ y = v ) -> ( ( x ` w ) = ( y ` w ) <-> ( u ` w ) = ( v ` w ) ) )
129 128 imbi2d 
 |-  ( ( x = u /\ y = v ) -> ( ( t e. w -> ( x ` w ) = ( y ` w ) ) <-> ( t e. w -> ( u ` w ) = ( v ` w ) ) ) )
130 129 ralbidv 
 |-  ( ( x = u /\ y = v ) -> ( A. w e. B ( t e. w -> ( x ` w ) = ( y ` w ) ) <-> A. w e. B ( t e. w -> ( u ` w ) = ( v ` w ) ) ) )
131 125 130 anbi12d 
 |-  ( ( x = u /\ y = v ) -> ( ( ( x ` t ) e. ( y ` t ) /\ A. w e. B ( t e. w -> ( x ` w ) = ( y ` w ) ) ) <-> ( ( u ` t ) e. ( v ` t ) /\ A. w e. B ( t e. w -> ( u ` w ) = ( v ` w ) ) ) ) )
132 131 rexbidv 
 |-  ( ( x = u /\ y = v ) -> ( E. t e. B ( ( x ` t ) e. ( y ` t ) /\ A. w e. B ( t e. w -> ( x ` w ) = ( y ` w ) ) ) <-> E. t e. B ( ( u ` t ) e. ( v ` t ) /\ A. w e. B ( t e. w -> ( u ` w ) = ( v ` w ) ) ) ) )
133 121 132 bitrid 
 |-  ( ( x = u /\ y = v ) -> ( E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) <-> E. t e. B ( ( u ` t ) e. ( v ` t ) /\ A. w e. B ( t e. w -> ( u ` w ) = ( v ` w ) ) ) ) )
134 133 cbvopabv 
 |-  { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) } = { <. u , v >. | E. t e. B ( ( u ` t ) e. ( v ` t ) /\ A. w e. B ( t e. w -> ( u ` w ) = ( v ` w ) ) ) }
135 4 134 eqtri 
 |-  T = { <. u , v >. | E. t e. B ( ( u ` t ) e. ( v ` t ) /\ A. w e. B ( t e. w -> ( u ` w ) = ( v ` w ) ) ) }
136 simprll 
 |-  ( ( ph /\ ( ( f e. S /\ g e. S ) /\ f T g ) ) -> f e. S )
137 simprlr 
 |-  ( ( ph /\ ( ( f e. S /\ g e. S ) /\ f T g ) ) -> g e. S )
138 simprr 
 |-  ( ( ph /\ ( ( f e. S /\ g e. S ) /\ f T g ) ) -> f T g )
139 eqid 
 |-  U. { c e. B | ( f ` c ) e. ( g ` c ) } = U. { c e. B | ( f ` c ) e. ( g ` c ) }
140 eqid 
 |-  OrdIso ( _E , ( g supp (/) ) ) = OrdIso ( _E , ( g supp (/) ) )
141 eqid 
 |-  seqom ( ( k e. _V , t e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( g supp (/) ) ) ` k ) ) .o ( g ` ( OrdIso ( _E , ( g supp (/) ) ) ` k ) ) ) +o t ) ) , (/) ) = seqom ( ( k e. _V , t e. _V |-> ( ( ( A ^o ( OrdIso ( _E , ( g supp (/) ) ) ` k ) ) .o ( g ` ( OrdIso ( _E , ( g supp (/) ) ) ` k ) ) ) +o t ) ) , (/) )
142 1 112 113 135 136 137 138 139 140 141 cantnflem1 
 |-  ( ( ph /\ ( ( f e. S /\ g e. S ) /\ f T g ) ) -> ( ( A CNF B ) ` f ) e. ( ( A CNF B ) ` g ) )
143 fvex 
 |-  ( ( A CNF B ) ` g ) e. _V
144 143 epeli 
 |-  ( ( ( A CNF B ) ` f ) _E ( ( A CNF B ) ` g ) <-> ( ( A CNF B ) ` f ) e. ( ( A CNF B ) ` g ) )
145 142 144 sylibr 
 |-  ( ( ph /\ ( ( f e. S /\ g e. S ) /\ f T g ) ) -> ( ( A CNF B ) ` f ) _E ( ( A CNF B ) ` g ) )
146 145 expr 
 |-  ( ( ph /\ ( f e. S /\ g e. S ) ) -> ( f T g -> ( ( A CNF B ) ` f ) _E ( ( A CNF B ) ` g ) ) )
147 146 ralrimivva 
 |-  ( ph -> A. f e. S A. g e. S ( f T g -> ( ( A CNF B ) ` f ) _E ( ( A CNF B ) ` g ) ) )
148 soisoi 
 |-  ( ( ( T Or S /\ _E Po ( A ^o B ) ) /\ ( ( A CNF B ) : S -onto-> ( A ^o B ) /\ A. f e. S A. g e. S ( f T g -> ( ( A CNF B ) ` f ) _E ( ( A CNF B ) ` g ) ) ) ) -> ( A CNF B ) Isom T , _E ( S , ( A ^o B ) ) )
149 5 13 111 147 148 syl22anc 
 |-  ( ph -> ( A CNF B ) Isom T , _E ( S , ( A ^o B ) ) )