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 ffvelrnd
 |-  ( 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 ffvelrnd
 |-  ( 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 ffvelrni
 |-  ( ( `' 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 ffvelrnda
 |-  ( ( 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 ffvelrnd
 |-  ( 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 suceloni
 |-  ( ( 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 ) ) )