MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnfcomlem Unicode version

Theorem cnfcomlem 8164
Description: Lemma for cnfcom 8165. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 3-Jul-2019.)
Hypotheses
Ref Expression
cnfcom.s
cnfcom.a
cnfcom.b
cnfcom.f
cnfcom.g
cnfcom.h
cnfcom.t
cnfcom.m
cnfcom.k
cnfcom.1
cnfcom.2
cnfcom.3
Assertion
Ref Expression
cnfcomlem
Distinct variable groups:   , , ,   ,I, ,   ,M   , , , ,   ,   , , , ,   , ,   S, ,

Proof of Theorem cnfcomlem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 omelon 8084 . . . . . . 7
2 cnfcom.a . . . . . . . 8
3 suppssdm 6931 . . . . . . . . . 10
4 cnfcom.f . . . . . . . . . . . . . 14
5 cnfcom.s . . . . . . . . . . . . . . . . 17
61a1i 11 . . . . . . . . . . . . . . . . 17
75, 6, 2cantnff1o 8158 . . . . . . . . . . . . . . . 16
8 f1ocnv 5833 . . . . . . . . . . . . . . . 16
9 f1of 5821 . . . . . . . . . . . . . . . 16
107, 8, 93syl 20 . . . . . . . . . . . . . . 15
11 cnfcom.b . . . . . . . . . . . . . . 15
1210, 11ffvelrnd 6032 . . . . . . . . . . . . . 14
134, 12syl5eqel 2549 . . . . . . . . . . . . 13
145, 6, 2cantnfs 8106 . . . . . . . . . . . . 13
1513, 14mpbid 210 . . . . . . . . . . . 12
1615simpld 459 . . . . . . . . . . 11
17 fdm 5740 . . . . . . . . . . 11
1816, 17syl 16 . . . . . . . . . 10
193, 18syl5sseq 3551 . . . . . . . . 9
20 cnfcom.1 . . . . . . . . . 10
21 cnfcom.g . . . . . . . . . . . 12
2221oif 7976 . . . . . . . . . . 11
2322ffvelrni 6030 . . . . . . . . . 10
2420, 23syl 16 . . . . . . . . 9
2519, 24sseldd 3504 . . . . . . . 8
26 onelon 4908 . . . . . . . 8
272, 25, 26syl2anc 661 . . . . . . 7
28 oecl 7206 . . . . . . 7
291, 27, 28sylancr 663 . . . . . 6
3016, 25ffvelrnd 6032 . . . . . . 7
31 nnon 6706 . . . . . . 7
3230, 31syl 16 . . . . . 6
33 omcl 7205 . . . . . 6
3429, 32, 33syl2anc 661 . . . . 5
355, 6, 2, 21, 13cantnfcl 8107 . . . . . . . 8
3635simprd 463 . . . . . . 7
37 elnn 6710 . . . . . . 7
3820, 36, 37syl2anc 661 . . . . . 6
39 cnfcom.h . . . . . . . 8
4039cantnfvalf 8105 . . . . . . 7
4140ffvelrni 6030 . . . . . 6
4238, 41syl 16 . . . . 5
43 eqid 2457 . . . . . 6
4443oacomf1o 7233 . . . . 5
4534, 42, 44syl2anc 661 . . . 4
46 cnfcom.t . . . . . . . 8
4746seqomsuc 7141 . . . . . . 7
4838, 47syl 16 . . . . . 6
49 nfcv 2619 . . . . . . . . 9
50 nfcv 2619 . . . . . . . . 9
51 nfcv 2619 . . . . . . . . 9
52 nfcv 2619 . . . . . . . . 9
53 cnfcom.k . . . . . . . . . 10
54 oveq2 6304 . . . . . . . . . . . . 13
5554cbvmptv 4543 . . . . . . . . . . . 12
56 cnfcom.m . . . . . . . . . . . . . 14
57 simpl 457 . . . . . . . . . . . . . . . . 17
5857fveq2d 5875 . . . . . . . . . . . . . . . 16
5958oveq2d 6312 . . . . . . . . . . . . . . 15
6058fveq2d 5875 . . . . . . . . . . . . . . 15
6159, 60oveq12d 6314 . . . . . . . . . . . . . 14
6256, 61syl5eq 2510 . . . . . . . . . . . . 13
63 simpr 461 . . . . . . . . . . . . . . 15
6463dmeqd 5210 . . . . . . . . . . . . . 14
6564oveq1d 6311 . . . . . . . . . . . . 13
6662, 65mpteq12dv 4530 . . . . . . . . . . . 12
6755, 66syl5eq 2510 . . . . . . . . . . 11
68 oveq2 6304 . . . . . . . . . . . . . 14
6968cbvmptv 4543 . . . . . . . . . . . . 13
7062oveq1d 6311 . . . . . . . . . . . . . 14
7164, 70mpteq12dv 4530 . . . . . . . . . . . . 13
7269, 71syl5eq 2510 . . . . . . . . . . . 12
7372cnveqd 5183 . . . . . . . . . . 11
7467, 73uneq12d 3658 . . . . . . . . . 10
7553, 74syl5eq 2510 . . . . . . . . 9
7649, 50, 51, 52, 75cbvmpt2 6376 . . . . . . . 8
7776a1i 11 . . . . . . 7
78 simprl 756 . . . . . . . . . . . 12
7978fveq2d 5875 . . . . . . . . . . 11
8079oveq2d 6312 . . . . . . . . . 10
8179fveq2d 5875 . . . . . . . . . 10
8280, 81oveq12d 6314 . . . . . . . . 9
83 simpr 461 . . . . . . . . . . . 12
8483dmeqd 5210 . . . . . . . . . . 11
85 cnfcom.3 . . . . . . . . . . . 12
86 f1odm 5825 . . . . . . . . . . . 12
8785, 86syl 16 . . . . . . . . . . 11
8884, 87sylan9eqr 2520 . . . . . . . . . 10
8988oveq1d 6311 . . . . . . . . 9
9082, 89mpteq12dv 4530 . . . . . . . 8
9182oveq1d 6311 . . . . . . . . . 10
9288, 91mpteq12dv 4530 . . . . . . . . 9
9392cnveqd 5183 . . . . . . . 8
9490, 93uneq12d 3658 . . . . . . 7
95 elex 3118 . . . . . . . 8
9620, 95syl 16 . . . . . . 7
97 fvex 5881 . . . . . . . 8
9897a1i 11 . . . . . . 7
99 ovex 6324 . . . . . . . . . 10
10099mptex 6143 . . . . . . . . 9
101 fvex 5881 . . . . . . . . . . 11
102101mptex 6143 . . . . . . . . . 10
103102cnvex 6747 . . . . . . . . 9
104100, 103unex 6598 . . . . . . . 8
105104a1i 11 . . . . . . 7
10677, 94, 96, 98, 105ovmpt2d 6430 . . . . . 6
10748, 106eqtrd 2498 . . . . 5
108 f1oeq1 5812 . . . . 5
109107, 108syl 16 . . . 4
11045, 109mpbird 232 . . 3
1111a1i 11 . . . . . 6
112 simpl 457 . . . . . 6
113 simpr 461 . . . . . 6
11456oveq1i 6306 . . . . . . . . . 10
115114a1i 11 . . . . . . . . 9
116115mpt2eq3ia 6362 . . . . . . . 8
117 eqid 2457 . . . . . . . 8
118 seqomeq12 7138 . . . . . . . 8
119116, 117, 118mp2an 672 . . . . . . 7
12039, 119eqtri 2486 . . . . . 6
1215, 111, 112, 21, 113, 120cantnfsuc 8110 . . . . 5
1222, 13, 38, 121syl21anc 1227 . . . 4
123 f1oeq2 5813 . . . 4
124122, 123syl 16 . . 3
125110, 124mpbird 232 . 2
126 sssucid 4960 . . . . . 6
127126, 20sseldi 3501 . . . . 5
128 epelg 4797 . . . . . . . . . . 11
12920, 128syl 16 . . . . . . . . . 10
130129biimpar 485 . . . . . . . . 9
1312, 19ssexd 4599 . . . . . . . . . . . 12
13235simpld 459 . . . . . . . . . . . 12
13321oiiso 7983 . . . . . . . . . . . 12
134131, 132, 133syl2anc 661 . . . . . . . . . . 11
135134adantr 465 . . . . . . . . . 10
13621oicl 7975 . . . . . . . . . . . 12
137 ordelss 4899 . . . . . . . . . . . 12
138136, 20, 137sylancr 663 . . . . . . . . . . 11
139138sselda 3503 . . . . . . . . . 10
14020adantr 465 . . . . . . . . . 10
141 isorel 6222 . . . . . . . . . 10
142135, 139, 140, 141syl12anc 1226 . . . . . . . . 9
143130, 142mpbid 210 . . . . . . . 8
144 fvex 5881 . . . . . . . . 9
145144epelc 4798 . . . . . . . 8
146143, 145sylib 196 . . . . . . 7
147146ralrimiva 2871 . . . . . 6
148 ffun 5738 . . . . . . . 8
14922, 148ax-mp 5 . . . . . . 7
150 funimass4 5924 . . . . . . 7
151149, 138, 150sylancr 663 . . . . . 6
152147, 151mpbird 232 . . . . 5
1531a1i 11 . . . . . 6
154 simpll 753 . . . . . 6
155 simplr 755 . . . . . 6
156 peano1 6719 . . . . . . 7
157156a1i 11 . . . . . 6
158 simpr1 1002 . . . . . 6
159 simpr2 1003 . . . . . 6
160 simpr3 1004 . . . . . 6
1615, 153, 154, 21, 155, 120, 157, 158, 159, 160cantnflt 8112 . . . . 5
1622, 13, 127, 27, 152, 161syl23anc 1235 . . . 4
163 ffn 5736 . . . . . . . . . 10
16416, 163syl 16 . . . . . . . . 9
165 0ex 4582 . . . . . . . . . 10
166165a1i 11 . . . . . . . . 9
167 elsuppfn 6926 . . . . . . . . 9
168164, 2, 166, 167syl3anc 1228 . . . . . . . 8
169 simpr 461 . . . . . . . 8
170168, 169syl6bi 228 . . . . . . 7
17124, 170mpd 15 . . . . . 6
172 on0eln0 4938 . . . . . . 7
17332, 172syl 16 . . . . . 6
174171, 173mpbird 232 . . . . 5
175 omword1 7241 . . . . 5
17629, 32, 174, 175syl21anc 1227 . . . 4
177 oaabs2 7313 . . . 4
178162, 34, 176, 177syl21anc 1227 . . 3
179 f1oeq3 5814 . . 3
180178, 179syl 16 . 2
181125, 180mpbid 210 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  /\w3a 973  =wceq 1395  e.wcel 1818  =/=wne 2652  A.wral 2807   cvv 3109  u.cun 3473  C_wss 3475   c0 3784   class class class wbr 4452  e.cmpt 4510