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 syl5bi
 |-  ( 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 syl5bb
 |-  ( ( 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 ) ) )