Theorem cantnflem1d

Description: Lemma for cantnf . (Contributed by Mario Carneiro, 4-Jun-2015) (Revised by AV, 2-Jul-2019)

	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 ) ) ) }
	oemapval.f	|- ( ph -> F e. S )
	oemapval.g	|- ( ph -> G e. S )
	oemapvali.r	|- ( ph -> F T G )
	oemapvali.x	|- X = U. { c e. B | ( F ` c ) e. ( G ` c ) }
	cantnflem1.o	|- O = OrdIso ( _E , ( G supp (/) ) )
	cantnflem1.h	|- H = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( O ` k ) ) .o ( G ` ( O ` k ) ) ) +o z ) ) , (/) )
Assertion	cantnflem1d	|- ( ph -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ X , ( F ` x ) , (/) ) ) ) e. ( H ` suc ( `' O ` X ) ) )

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		oemapval.f	|- ( ph -> F e. S )
6		oemapval.g	|- ( ph -> G e. S )
7		oemapvali.r	|- ( ph -> F T G )
8		oemapvali.x	|- X = U. { c e. B | ( F ` c ) e. ( G ` c ) }
9		cantnflem1.o	|- O = OrdIso ( _E , ( G supp (/) ) )
10		cantnflem1.h	|- H = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( O ` k ) ) .o ( G ` ( O ` k ) ) ) +o z ) ) , (/) )
11	1 2 3 4 5 6 7 8	oemapvali	|- ( ph -> ( X e. B /\ ( F ` X ) e. ( G ` X ) /\ A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) ) )
12	11	simp1d	|- ( ph -> X e. B )
13		onelon	|- ( ( B e. On /\ X e. B ) -> X e. On )
14	3 12 13	syl2anc	|- ( ph -> X e. On )
15		oecl	|- ( ( A e. On /\ X e. On ) -> ( A ^o X ) e. On )
16	2 14 15	syl2anc	|- ( ph -> ( A ^o X ) e. On )
17	1 2 3	cantnfs	|- ( ph -> ( G e. S <-> ( G : B --> A /\ G finSupp (/) ) ) )
18	6 17	mpbid	|- ( ph -> ( G : B --> A /\ G finSupp (/) ) )
19	18	simpld	|- ( ph -> G : B --> A )
20	19 12	ffvelcdmd	|- ( ph -> ( G ` X ) e. A )
21		onelon	|- ( ( A e. On /\ ( G ` X ) e. A ) -> ( G ` X ) e. On )
22	2 20 21	syl2anc	|- ( ph -> ( G ` X ) e. On )
23		omcl	|- ( ( ( A ^o X ) e. On /\ ( G ` X ) e. On ) -> ( ( A ^o X ) .o ( G ` X ) ) e. On )
24	16 22 23	syl2anc	|- ( ph -> ( ( A ^o X ) .o ( G ` X ) ) e. On )
25		ovexd	|- ( ph -> ( G supp (/) ) e. _V )
26	1 2 3 9 6	cantnfcl	|- ( ph -> ( _E We ( G supp (/) ) /\ dom O e. _om ) )
27	26	simpld	|- ( ph -> _E We ( G supp (/) ) )
28	9	oiiso	|- ( ( ( G supp (/) ) e. _V /\ _E We ( G supp (/) ) ) -> O Isom _E , _E ( dom O , ( G supp (/) ) ) )
29	25 27 28	syl2anc	|- ( ph -> O Isom _E , _E ( dom O , ( G supp (/) ) ) )
30		isof1o	|- ( O Isom _E , _E ( dom O , ( G supp (/) ) ) -> O : dom O -1-1-onto-> ( G supp (/) ) )
31	29 30	syl	|- ( ph -> O : dom O -1-1-onto-> ( G supp (/) ) )
32		f1ocnv	|- ( O : dom O -1-1-onto-> ( G supp (/) ) -> `' O : ( G supp (/) ) -1-1-onto-> dom O )
33		f1of	|- ( `' O : ( G supp (/) ) -1-1-onto-> dom O -> `' O : ( G supp (/) ) --> dom O )
34	31 32 33	3syl	|- ( ph -> `' O : ( G supp (/) ) --> dom O )
35	1 2 3 4 5 6 7 8	cantnflem1a	|- ( ph -> X e. ( G supp (/) ) )
36	34 35	ffvelcdmd	|- ( ph -> ( `' O ` X ) e. dom O )
37	26	simprd	|- ( ph -> dom O e. _om )
38		elnn	|- ( ( ( `' O ` X ) e. dom O /\ dom O e. _om ) -> ( `' O ` X ) e. _om )
39	36 37 38	syl2anc	|- ( ph -> ( `' O ` X ) e. _om )
40	10	cantnfvalf	|- H : _om --> On
41	40	ffvelcdmi	|- ( ( `' O ` X ) e. _om -> ( H ` ( `' O ` X ) ) e. On )
42	39 41	syl	|- ( ph -> ( H ` ( `' O ` X ) ) e. On )
43		oaword1	|- ( ( ( ( A ^o X ) .o ( G ` X ) ) e. On /\ ( H ` ( `' O ` X ) ) e. On ) -> ( ( A ^o X ) .o ( G ` X ) ) C_ ( ( ( A ^o X ) .o ( G ` X ) ) +o ( H ` ( `' O ` X ) ) ) )
44	24 42 43	syl2anc	|- ( ph -> ( ( A ^o X ) .o ( G ` X ) ) C_ ( ( ( A ^o X ) .o ( G ` X ) ) +o ( H ` ( `' O ` X ) ) ) )
45	1 2 3 9 6 10	cantnfsuc	|- ( ( ph /\ ( `' O ` X ) e. _om ) -> ( H ` suc ( `' O ` X ) ) = ( ( ( A ^o ( O ` ( `' O ` X ) ) ) .o ( G ` ( O ` ( `' O ` X ) ) ) ) +o ( H ` ( `' O ` X ) ) ) )
46	39 45	mpdan	|- ( ph -> ( H ` suc ( `' O ` X ) ) = ( ( ( A ^o ( O ` ( `' O ` X ) ) ) .o ( G ` ( O ` ( `' O ` X ) ) ) ) +o ( H ` ( `' O ` X ) ) ) )
47		f1ocnvfv2	|- ( ( O : dom O -1-1-onto-> ( G supp (/) ) /\ X e. ( G supp (/) ) ) -> ( O ` ( `' O ` X ) ) = X )
48	31 35 47	syl2anc	|- ( ph -> ( O ` ( `' O ` X ) ) = X )
49	48	oveq2d	|- ( ph -> ( A ^o ( O ` ( `' O ` X ) ) ) = ( A ^o X ) )
50	48	fveq2d	|- ( ph -> ( G ` ( O ` ( `' O ` X ) ) ) = ( G ` X ) )
51	49 50	oveq12d	|- ( ph -> ( ( A ^o ( O ` ( `' O ` X ) ) ) .o ( G ` ( O ` ( `' O ` X ) ) ) ) = ( ( A ^o X ) .o ( G ` X ) ) )
52	51	oveq1d	|- ( ph -> ( ( ( A ^o ( O ` ( `' O ` X ) ) ) .o ( G ` ( O ` ( `' O ` X ) ) ) ) +o ( H ` ( `' O ` X ) ) ) = ( ( ( A ^o X ) .o ( G ` X ) ) +o ( H ` ( `' O ` X ) ) ) )
53	46 52	eqtrd	|- ( ph -> ( H ` suc ( `' O ` X ) ) = ( ( ( A ^o X ) .o ( G ` X ) ) +o ( H ` ( `' O ` X ) ) ) )
54	44 53	sseqtrrd	|- ( ph -> ( ( A ^o X ) .o ( G ` X ) ) C_ ( H ` suc ( `' O ` X ) ) )
55		onss	|- ( B e. On -> B C_ On )
56	3 55	syl	|- ( ph -> B C_ On )
57	56	sselda	|- ( ( ph /\ x e. B ) -> x e. On )
58	14	adantr	|- ( ( ph /\ x e. B ) -> X e. On )
59		onsseleq	|- ( ( x e. On /\ X e. On ) -> ( x C_ X <-> ( x e. X \/ x = X ) ) )
60	57 58 59	syl2anc	|- ( ( ph /\ x e. B ) -> ( x C_ X <-> ( x e. X \/ x = X ) ) )
61		orcom	|- ( ( x e. X \/ x = X ) <-> ( x = X \/ x e. X ) )
62	60 61	bitrdi	|- ( ( ph /\ x e. B ) -> ( x C_ X <-> ( x = X \/ x e. X ) ) )
63	62	ifbid	|- ( ( ph /\ x e. B ) -> if ( x C_ X , ( F ` x ) , (/) ) = if ( ( x = X \/ x e. X ) , ( F ` x ) , (/) ) )
64	63	mpteq2dva	|- ( ph -> ( x e. B |-> if ( x C_ X , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( ( x = X \/ x e. X ) , ( F ` x ) , (/) ) ) )
65	64	fveq2d	|- ( ph -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ X , ( F ` x ) , (/) ) ) ) = ( ( A CNF B ) ` ( x e. B |-> if ( ( x = X \/ x e. X ) , ( F ` x ) , (/) ) ) ) )
66	1 2 3	cantnfs	|- ( ph -> ( F e. S <-> ( F : B --> A /\ F finSupp (/) ) ) )
67	5 66	mpbid	|- ( ph -> ( F : B --> A /\ F finSupp (/) ) )
68	67	simpld	|- ( ph -> F : B --> A )
69	68	ffvelcdmda	|- ( ( ph /\ y e. B ) -> ( F ` y ) e. A )
70	20	ne0d	|- ( ph -> A =/= (/) )
71		on0eln0	|- ( A e. On -> ( (/) e. A <-> A =/= (/) ) )
72	2 71	syl	|- ( ph -> ( (/) e. A <-> A =/= (/) ) )
73	70 72	mpbird	|- ( ph -> (/) e. A )
74	73	adantr	|- ( ( ph /\ y e. B ) -> (/) e. A )
75	69 74	ifcld	|- ( ( ph /\ y e. B ) -> if ( y e. X , ( F ` y ) , (/) ) e. A )
76	75	fmpttd	|- ( ph -> ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) : B --> A )
77		0ex	|- (/) e. _V
78	77	a1i	|- ( ph -> (/) e. _V )
79	67	simprd	|- ( ph -> F finSupp (/) )
80	68 3 78 79	fsuppmptif	|- ( ph -> ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) finSupp (/) )
81	1 2 3	cantnfs	|- ( ph -> ( ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) e. S <-> ( ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) : B --> A /\ ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) finSupp (/) ) ) )
82	76 80 81	mpbir2and	|- ( ph -> ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) e. S )
83	68 12	ffvelcdmd	|- ( ph -> ( F ` X ) e. A )
84		eldifn	|- ( y e. ( B \ X ) -> -. y e. X )
85	84	adantl	|- ( ( ph /\ y e. ( B \ X ) ) -> -. y e. X )
86	85	iffalsed	|- ( ( ph /\ y e. ( B \ X ) ) -> if ( y e. X , ( F ` y ) , (/) ) = (/) )
87	86 3	suppss2	|- ( ph -> ( ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) supp (/) ) C_ X )
88		ifor	|- if ( ( x = X \/ x e. X ) , ( F ` x ) , (/) ) = if ( x = X , ( F ` x ) , if ( x e. X , ( F ` x ) , (/) ) )
89		fveq2	|- ( x = X -> ( F ` x ) = ( F ` X ) )
90	89	adantl	|- ( ( x e. B /\ x = X ) -> ( F ` x ) = ( F ` X ) )
91	90	ifeq1da	|- ( x e. B -> if ( x = X , ( F ` x ) , ( ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ` x ) ) = if ( x = X , ( F ` X ) , ( ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ` x ) ) )
92		eleq1w	|- ( y = x -> ( y e. X <-> x e. X ) )
93		fveq2	|- ( y = x -> ( F ` y ) = ( F ` x ) )
94	92 93	ifbieq1d	|- ( y = x -> if ( y e. X , ( F ` y ) , (/) ) = if ( x e. X , ( F ` x ) , (/) ) )
95		eqid	|- ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) = ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) )
96		fvex	|- ( F ` x ) e. _V
97	96 77	ifex	|- if ( x e. X , ( F ` x ) , (/) ) e. _V
98	94 95 97	fvmpt	|- ( x e. B -> ( ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ` x ) = if ( x e. X , ( F ` x ) , (/) ) )
99	98	ifeq2d	|- ( x e. B -> if ( x = X , ( F ` x ) , ( ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ` x ) ) = if ( x = X , ( F ` x ) , if ( x e. X , ( F ` x ) , (/) ) ) )
100	91 99	eqtr3d	|- ( x e. B -> if ( x = X , ( F ` X ) , ( ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ` x ) ) = if ( x = X , ( F ` x ) , if ( x e. X , ( F ` x ) , (/) ) ) )
101	88 100	eqtr4id	|- ( x e. B -> if ( ( x = X \/ x e. X ) , ( F ` x ) , (/) ) = if ( x = X , ( F ` X ) , ( ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ` x ) ) )
102	101	mpteq2ia	|- ( x e. B |-> if ( ( x = X \/ x e. X ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x = X , ( F ` X ) , ( ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ` x ) ) )
103	1 2 3 82 12 83 87 102	cantnfp1	|- ( ph -> ( ( x e. B |-> if ( ( x = X \/ x e. X ) , ( F ` x ) , (/) ) ) e. S /\ ( ( A CNF B ) ` ( x e. B |-> if ( ( x = X \/ x e. X ) , ( F ` x ) , (/) ) ) ) = ( ( ( A ^o X ) .o ( F ` X ) ) +o ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) ) ) )
104	103	simprd	|- ( ph -> ( ( A CNF B ) ` ( x e. B |-> if ( ( x = X \/ x e. X ) , ( F ` x ) , (/) ) ) ) = ( ( ( A ^o X ) .o ( F ` X ) ) +o ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) ) )
105	65 104	eqtrd	|- ( ph -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ X , ( F ` x ) , (/) ) ) ) = ( ( ( A ^o X ) .o ( F ` X ) ) +o ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) ) )
106		onelon	|- ( ( A e. On /\ ( F ` X ) e. A ) -> ( F ` X ) e. On )
107	2 83 106	syl2anc	|- ( ph -> ( F ` X ) e. On )
108		omsuc	|- ( ( ( A ^o X ) e. On /\ ( F ` X ) e. On ) -> ( ( A ^o X ) .o suc ( F ` X ) ) = ( ( ( A ^o X ) .o ( F ` X ) ) +o ( A ^o X ) ) )
109	16 107 108	syl2anc	|- ( ph -> ( ( A ^o X ) .o suc ( F ` X ) ) = ( ( ( A ^o X ) .o ( F ` X ) ) +o ( A ^o X ) ) )
110		eloni	|- ( ( G ` X ) e. On -> Ord ( G ` X ) )
111	22 110	syl	|- ( ph -> Ord ( G ` X ) )
112	11	simp2d	|- ( ph -> ( F ` X ) e. ( G ` X ) )
113		ordsucss	|- ( Ord ( G ` X ) -> ( ( F ` X ) e. ( G ` X ) -> suc ( F ` X ) C_ ( G ` X ) ) )
114	111 112 113	sylc	|- ( ph -> suc ( F ` X ) C_ ( G ` X ) )
115		onsuc	|- ( ( F ` X ) e. On -> suc ( F ` X ) e. On )
116	107 115	syl	|- ( ph -> suc ( F ` X ) e. On )
117		omwordi	|- ( ( suc ( F ` X ) e. On /\ ( G ` X ) e. On /\ ( A ^o X ) e. On ) -> ( suc ( F ` X ) C_ ( G ` X ) -> ( ( A ^o X ) .o suc ( F ` X ) ) C_ ( ( A ^o X ) .o ( G ` X ) ) ) )
118	116 22 16 117	syl3anc	|- ( ph -> ( suc ( F ` X ) C_ ( G ` X ) -> ( ( A ^o X ) .o suc ( F ` X ) ) C_ ( ( A ^o X ) .o ( G ` X ) ) ) )
119	114 118	mpd	|- ( ph -> ( ( A ^o X ) .o suc ( F ` X ) ) C_ ( ( A ^o X ) .o ( G ` X ) ) )
120	109 119	eqsstrrd	|- ( ph -> ( ( ( A ^o X ) .o ( F ` X ) ) +o ( A ^o X ) ) C_ ( ( A ^o X ) .o ( G ` X ) ) )
121	1 2 3 82 73 14 87	cantnflt2	|- ( ph -> ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) e. ( A ^o X ) )
122		onelon	|- ( ( ( A ^o X ) e. On /\ ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) e. ( A ^o X ) ) -> ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) e. On )
123	16 121 122	syl2anc	|- ( ph -> ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) e. On )
124		omcl	|- ( ( ( A ^o X ) e. On /\ ( F ` X ) e. On ) -> ( ( A ^o X ) .o ( F ` X ) ) e. On )
125	16 107 124	syl2anc	|- ( ph -> ( ( A ^o X ) .o ( F ` X ) ) e. On )
126		oaord	|- ( ( ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) e. On /\ ( A ^o X ) e. On /\ ( ( A ^o X ) .o ( F ` X ) ) e. On ) -> ( ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) e. ( A ^o X ) <-> ( ( ( A ^o X ) .o ( F ` X ) ) +o ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) ) e. ( ( ( A ^o X ) .o ( F ` X ) ) +o ( A ^o X ) ) ) )
127	123 16 125 126	syl3anc	|- ( ph -> ( ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) e. ( A ^o X ) <-> ( ( ( A ^o X ) .o ( F ` X ) ) +o ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) ) e. ( ( ( A ^o X ) .o ( F ` X ) ) +o ( A ^o X ) ) ) )
128	121 127	mpbid	|- ( ph -> ( ( ( A ^o X ) .o ( F ` X ) ) +o ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) ) e. ( ( ( A ^o X ) .o ( F ` X ) ) +o ( A ^o X ) ) )
129	120 128	sseldd	|- ( ph -> ( ( ( A ^o X ) .o ( F ` X ) ) +o ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) ) e. ( ( A ^o X ) .o ( G ` X ) ) )
130	105 129	eqeltrd	|- ( ph -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ X , ( F ` x ) , (/) ) ) ) e. ( ( A ^o X ) .o ( G ` X ) ) )
131	54 130	sseldd	|- ( ph -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ X , ( F ` x ) , (/) ) ) ) e. ( H ` suc ( `' O ` X ) ) )