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

Metamath Proof Explorer

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