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

Theorem cnfcomlemOLD 8172
Description: Lemma for cnfcomOLD 8173. (Contributed by Mario Carneiro, 30-May-2015.) Obsolete version of cnfcomlem 8164 as of 3-Jul-2019. (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
cnfcomOLD.s
cnfcomOLD.a
cnfcomOLD.b
cnfcomOLD.f
cnfcomOLD.g
cnfcomOLD.h
cnfcomOLD.t
cnfcomOLD.m
cnfcomOLD.k
cnfcomOLD.1
cnfcomOLD.2
cnfcomOLD.3
Assertion
Ref Expression
cnfcomlemOLD
Distinct variable groups:   , , ,   ,I, ,   ,M   , , , ,   ,   , , , ,   , ,   S, ,

Proof of Theorem cnfcomlemOLD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 omelon 8084 . . . . . . 7
2 cnfcomOLD.a . . . . . . . 8
3 cnvimass 5362 . . . . . . . . . 10
4 cnfcomOLD.f . . . . . . . . . . . . . 14
5 cnfcomOLD.s . . . . . . . . . . . . . . . . 17
61a1i 11 . . . . . . . . . . . . . . . . 17
75, 6, 2cantnff1o 8158 . . . . . . . . . . . . . . . 16
8 f1ocnv 5833 . . . . . . . . . . . . . . . 16
9 f1of 5821 . . . . . . . . . . . . . . . 16
107, 8, 93syl 20 . . . . . . . . . . . . . . 15
11 cnfcomOLD.b . . . . . . . . . . . . . . 15
1210, 11ffvelrnd 6032 . . . . . . . . . . . . . 14
134, 12syl5eqel 2549 . . . . . . . . . . . . 13
145, 6, 2cantnfsOLD 8136 . . . . . . . . . . . . 13
1513, 14mpbid 210 . . . . . . . . . . . 12
1615simpld 459 . . . . . . . . . . 11
17 fdm 5740 . . . . . . . . . . 11
1816, 17syl 16 . . . . . . . . . 10
193, 18syl5sseq 3551 . . . . . . . . 9
20 cnfcomOLD.1 . . . . . . . . . 10
21 cnfcomOLD.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, 13cantnfclOLD 8137 . . . . . . . 8
3635simprd 463 . . . . . . 7
37 elnn 6710 . . . . . . 7
3820, 36, 37syl2anc 661 . . . . . 6
39 cnfcomOLD.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 cnfcomOLD.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 cnfcomOLD.k . . . . . . . . . 10
54 oveq2 6304 . . . . . . . . . . . . 13
5554cbvmptv 4543 . . . . . . . . . . . 12
56 cnfcomOLD.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 cnfcomOLD.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, 120cantnfsucOLD 8140 . . . . 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, 160cantnfltOLD 8142 . . . . 5
1622, 13, 127, 27, 152, 161syl23anc 1235 . . . 4
163 ffn 5736 . . . . . . . . . 10
164 elpreima 6007 . . . . . . . . . 10
16516, 163, 1643syl 20 . . . . . . . . 9
16624, 165mpbid 210 . . . . . . . 8
167166simprd 463 . . . . . . 7
168 dif1o 7169 . . . . . . . 8
169168simprbi 464 . . . . . . 7
170167, 169syl 16 . . . . . 6
171 on0eln0 4938 . . . . . . 7
17232, 171syl 16 . . . . . 6
173170, 172mpbird 232 . . . . 5
174 omword1 7241 . . . . 5
17529, 32, 173, 174syl21anc 1227 . . . 4
176 oaabs2 7313 . . . 4
177162, 34, 175, 176syl21anc 1227 . . 3
178 f1oeq3 5814 . . 3
179177, 178syl 16 . 2