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	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 ) ) )