Metamath Proof Explorer

Theorem cantnfle

Description: A lower bound on the CNF function. Since ( ( A CNF B )F ) is defined as the sum of ( A ^o x ) .o ( Fx ) over all x in the support of F , it is larger than any of these terms (and all other terms are zero, so we can extend the statement to all C e. B instead of just those C in the support). (Contributed by Mario Carneiro, 28-May-2015) (Revised by AV, 28-Jun-2019)

Ref Expression
Hypotheses cantnfs.s 
|- S = dom ( A CNF B )
cantnfs.a 
|- ( ph -> A e. On )
cantnfs.b 
|- ( ph -> B e. On )
cantnfcl.g 
|- G = OrdIso ( _E , ( F supp (/) ) )
cantnfcl.f 
|- ( ph -> F e. S )
cantnfval.h 
|- H = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) ) , (/) )
cantnfle.c 
|- ( ph -> C e. B )
Assertion cantnfle 
|- ( ph -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( ( A CNF B ) ` F ) )

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 cantnfcl.g 
 |-  G = OrdIso ( _E , ( F supp (/) ) )
5 cantnfcl.f 
 |-  ( ph -> F e. S )
6 cantnfval.h 
 |-  H = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) ) , (/) )
7 cantnfle.c 
 |-  ( ph -> C e. B )
8 oveq2 
 |-  ( ( F ` C ) = (/) -> ( ( A ^o C ) .o ( F ` C ) ) = ( ( A ^o C ) .o (/) ) )
9 8 sseq1d 
 |-  ( ( F ` C ) = (/) -> ( ( ( A ^o C ) .o ( F ` C ) ) C_ ( ( A CNF B ) ` F ) <-> ( ( A ^o C ) .o (/) ) C_ ( ( A CNF B ) ` F ) ) )
10 ovexd 
 |-  ( ph -> ( F supp (/) ) e. _V )
11 1 2 3 4 5 cantnfcl 
 |-  ( ph -> ( _E We ( F supp (/) ) /\ dom G e. _om ) )
12 11 simpld 
 |-  ( ph -> _E We ( F supp (/) ) )
13 4 oiiso 
 |-  ( ( ( F supp (/) ) e. _V /\ _E We ( F supp (/) ) ) -> G Isom _E , _E ( dom G , ( F supp (/) ) ) )
14 10 12 13 syl2anc 
 |-  ( ph -> G Isom _E , _E ( dom G , ( F supp (/) ) ) )
15 isof1o 
 |-  ( G Isom _E , _E ( dom G , ( F supp (/) ) ) -> G : dom G -1-1-onto-> ( F supp (/) ) )
16 14 15 syl 
 |-  ( ph -> G : dom G -1-1-onto-> ( F supp (/) ) )
17 16 adantr 
 |-  ( ( ph /\ ( F ` C ) =/= (/) ) -> G : dom G -1-1-onto-> ( F supp (/) ) )
18 f1ocnv 
 |-  ( G : dom G -1-1-onto-> ( F supp (/) ) -> `' G : ( F supp (/) ) -1-1-onto-> dom G )
19 f1of 
 |-  ( `' G : ( F supp (/) ) -1-1-onto-> dom G -> `' G : ( F supp (/) ) --> dom G )
20 17 18 19 3syl 
 |-  ( ( ph /\ ( F ` C ) =/= (/) ) -> `' G : ( F supp (/) ) --> dom G )
21 7 anim1i 
 |-  ( ( ph /\ ( F ` C ) =/= (/) ) -> ( C e. B /\ ( F ` C ) =/= (/) ) )
22 1 2 3 cantnfs 
 |-  ( ph -> ( F e. S <-> ( F : B --> A /\ F finSupp (/) ) ) )
23 5 22 mpbid 
 |-  ( ph -> ( F : B --> A /\ F finSupp (/) ) )
24 23 simpld 
 |-  ( ph -> F : B --> A )
25 24 adantr 
 |-  ( ( ph /\ ( F ` C ) =/= (/) ) -> F : B --> A )
26 25 ffnd 
 |-  ( ( ph /\ ( F ` C ) =/= (/) ) -> F Fn B )
27 3 adantr 
 |-  ( ( ph /\ ( F ` C ) =/= (/) ) -> B e. On )
28 0ex 
 |-  (/) e. _V
29 28 a1i 
 |-  ( ( ph /\ ( F ` C ) =/= (/) ) -> (/) e. _V )
30 elsuppfn 
 |-  ( ( F Fn B /\ B e. On /\ (/) e. _V ) -> ( C e. ( F supp (/) ) <-> ( C e. B /\ ( F ` C ) =/= (/) ) ) )
31 26 27 29 30 syl3anc 
 |-  ( ( ph /\ ( F ` C ) =/= (/) ) -> ( C e. ( F supp (/) ) <-> ( C e. B /\ ( F ` C ) =/= (/) ) ) )
32 21 31 mpbird 
 |-  ( ( ph /\ ( F ` C ) =/= (/) ) -> C e. ( F supp (/) ) )
33 20 32 ffvelcdmd 
 |-  ( ( ph /\ ( F ` C ) =/= (/) ) -> ( `' G ` C ) e. dom G )
34 11 simprd 
 |-  ( ph -> dom G e. _om )
35 34 adantr 
 |-  ( ( ph /\ ( F ` C ) =/= (/) ) -> dom G e. _om )
36 eqimss 
 |-  ( x = dom G -> x C_ dom G )
37 36 biantrurd 
 |-  ( x = dom G -> ( ( `' G ` C ) e. x <-> ( x C_ dom G /\ ( `' G ` C ) e. x ) ) )
38 eleq2 
 |-  ( x = dom G -> ( ( `' G ` C ) e. x <-> ( `' G ` C ) e. dom G ) )
39 37 38 bitr3d 
 |-  ( x = dom G -> ( ( x C_ dom G /\ ( `' G ` C ) e. x ) <-> ( `' G ` C ) e. dom G ) )
40 fveq2 
 |-  ( x = dom G -> ( H ` x ) = ( H ` dom G ) )
41 40 sseq2d 
 |-  ( x = dom G -> ( ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` x ) <-> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` dom G ) ) )
42 39 41 imbi12d 
 |-  ( x = dom G -> ( ( ( x C_ dom G /\ ( `' G ` C ) e. x ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` x ) ) <-> ( ( `' G ` C ) e. dom G -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` dom G ) ) ) )
43 42 imbi2d 
 |-  ( x = dom G -> ( ( ( ph /\ ( F ` C ) =/= (/) ) -> ( ( x C_ dom G /\ ( `' G ` C ) e. x ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` x ) ) ) <-> ( ( ph /\ ( F ` C ) =/= (/) ) -> ( ( `' G ` C ) e. dom G -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` dom G ) ) ) ) )
44 sseq1 
 |-  ( x = (/) -> ( x C_ dom G <-> (/) C_ dom G ) )
45 eleq2 
 |-  ( x = (/) -> ( ( `' G ` C ) e. x <-> ( `' G ` C ) e. (/) ) )
46 44 45 anbi12d 
 |-  ( x = (/) -> ( ( x C_ dom G /\ ( `' G ` C ) e. x ) <-> ( (/) C_ dom G /\ ( `' G ` C ) e. (/) ) ) )
47 fveq2 
 |-  ( x = (/) -> ( H ` x ) = ( H ` (/) ) )
48 47 sseq2d 
 |-  ( x = (/) -> ( ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` x ) <-> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` (/) ) ) )
49 46 48 imbi12d 
 |-  ( x = (/) -> ( ( ( x C_ dom G /\ ( `' G ` C ) e. x ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` x ) ) <-> ( ( (/) C_ dom G /\ ( `' G ` C ) e. (/) ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` (/) ) ) ) )
50 sseq1 
 |-  ( x = y -> ( x C_ dom G <-> y C_ dom G ) )
51 eleq2 
 |-  ( x = y -> ( ( `' G ` C ) e. x <-> ( `' G ` C ) e. y ) )
52 50 51 anbi12d 
 |-  ( x = y -> ( ( x C_ dom G /\ ( `' G ` C ) e. x ) <-> ( y C_ dom G /\ ( `' G ` C ) e. y ) ) )
53 fveq2 
 |-  ( x = y -> ( H ` x ) = ( H ` y ) )
54 53 sseq2d 
 |-  ( x = y -> ( ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` x ) <-> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` y ) ) )
55 52 54 imbi12d 
 |-  ( x = y -> ( ( ( x C_ dom G /\ ( `' G ` C ) e. x ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` x ) ) <-> ( ( y C_ dom G /\ ( `' G ` C ) e. y ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` y ) ) ) )
56 sseq1 
 |-  ( x = suc y -> ( x C_ dom G <-> suc y C_ dom G ) )
57 eleq2 
 |-  ( x = suc y -> ( ( `' G ` C ) e. x <-> ( `' G ` C ) e. suc y ) )
58 56 57 anbi12d 
 |-  ( x = suc y -> ( ( x C_ dom G /\ ( `' G ` C ) e. x ) <-> ( suc y C_ dom G /\ ( `' G ` C ) e. suc y ) ) )
59 fveq2 
 |-  ( x = suc y -> ( H ` x ) = ( H ` suc y ) )
60 59 sseq2d 
 |-  ( x = suc y -> ( ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` x ) <-> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` suc y ) ) )
61 58 60 imbi12d 
 |-  ( x = suc y -> ( ( ( x C_ dom G /\ ( `' G ` C ) e. x ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` x ) ) <-> ( ( suc y C_ dom G /\ ( `' G ` C ) e. suc y ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` suc y ) ) ) )
62 noel 
 |-  -. ( `' G ` C ) e. (/)
63 62 pm2.21i 
 |-  ( ( `' G ` C ) e. (/) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` (/) ) )
64 63 adantl 
 |-  ( ( (/) C_ dom G /\ ( `' G ` C ) e. (/) ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` (/) ) )
65 64 a1i 
 |-  ( ( ph /\ ( F ` C ) =/= (/) ) -> ( ( (/) C_ dom G /\ ( `' G ` C ) e. (/) ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` (/) ) ) )
66 fvex 
 |-  ( `' G ` C ) e. _V
67 66 elsuc 
 |-  ( ( `' G ` C ) e. suc y <-> ( ( `' G ` C ) e. y \/ ( `' G ` C ) = y ) )
68 sssucid 
 |-  y C_ suc y
69 sstr 
 |-  ( ( y C_ suc y /\ suc y C_ dom G ) -> y C_ dom G )
70 68 69 mpan 
 |-  ( suc y C_ dom G -> y C_ dom G )
71 70 ad2antrl 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ ( suc y C_ dom G /\ ( `' G ` C ) e. y ) ) -> y C_ dom G )
72 simprr 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ ( suc y C_ dom G /\ ( `' G ` C ) e. y ) ) -> ( `' G ` C ) e. y )
73 pm2.27 
 |-  ( ( y C_ dom G /\ ( `' G ` C ) e. y ) -> ( ( ( y C_ dom G /\ ( `' G ` C ) e. y ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` y ) ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` y ) ) )
74 71 72 73 syl2anc 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ ( suc y C_ dom G /\ ( `' G ` C ) e. y ) ) -> ( ( ( y C_ dom G /\ ( `' G ` C ) e. y ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` y ) ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` y ) ) )
75 6 cantnfvalf 
 |-  H : _om --> On
76 75 ffvelcdmi 
 |-  ( y e. _om -> ( H ` y ) e. On )
77 76 ad2antlr 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ suc y C_ dom G ) -> ( H ` y ) e. On )
78 2 ad3antrrr 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ suc y C_ dom G ) -> A e. On )
79 3 ad3antrrr 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ suc y C_ dom G ) -> B e. On )
80 suppssdm 
 |-  ( F supp (/) ) C_ dom F
81 80 24 fssdm 
 |-  ( ph -> ( F supp (/) ) C_ B )
82 81 ad3antrrr 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ suc y C_ dom G ) -> ( F supp (/) ) C_ B )
83 simpr 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ suc y C_ dom G ) -> suc y C_ dom G )
84 sucidg 
 |-  ( y e. _om -> y e. suc y )
85 84 ad2antlr 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ suc y C_ dom G ) -> y e. suc y )
86 83 85 sseldd 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ suc y C_ dom G ) -> y e. dom G )
87 4 oif 
 |-  G : dom G --> ( F supp (/) )
88 87 ffvelcdmi 
 |-  ( y e. dom G -> ( G ` y ) e. ( F supp (/) ) )
89 86 88 syl 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ suc y C_ dom G ) -> ( G ` y ) e. ( F supp (/) ) )
90 82 89 sseldd 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ suc y C_ dom G ) -> ( G ` y ) e. B )
91 onelon 
 |-  ( ( B e. On /\ ( G ` y ) e. B ) -> ( G ` y ) e. On )
92 79 90 91 syl2anc 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ suc y C_ dom G ) -> ( G ` y ) e. On )
93 oecl 
 |-  ( ( A e. On /\ ( G ` y ) e. On ) -> ( A ^o ( G ` y ) ) e. On )
94 78 92 93 syl2anc 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ suc y C_ dom G ) -> ( A ^o ( G ` y ) ) e. On )
95 24 ad3antrrr 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ suc y C_ dom G ) -> F : B --> A )
96 95 90 ffvelcdmd 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ suc y C_ dom G ) -> ( F ` ( G ` y ) ) e. A )
97 onelon 
 |-  ( ( A e. On /\ ( F ` ( G ` y ) ) e. A ) -> ( F ` ( G ` y ) ) e. On )
98 78 96 97 syl2anc 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ suc y C_ dom G ) -> ( F ` ( G ` y ) ) e. On )
99 omcl 
 |-  ( ( ( A ^o ( G ` y ) ) e. On /\ ( F ` ( G ` y ) ) e. On ) -> ( ( A ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) e. On )
100 94 98 99 syl2anc 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ suc y C_ dom G ) -> ( ( A ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) e. On )
101 oaword2 
 |-  ( ( ( H ` y ) e. On /\ ( ( A ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) e. On ) -> ( H ` y ) C_ ( ( ( A ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) +o ( H ` y ) ) )
102 77 100 101 syl2anc 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ suc y C_ dom G ) -> ( H ` y ) C_ ( ( ( A ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) +o ( H ` y ) ) )
103 1 2 3 4 5 6 cantnfsuc 
 |-  ( ( ph /\ y e. _om ) -> ( H ` suc y ) = ( ( ( A ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) +o ( H ` y ) ) )
104 103 ad4ant13 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ suc y C_ dom G ) -> ( H ` suc y ) = ( ( ( A ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) +o ( H ` y ) ) )
105 102 104 sseqtrrd 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ suc y C_ dom G ) -> ( H ` y ) C_ ( H ` suc y ) )
106 sstr 
 |-  ( ( ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` y ) /\ ( H ` y ) C_ ( H ` suc y ) ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` suc y ) )
107 106 expcom 
 |-  ( ( H ` y ) C_ ( H ` suc y ) -> ( ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` y ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` suc y ) ) )
108 105 107 syl 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ suc y C_ dom G ) -> ( ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` y ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` suc y ) ) )
109 108 adantrr 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ ( suc y C_ dom G /\ ( `' G ` C ) e. y ) ) -> ( ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` y ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` suc y ) ) )
110 74 109 syld 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ ( suc y C_ dom G /\ ( `' G ` C ) e. y ) ) -> ( ( ( y C_ dom G /\ ( `' G ` C ) e. y ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` y ) ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` suc y ) ) )
111 110 expr 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ suc y C_ dom G ) -> ( ( `' G ` C ) e. y -> ( ( ( y C_ dom G /\ ( `' G ` C ) e. y ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` y ) ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` suc y ) ) ) )
112 simprr 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ ( suc y C_ dom G /\ ( `' G ` C ) = y ) ) -> ( `' G ` C ) = y )
113 112 fveq2d 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ ( suc y C_ dom G /\ ( `' G ` C ) = y ) ) -> ( G ` ( `' G ` C ) ) = ( G ` y ) )
114 f1ocnvfv2 
 |-  ( ( G : dom G -1-1-onto-> ( F supp (/) ) /\ C e. ( F supp (/) ) ) -> ( G ` ( `' G ` C ) ) = C )
115 17 32 114 syl2anc 
 |-  ( ( ph /\ ( F ` C ) =/= (/) ) -> ( G ` ( `' G ` C ) ) = C )
116 115 ad2antrr 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ ( suc y C_ dom G /\ ( `' G ` C ) = y ) ) -> ( G ` ( `' G ` C ) ) = C )
117 113 116 eqtr3d 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ ( suc y C_ dom G /\ ( `' G ` C ) = y ) ) -> ( G ` y ) = C )
118 117 oveq2d 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ ( suc y C_ dom G /\ ( `' G ` C ) = y ) ) -> ( A ^o ( G ` y ) ) = ( A ^o C ) )
119 117 fveq2d 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ ( suc y C_ dom G /\ ( `' G ` C ) = y ) ) -> ( F ` ( G ` y ) ) = ( F ` C ) )
120 118 119 oveq12d 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ ( suc y C_ dom G /\ ( `' G ` C ) = y ) ) -> ( ( A ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) = ( ( A ^o C ) .o ( F ` C ) ) )
121 oaword1 
 |-  ( ( ( ( A ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) e. On /\ ( H ` y ) e. On ) -> ( ( A ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) C_ ( ( ( A ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) +o ( H ` y ) ) )
122 100 77 121 syl2anc 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ suc y C_ dom G ) -> ( ( A ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) C_ ( ( ( A ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) +o ( H ` y ) ) )
123 122 adantrr 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ ( suc y C_ dom G /\ ( `' G ` C ) = y ) ) -> ( ( A ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) C_ ( ( ( A ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) +o ( H ` y ) ) )
124 120 123 eqsstrrd 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ ( suc y C_ dom G /\ ( `' G ` C ) = y ) ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( ( ( A ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) +o ( H ` y ) ) )
125 103 ad4ant13 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ ( suc y C_ dom G /\ ( `' G ` C ) = y ) ) -> ( H ` suc y ) = ( ( ( A ^o ( G ` y ) ) .o ( F ` ( G ` y ) ) ) +o ( H ` y ) ) )
126 124 125 sseqtrrd 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ ( suc y C_ dom G /\ ( `' G ` C ) = y ) ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` suc y ) )
127 126 expr 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ suc y C_ dom G ) -> ( ( `' G ` C ) = y -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` suc y ) ) )
128 127 a1dd 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ suc y C_ dom G ) -> ( ( `' G ` C ) = y -> ( ( ( y C_ dom G /\ ( `' G ` C ) e. y ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` y ) ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` suc y ) ) ) )
129 111 128 jaod 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ suc y C_ dom G ) -> ( ( ( `' G ` C ) e. y \/ ( `' G ` C ) = y ) -> ( ( ( y C_ dom G /\ ( `' G ` C ) e. y ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` y ) ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` suc y ) ) ) )
130 67 129 biimtrid 
 |-  ( ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) /\ suc y C_ dom G ) -> ( ( `' G ` C ) e. suc y -> ( ( ( y C_ dom G /\ ( `' G ` C ) e. y ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` y ) ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` suc y ) ) ) )
131 130 expimpd 
 |-  ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) -> ( ( suc y C_ dom G /\ ( `' G ` C ) e. suc y ) -> ( ( ( y C_ dom G /\ ( `' G ` C ) e. y ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` y ) ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` suc y ) ) ) )
132 131 com23 
 |-  ( ( ( ph /\ ( F ` C ) =/= (/) ) /\ y e. _om ) -> ( ( ( y C_ dom G /\ ( `' G ` C ) e. y ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` y ) ) -> ( ( suc y C_ dom G /\ ( `' G ` C ) e. suc y ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` suc y ) ) ) )
133 132 expcom 
 |-  ( y e. _om -> ( ( ph /\ ( F ` C ) =/= (/) ) -> ( ( ( y C_ dom G /\ ( `' G ` C ) e. y ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` y ) ) -> ( ( suc y C_ dom G /\ ( `' G ` C ) e. suc y ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` suc y ) ) ) ) )
134 49 55 61 65 133 finds2 
 |-  ( x e. _om -> ( ( ph /\ ( F ` C ) =/= (/) ) -> ( ( x C_ dom G /\ ( `' G ` C ) e. x ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` x ) ) ) )
135 43 134 vtoclga 
 |-  ( dom G e. _om -> ( ( ph /\ ( F ` C ) =/= (/) ) -> ( ( `' G ` C ) e. dom G -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` dom G ) ) ) )
136 35 135 mpcom 
 |-  ( ( ph /\ ( F ` C ) =/= (/) ) -> ( ( `' G ` C ) e. dom G -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` dom G ) ) )
137 33 136 mpd 
 |-  ( ( ph /\ ( F ` C ) =/= (/) ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( H ` dom G ) )
138 1 2 3 4 5 6 cantnfval 
 |-  ( ph -> ( ( A CNF B ) ` F ) = ( H ` dom G ) )
139 138 adantr 
 |-  ( ( ph /\ ( F ` C ) =/= (/) ) -> ( ( A CNF B ) ` F ) = ( H ` dom G ) )
140 137 139 sseqtrrd 
 |-  ( ( ph /\ ( F ` C ) =/= (/) ) -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( ( A CNF B ) ` F ) )
141 onelon 
 |-  ( ( B e. On /\ C e. B ) -> C e. On )
142 3 7 141 syl2anc 
 |-  ( ph -> C e. On )
143 oecl 
 |-  ( ( A e. On /\ C e. On ) -> ( A ^o C ) e. On )
144 2 142 143 syl2anc 
 |-  ( ph -> ( A ^o C ) e. On )
145 om0 
 |-  ( ( A ^o C ) e. On -> ( ( A ^o C ) .o (/) ) = (/) )
146 144 145 syl 
 |-  ( ph -> ( ( A ^o C ) .o (/) ) = (/) )
147 0ss 
 |-  (/) C_ ( ( A CNF B ) ` F )
148 146 147 eqsstrdi 
 |-  ( ph -> ( ( A ^o C ) .o (/) ) C_ ( ( A CNF B ) ` F ) )
149 9 140 148 pm2.61ne 
 |-  ( ph -> ( ( A ^o C ) .o ( F ` C ) ) C_ ( ( A CNF B ) ` F ) )