Theorem cantnf 7605

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 indexes 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 7589, implies that such a representation is unique). (Contributed by Mario Carneiro, 28-May-2015.)

Hypotheses

Ref	Expression
cantnfs.1	|- S = dom ( A CNF B )
cantnfs.2	|- ( ph -> A e. On )
cantnfs.3	|- ( 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

Ref	Expression
cantnf	|- ( ph -> ( A CNF B ) Isom T , _E ( S , ( A ^o B ) ) )

Distinct variable groups:   x, w, y, z, B   w, A, x, y, z   x, S, y, z   ph, x, y, z

Allowed substitution hints:   ph( w)   S( w)   T( x, y, z, w)

Proof of Theorem cantnf

Dummy variables f c g k t u v a b d are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cantnfs.1	. . 3 |- S = dom ( A CNF B )
2		cantnfs.2	. . 3 |- ( ph -> A e. On )
3		cantnfs.3	. . 3 |- ( ph -> B e. On )
4		oemapval.t	. . 3 |- 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 7594	. 2 |- ( ph -> T Or S )
6		oecl 6740	. . . . . 6 |- ( ( A e. On /\ B e. On ) -> ( A ^o B ) e. On )
7	2, 3, 6	syl2anc 643	. . . . 5 |- ( ph -> ( A ^o B ) e. On )
8		eloni 4551	. . . . 5 |- ( ( A ^o B ) e. On -> Ord ( A ^o B ) )
9	7, 8	syl 16	. . . 4 |- ( ph -> Ord ( A ^o B ) )
10		ordwe 4554	. . . 4 |- ( Ord ( A ^o B ) -> _E We ( A ^o B ) )
11	9, 10	syl 16	. . 3 |- ( ph -> _E We ( A ^o B ) )
12		weso 4533	. . 3 |- ( _E We ( A ^o B ) -> _E Or ( A ^o B ) )
13		sopo 4480	. . 3 |- ( _E Or ( A ^o B ) -> _E Po ( A ^o B ) )
14	11, 12, 13	3syl 19	. 2 |- ( ph -> _E Po ( A ^o B ) )
15	1, 2, 3	cantnff 7585	. . 3 |- ( ph -> ( A CNF B ) : S --> ( A ^o B ) )
16		frn 5556	. . . . 5 |- ( ( A CNF B ) : S --> ( A ^o B ) -> ran ( A CNF B ) C_ ( A ^o B ) )
17	15, 16	syl 16	. . . 4 |- ( ph -> ran ( A CNF B ) C_ ( A ^o B ) )
18		onss 4730	. . . . . . . 8 |- ( ( A ^o B ) e. On -> ( A ^o B ) C_ On )
19	7, 18	syl 16	. . . . . . 7 |- ( ph -> ( A ^o B ) C_ On )
20	19	sseld 3307	. . . . . 6 |- ( ph -> ( t e. ( A ^o B ) -> t e. On ) )
21		eleq1 2464	. . . . . . . . . 10 |- ( t = y -> ( t e. ( A ^o B ) <-> y e. ( A ^o B ) ) )
22		eleq1 2464	. . . . . . . . . 10 |- ( t = y -> ( t e. ran ( A CNF B ) <-> y e. ran ( A CNF B ) ) )
23	21, 22	imbi12d 312	. . . . . . . . 9 |- ( t = y -> ( ( t e. ( A ^o B ) -> t e. ran ( A CNF B ) ) <-> ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) ) )
24	23	imbi2d 308	. . . . . . . 8 |- ( 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 ) ) ) ) )
25		r19.21v 2753	. . . . . . . . 9 |- ( 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 ) ) ) )
26		ordelss 4557	. . . . . . . . . . . . . . . . . . 19 |- ( ( Ord ( A ^o B ) /\ t e. ( A ^o B ) ) -> t C_ ( A ^o B ) )
27	9, 26	sylan 458	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ t e. ( A ^o B ) ) -> t C_ ( A ^o B ) )
28	27	sselda 3308	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ t e. ( A ^o B ) ) /\ y e. t ) -> y e. ( A ^o B ) )
29		pm5.5 327	. . . . . . . . . . . . . . . . 17 |- ( y e. ( A ^o B ) -> ( ( y e. ( A ^o B ) -> y e. ran ( A CNF B ) ) <-> y e. ran ( A CNF B ) ) )
30	28, 29	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 ) ) )
31	30	ralbidva 2682	. . . . . . . . . . . . . . 15 |- ( ( 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 ) ) )
32		dfss3 3298	. . . . . . . . . . . . . . 15 |- ( t C_ ran ( A CNF B ) <-> A. y e. t y e. ran ( A CNF B ) )
33	31, 32	syl6bbr 255	. . . . . . . . . . . . . 14 |- ( ( 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 ) ) )
34		eleq1 2464	. . . . . . . . . . . . . . . 16 |- ( t = (/) -> ( t e. ran ( A CNF B ) <-> (/) e. ran ( A CNF B ) ) )
35	2	adantr 452	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> A e. On )
36	35	adantr 452	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) /\ t =/= (/) ) -> A e. On )
37	3	adantr 452	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> B e. On )
38	37	adantr 452	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) /\ t =/= (/) ) -> B e. On )
39		simplrl 737	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) /\ t =/= (/) ) -> t e. ( A ^o B ) )
40		simplrr 738	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) /\ t =/= (/) ) -> t C_ ran ( A CNF B ) )
41	7	adantr 452	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( A ^o B ) e. On )
42		simprl 733	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> t e. ( A ^o B ) )
43		onelon 4566	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( A ^o B ) e. On /\ t e. ( A ^o B ) ) -> t e. On )
44	41, 42, 43	syl2anc 643	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> t e. On )
45		on0eln0 4596	. . . . . . . . . . . . . . . . . . 19 |- ( t e. On -> ( (/) e. t <-> t =/= (/) ) )
46	44, 45	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( (/) e. t <-> t =/= (/) ) )
47	46	biimpar 472	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) /\ t =/= (/) ) -> (/) e. t )
48		eqid 2404	. . . . . . . . . . . . . . . . 17 |- U. |^| { c e. On | t e. ( A ^o c ) } = U. |^| { c e. On | t e. ( A ^o c ) }
49		eqid 2404	. . . . . . . . . . . . . . . . 17 |- ( 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 ) )
50		eqid 2404	. . . . . . . . . . . . . . . . 17 |- ( 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 ) ) )
51		eqid 2404	. . . . . . . . . . . . . . . . 17 |- ( 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 ) ) )
52	1, 36, 38, 4, 39, 40, 47, 48, 49, 50, 51	cantnflem4 7604	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) /\ t =/= (/) ) -> t e. ran ( A CNF B ) )
53		fconstmpt 4880	. . . . . . . . . . . . . . . . . . . . . 22 |- ( B X. { (/) } ) = ( y e. B |-> (/) )
54	53	mptpreima 5322	. . . . . . . . . . . . . . . . . . . . 21 |- ( `' ( B X. { (/) } ) " ( _V \ 1o ) ) = { y e. B | (/) e. ( _V \ 1o ) }
55		neirr 2572	. . . . . . . . . . . . . . . . . . . . . . . 24 |- -. (/) =/= (/)
56		dif1o 6703	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( (/) e. ( _V \ 1o ) <-> ( (/) e. _V /\ (/) =/= (/) ) )
57	56	simprbi 451	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( (/) e. ( _V \ 1o ) -> (/) =/= (/) )
58	55, 57	mto 169	. . . . . . . . . . . . . . . . . . . . . . 23 |- -. (/) e. ( _V \ 1o )
59	58	rgenw 2733	. . . . . . . . . . . . . . . . . . . . . 22 |- A. y e. B -. (/) e. ( _V \ 1o )
60		rabeq0 3609	. . . . . . . . . . . . . . . . . . . . . 22 |- ( { y e. B | (/) e. ( _V \ 1o ) } = (/) <-> A. y e. B -. (/) e. ( _V \ 1o ) )
61	59, 60	mpbir 201	. . . . . . . . . . . . . . . . . . . . 21 |- { y e. B | (/) e. ( _V \ 1o ) } = (/)
62	54, 61	eqtr2i 2425	. . . . . . . . . . . . . . . . . . . 20 |- (/) = ( `' ( B X. { (/) } ) " ( _V \ 1o ) )
63		oieq2 7438	. . . . . . . . . . . . . . . . . . . 20 |- ( (/) = ( `' ( B X. { (/) } ) " ( _V \ 1o ) ) -> OrdIso ( _E , (/) ) = OrdIso ( _E , ( `' ( B X. { (/) } ) " ( _V \ 1o ) ) ) )
64	62, 63	ax-mp 8	. . . . . . . . . . . . . . . . . . 19 |- OrdIso ( _E , (/) ) = OrdIso ( _E , ( `' ( B X. { (/) } ) " ( _V \ 1o ) ) )
65		ne0i 3594	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y e. B -> B =/= (/) )
66		ne0i 3594	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( t e. ( A ^o B ) -> ( A ^o B ) =/= (/) )
67	66	ad2antrl 709	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( A ^o B ) =/= (/) )
68		oveq1 6047	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( A = (/) -> ( A ^o B ) = ( (/) ^o B ) )
69	68	neeq1d 2580	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( A = (/) -> ( ( A ^o B ) =/= (/) <-> ( (/) ^o B ) =/= (/) ) )
70	67, 69	syl5ibcom 212	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( A = (/) -> ( (/) ^o B ) =/= (/) ) )
71	70	necon2d 2617	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( ( (/) ^o B ) = (/) -> A =/= (/) ) )
72		on0eln0 4596	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( B e. On -> ( (/) e. B <-> B =/= (/) ) )
73		oe0m1 6724	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( B e. On -> ( (/) e. B <-> ( (/) ^o B ) = (/) ) )
74	72, 73	bitr3d 247	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( B e. On -> ( B =/= (/) <-> ( (/) ^o B ) = (/) ) )
75	37, 74	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( B =/= (/) <-> ( (/) ^o B ) = (/) ) )
76		on0eln0 4596	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A e. On -> ( (/) e. A <-> A =/= (/) ) )
77	35, 76	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( (/) e. A <-> A =/= (/) ) )
78	71, 75, 77	3imtr4d 260	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( B =/= (/) -> (/) e. A ) )
79	65, 78	syl5 30	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( y e. B -> (/) e. A ) )
80	79	imp 419	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) /\ y e. B ) -> (/) e. A )
81	80, 53	fmptd 5852	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( B X. { (/) } ) : B --> A )
82		0fin 7295	. . . . . . . . . . . . . . . . . . . . . 22 |- (/) e. Fin
83	62, 82	eqeltrri 2475	. . . . . . . . . . . . . . . . . . . . 21 |- ( `' ( B X. { (/) } ) " ( _V \ 1o ) ) e. Fin
84	83	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( `' ( B X. { (/) } ) " ( _V \ 1o ) ) e. Fin )
85	1, 2, 3	cantnfs 7577	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( ( B X. { (/) } ) e. S <-> ( ( B X. { (/) } ) : B --> A /\ ( `' ( B X. { (/) } ) " ( _V \ 1o ) ) e. Fin ) ) )
86	85	adantr 452	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( ( B X. { (/) } ) e. S <-> ( ( B X. { (/) } ) : B --> A /\ ( `' ( B X. { (/) } ) " ( _V \ 1o ) ) e. Fin ) ) )
87	81, 84, 86	mpbir2and 889	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( B X. { (/) } ) e. S )
88		eqid 2404	. . . . . . . . . . . . . . . . . . 19 |- seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o (OrdIso ( _E , (/) ) ` k ) ) .o ( ( B X. { (/) } ) ` (OrdIso ( _E , (/) ) ` k ) ) ) +o z ) ) , (/) ) = seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o (OrdIso ( _E , (/) ) ` k ) ) .o ( ( B X. { (/) } ) ` (OrdIso ( _E , (/) ) ` k ) ) ) +o z ) ) , (/) )
89	1, 35, 37, 64, 87, 88	cantnfval 7579	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( ( A CNF B ) ` ( B X. { (/) } ) ) = (seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o (OrdIso ( _E , (/) ) ` k ) ) .o ( ( B X. { (/) } ) ` (OrdIso ( _E , (/) ) ` k ) ) ) +o z ) ) , (/) ) ` dom OrdIso ( _E , (/) ) ) )
90		0ex 4299	. . . . . . . . . . . . . . . . . . . . . 22 |- (/) e. _V
91		we0 4537	. . . . . . . . . . . . . . . . . . . . . 22 |- _E We (/)
92		eqid 2404	. . . . . . . . . . . . . . . . . . . . . . 23 |- OrdIso ( _E , (/) ) = OrdIso ( _E , (/) )
93	92	oien 7463	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( (/) e. _V /\ _E We (/) ) -> dom OrdIso ( _E , (/) ) ~~ (/) )
94	90, 91, 93	mp2an 654	. . . . . . . . . . . . . . . . . . . . 21 |- dom OrdIso ( _E , (/) ) ~~ (/)
95		en0 7129	. . . . . . . . . . . . . . . . . . . . 21 |- ( dom OrdIso ( _E , (/) ) ~~ (/) <-> dom OrdIso ( _E , (/) ) = (/) )
96	94, 95	mpbi 200	. . . . . . . . . . . . . . . . . . . 20 |- dom OrdIso ( _E , (/) ) = (/)
97	96	fveq2i 5690	. . . . . . . . . . . . . . . . . . 19 |- (seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o (OrdIso ( _E , (/) ) ` k ) ) .o ( ( B X. { (/) } ) ` (OrdIso ( _E , (/) ) ` k ) ) ) +o z ) ) , (/) ) ` dom OrdIso ( _E , (/) ) ) = (seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o (OrdIso ( _E , (/) ) ` k ) ) .o ( ( B X. { (/) } ) ` (OrdIso ( _E , (/) ) ` k ) ) ) +o z ) ) , (/) ) ` (/) )
98	88	seqom0g 6672	. . . . . . . . . . . . . . . . . . . 20 |- ( (/) e. _V -> (seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o (OrdIso ( _E , (/) ) ` k ) ) .o ( ( B X. { (/) } ) ` (OrdIso ( _E , (/) ) ` k ) ) ) +o z ) ) , (/) ) ` (/) ) = (/) )
99	90, 98	ax-mp 8	. . . . . . . . . . . . . . . . . . 19 |- (seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o (OrdIso ( _E , (/) ) ` k ) ) .o ( ( B X. { (/) } ) ` (OrdIso ( _E , (/) ) ` k ) ) ) +o z ) ) , (/) ) ` (/) ) = (/)
100	97, 99	eqtri 2424	. . . . . . . . . . . . . . . . . 18 |- (seq𝜔 ( ( k e. _V , z e. _V |-> ( ( ( A ^o (OrdIso ( _E , (/) ) ` k ) ) .o ( ( B X. { (/) } ) ` (OrdIso ( _E , (/) ) ` k ) ) ) +o z ) ) , (/) ) ` dom OrdIso ( _E , (/) ) ) = (/)
101	89, 100	syl6eq 2452	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( ( A CNF B ) ` ( B X. { (/) } ) ) = (/) )
102	15	adantr 452	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( A CNF B ) : S --> ( A ^o B ) )
103		ffn 5550	. . . . . . . . . . . . . . . . . . 19 |- ( ( A CNF B ) : S --> ( A ^o B ) -> ( A CNF B ) Fn S )
104	102, 103	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( A CNF B ) Fn S )
105		fnfvelrn 5826	. . . . . . . . . . . . . . . . . 18 |- ( ( ( A CNF B ) Fn S /\ ( B X. { (/) } ) e. S ) -> ( ( A CNF B ) ` ( B X. { (/) } ) ) e. ran ( A CNF B ) )
106	104, 87, 105	syl2anc 643	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> ( ( A CNF B ) ` ( B X. { (/) } ) ) e. ran ( A CNF B ) )
107	101, 106	eqeltrrd 2479	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> (/) e. ran ( A CNF B ) )
108	34, 52, 107	pm2.61ne 2642	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( t e. ( A ^o B ) /\ t C_ ran ( A CNF B ) ) ) -> t e. ran ( A CNF B ) )
109	108	expr 599	. . . . . . . . . . . . . 14 |- ( ( ph /\ t e. ( A ^o B ) ) -> ( t C_ ran ( A CNF B ) -> t e. ran ( A CNF B ) ) )
110	33, 109	sylbid 207	. . . . . . . . . . . . 13 |- ( ( 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 ) ) )
111	110	ex 424	. . . . . . . . . . . 12 |- ( 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 ) ) ) )
112	111	com23 74	. . . . . . . . . . 11 |- ( 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 ) ) ) )
113	112	a2i 13	. . . . . . . . . 10 |- ( ( 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 ) ) ) )
114	113	a1i 11	. . . . . . . . 9 |- ( 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 ) ) ) ) )
115	25, 114	syl5bi 209	. . . . . . . 8 |- ( 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 ) ) ) ) )
116	24, 115	tfis2 4795	. . . . . . 7 |- ( t e. On -> ( ph -> ( t e. ( A ^o B ) -> t e. ran ( A CNF B ) ) ) )
117	116	com3l 77	. . . . . 6 |- ( ph -> ( t e. ( A ^o B ) -> ( t e. On -> t e. ran ( A CNF B ) ) ) )
118	20, 117	mpdd 38	. . . . 5 |- ( ph -> ( t e. ( A ^o B ) -> t e. ran ( A CNF B ) ) )
119	118	ssrdv 3314	. . . 4 |- ( ph -> ( A ^o B ) C_ ran ( A CNF B ) )
120	17, 119	eqssd 3325	. . 3 |- ( ph -> ran ( A CNF B ) = ( A ^o B ) )
121		dffo2 5616	. . 3 |- ( ( A CNF B ) : S -onto-> ( A ^o B ) <-> ( ( A CNF B ) : S --> ( A ^o B ) /\ ran ( A CNF B ) = ( A ^o B ) ) )
122	15, 120, 121	sylanbrc 646	. 2 |- ( ph -> ( A CNF B ) : S -onto-> ( A ^o B ) )
123	2	adantr 452	. . . . . 6 |- ( ( ph /\ ( ( f e. S /\ g e. S ) /\ f T g ) ) -> A e. On )
124	3	adantr 452	. . . . . 6 |- ( ( ph /\ ( ( f e. S /\ g e. S ) /\ f T g ) ) -> B e. On )
125		fveq2 5687	. . . . . . . . . . . 12 |- ( z = t -> ( x ` z ) = ( x ` t ) )
126		fveq2 5687	. . . . . . . . . . . 12 |- ( z = t -> ( y ` z ) = ( y ` t ) )
127	125, 126	eleq12d 2472	. . . . . . . . . . 11 |- ( z = t -> ( ( x ` z ) e. ( y ` z ) <-> ( x ` t ) e. ( y ` t ) ) )
128		eleq1 2464	. . . . . . . . . . . . 13 |- ( z = t -> ( z e. w <-> t e. w ) )
129	128	imbi1d 309	. . . . . . . . . . . 12 |- ( z = t -> ( ( z e. w -> ( x ` w ) = ( y ` w ) ) <-> ( t e. w -> ( x ` w ) = ( y ` w ) ) ) )
130	129	ralbidv 2686	. . . . . . . . . . 11 |- ( z = t -> ( A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) <-> A. w e. B ( t e. w -> ( x ` w ) = ( y ` w ) ) ) )
131	127, 130	anbi12d 692	. . . . . . . . . 10 |- ( 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 ) ) ) ) )
132	131	cbvrexv 2893	. . . . . . . . 9 |- ( 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 ) ) ) )
133		fveq1 5686	. . . . . . . . . . . 12 |- ( x = u -> ( x ` t ) = ( u ` t ) )
134		fveq1 5686	. . . . . . . . . . . 12 |- ( y = v -> ( y ` t ) = ( v ` t ) )
135		eleq12 2466	. . . . . . . . . . . 12 |- ( ( ( x ` t ) = ( u ` t ) /\ ( y ` t ) = ( v ` t ) ) -> ( ( x ` t ) e. ( y ` t ) <-> ( u ` t ) e. ( v ` t ) ) )
136	133, 134, 135	syl2an 464	. . . . . . . . . . 11 |- ( ( x = u /\ y = v ) -> ( ( x ` t ) e. ( y ` t ) <-> ( u ` t ) e. ( v ` t ) ) )
137		fveq1 5686	. . . . . . . . . . . . . 14 |- ( x = u -> ( x ` w ) = ( u ` w ) )
138		fveq1 5686	. . . . . . . . . . . . . 14 |- ( y = v -> ( y ` w ) = ( v ` w ) )
139	137, 138	eqeqan12d 2419	. . . . . . . . . . . . 13 |- ( ( x = u /\ y = v ) -> ( ( x ` w ) = ( y ` w ) <-> ( u ` w ) = ( v ` w ) ) )
140	139	imbi2d 308	. . . . . . . . . . . 12 |- ( ( x = u /\ y = v ) -> ( ( t e. w -> ( x ` w ) = ( y ` w ) ) <-> ( t e. w -> ( u ` w ) = ( v ` w ) ) ) )
141	140	ralbidv 2686	. . . . . . . . . . 11 |- ( ( 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 ) ) ) )
142	136, 141	anbi12d 692	. . . . . . . . . 10 |- ( ( 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 ) ) ) ) )
143	142	rexbidv 2687	. . . . . . . . 9 |- ( ( 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 ) ) ) ) )
144	132, 143	syl5bb 249	. . . . . . . 8 |- ( ( 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 ) ) ) ) )
145	144	cbvopabv 4237	. . . . . . 7 |- { <. 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 ) ) ) }
146	4, 145	eqtri 2424	. . . . . 6 |- T = { <. u , v >. | E. t e. B ( ( u ` t ) e. ( v ` t ) /\ A. w e. B ( t e. w -> ( u ` w ) = ( v ` w ) ) ) }
147		simprll 739	. . . . . 6 |- ( ( ph /\ ( ( f e. S /\ g e. S ) /\ f T g ) ) -> f e. S )
148		simprlr 740	. . . . . 6 |- ( ( ph /\ ( ( f e. S /\ g e. S ) /\ f T g ) ) -> g e. S )
149		simprr 734	. . . . . 6 |- ( ( ph /\ ( ( f e. S /\ g e. S ) /\ f T g ) ) -> f T g )
150		eqid 2404	. . . . . 6 |- U. { c e. B | ( f ` c ) e. ( g ` c ) } = U. { c e. B | ( f ` c ) e. ( g ` c ) }
151		eqid 2404	. . . . . 6 |- OrdIso ( _E , ( `' g " ( _V \ 1o ) ) ) = OrdIso ( _E , ( `' g " ( _V \ 1o ) ) )
152		eqid 2404	. . . . . 6 |- seq𝜔 ( ( k e. _V , t e. _V |-> ( ( ( A ^o (OrdIso ( _E , ( `' g " ( _V \ 1o ) ) ) ` k ) ) .o ( g ` (OrdIso ( _E , ( `' g " ( _V \ 1o ) ) ) ` k ) ) ) +o t ) ) , (/) ) = seq𝜔 ( ( k e. _V , t e. _V |-> ( ( ( A ^o (OrdIso ( _E , ( `' g " ( _V \ 1o ) ) ) ` k ) ) .o ( g ` (OrdIso ( _E , ( `' g " ( _V \ 1o ) ) ) ` k ) ) ) +o t ) ) , (/) )
153	1, 123, 124, 146, 147, 148, 149, 150, 151, 152	cantnflem1 7601	. . . . 5 |- ( ( ph /\ ( ( f e. S /\ g e. S ) /\ f T g ) ) -> ( ( A CNF B ) ` f ) e. ( ( A CNF B ) ` g ) )
154		fvex 5701	. . . . . 6 |- ( ( A CNF B ) ` g ) e. _V
155	154	epelc 4456	. . . . 5 |- ( ( ( A CNF B ) ` f ) _E ( ( A CNF B ) ` g ) <-> ( ( A CNF B ) ` f ) e. ( ( A CNF B ) ` g ) )
156	153, 155	sylibr 204	. . . 4 |- ( ( ph /\ ( ( f e. S /\ g e. S ) /\ f T g ) ) -> ( ( A CNF B ) ` f ) _E ( ( A CNF B ) ` g ) )
157	156	expr 599	. . 3 |- ( ( ph /\ ( f e. S /\ g e. S ) ) -> ( f T g -> ( ( A CNF B ) ` f ) _E ( ( A CNF B ) ` g ) ) )
158	157	ralrimivva 2758	. 2 |- ( ph -> A. f e. S A. g e. S ( f T g -> ( ( A CNF B ) ` f ) _E ( ( A CNF B ) ` g ) ) )
159		soisoi 6007	. 2 |- ( ( ( 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 ) ) )
160	5, 14, 122, 158, 159	syl22anc 1185	1 |- ( ph -> ( A CNF B ) Isom T , _E ( S , ( A ^o B ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   /\ wa 359   = wceq 1649   e. wcel 1721   =/= wne 2567   A.wral 2666   E.wrex 2667   {crab 2670   _Vcvv 2916   \ cdif 3277   C_ wss 3280   (/)c0 3588   {csn 3774   <.cop 3777   U.cuni 3975   |^|cint 4010   class class class wbr 4172   {copab 4225   _E cep 4452   Po wpo 4461   Or wor 4462   We wwe 4500   Ord word 4540   Oncon0 4541   X. cxp 4835   `'ccnv 4836   dom cdm 4837   ran crn 4838   "cima 4840   iotacio 5375   Fn wfn 5408   -->wf 5409   -onto->wfo 5411   ` cfv 5413   Isom wiso 5414  (class class class)co 6040   e. cmpt2 6042   1stc1st 6306   2ndc2nd 6307  seq_𝜔cseqom 6663   1oc1o 6676   +o coa 6680   .o comu 6681   ^o coe 6682   ~~ cen 7065   Fincfn 7068  OrdIsocoi 7434   CNF ccnf 7572

This theorem is referenced by:  oemapwe  7606  cantnffval2  7607  cantnff1o  7608

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-seqom 6664  df-1o 6683  df-2o 6684  df-oadd 6687  df-omul 6688  df-oexp 6689  df-er 6864  df-map 6979  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-oi 7435  df-cnf 7573