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

Theorem cfsmolem 8671
Description: Lemma for cfsmo 8672. (Contributed by Mario Carneiro, 28-Feb-2013.)
Hypotheses
Ref Expression
cfsmolem.2
cfsmolem.3
Assertion
Ref Expression
cfsmolem
Distinct variable groups:   , , , , ,   , , ,   , , ,

Proof of Theorem cfsmolem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cff1 8659 . 2
2 cfon 8656 . . . . . . . . . . . 12
32oneli 4990 . . . . . . . . . . 11
433ad2ant3 1019 . . . . . . . . . 10
5 eleq1 2529 . . . . . . . . . . . . 13
653anbi3d 1305 . . . . . . . . . . . 12
7 fveq2 5871 . . . . . . . . . . . . 13
87eleq1d 2526 . . . . . . . . . . . 12
96, 8imbi12d 320 . . . . . . . . . . 11
10 simpl1 999 . . . . . . . . . . . . . . . 16
11 simpl2 1000 . . . . . . . . . . . . . . . 16
12 ontr1 4929 . . . . . . . . . . . . . . . . . . 19
132, 12ax-mp 5 . . . . . . . . . . . . . . . . . 18
1413ancoms 453 . . . . . . . . . . . . . . . . 17
15143ad2antl3 1160 . . . . . . . . . . . . . . . 16
16 pm2.27 39 . . . . . . . . . . . . . . . 16
1710, 11, 15, 16syl3anc 1228 . . . . . . . . . . . . . . 15
1817ralimdva 2865 . . . . . . . . . . . . . 14
19 cfsmolem.3 . . . . . . . . . . . . . . . . . . . . 21
2019fveq1i 5872 . . . . . . . . . . . . . . . . . . . 20
21 fvres 5885 . . . . . . . . . . . . . . . . . . . 20
2220, 21syl5eq 2510 . . . . . . . . . . . . . . . . . . 19
23 recsval 7089 . . . . . . . . . . . . . . . . . . . . . 22
24 recsfnon 7088 . . . . . . . . . . . . . . . . . . . . . . . . 25
25 fnfun 5683 . . . . . . . . . . . . . . . . . . . . . . . . 25
2624, 25ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . 24
27 vex 3112 . . . . . . . . . . . . . . . . . . . . . . . 24
28 resfunexg 6137 . . . . . . . . . . . . . . . . . . . . . . . 24
2926, 27, 28mp2an 672 . . . . . . . . . . . . . . . . . . . . . . 23
30 dmeq 5208 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3130fveq2d 5875 . . . . . . . . . . . . . . . . . . . . . . . . 25
32 fveq1 5870 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
33 suceq 4948 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
3432, 33syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3530, 34iuneq12d 4356 . . . . . . . . . . . . . . . . . . . . . . . . 25
3631, 35uneq12d 3658 . . . . . . . . . . . . . . . . . . . . . . . 24
37 cfsmolem.2 . . . . . . . . . . . . . . . . . . . . . . . 24
38 fvex 5881 . . . . . . . . . . . . . . . . . . . . . . . . 25
3929dmex 6733 . . . . . . . . . . . . . . . . . . . . . . . . . 26
40 fvex 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4140sucex 6646 . . . . . . . . . . . . . . . . . . . . . . . . . 26
4239, 41iunex 6780 . . . . . . . . . . . . . . . . . . . . . . . . 25
4338, 42unex 6598 . . . . . . . . . . . . . . . . . . . . . . . 24
4436, 37, 43fvmpt 5956 . . . . . . . . . . . . . . . . . . . . . . 23
4529, 44ax-mp 5 . . . . . . . . . . . . . . . . . . . . . 22
4623, 45syl6eq 2514 . . . . . . . . . . . . . . . . . . . . 21
47 onss 6626 . . . . . . . . . . . . . . . . . . . . . . 23
48 fnssres 5699 . . . . . . . . . . . . . . . . . . . . . . 23
4924, 47, 48sylancr 663 . . . . . . . . . . . . . . . . . . . . . 22
50 fndm 5685 . . . . . . . . . . . . . . . . . . . . . 22
51 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . 23
52 iuneq1 4344 . . . . . . . . . . . . . . . . . . . . . . . 24
53 fvres 5885 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
54 suceq 4948 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
5553, 54syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26
5655iuneq2i 4349 . . . . . . . . . . . . . . . . . . . . . . . . 25
57 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
58 suceq 4948 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
5957, 58syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26
6059cbviunv 4369 . . . . . . . . . . . . . . . . . . . . . . . . 25
6156, 60eqtr4i 2489 . . . . . . . . . . . . . . . . . . . . . . . 24
6252, 61syl6eq 2514 . . . . . . . . . . . . . . . . . . . . . . 23
6351, 62uneq12d 3658 . . . . . . . . . . . . . . . . . . . . . 22
6449, 50, 633syl 20 . . . . . . . . . . . . . . . . . . . . 21
6546, 64eqtrd 2498 . . . . . . . . . . . . . . . . . . . 20
663, 65syl 16 . . . . . . . . . . . . . . . . . . 19
6722, 66eqtrd 2498 . . . . . . . . . . . . . . . . . 18
68673ad2ant2 1018 . . . . . . . . . . . . . . . . 17
69 eloni 4893 . . . . . . . . . . . . . . . . . . . 20
7069adantl 466 . . . . . . . . . . . . . . . . . . 19
71703ad2ant1 1017 . . . . . . . . . . . . . . . . . 18
72 f1f 5786 . . . . . . . . . . . . . . . . . . . . 21
7372ffvelrnda 6031 . . . . . . . . . . . . . . . . . . . 20
7473adantlr 714 . . . . . . . . . . . . . . . . . . 19
75743adant3 1016 . . . . . . . . . . . . . . . . . 18
7619fveq1i 5872 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
77 fvres 5885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
7813, 77syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7976, 78syl5eq 2510 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8079adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8180ancoms 453 . . . . . . . . . . . . . . . . . . . . . . . . 25
8281eleq1d 2526 . . . . . . . . . . . . . . . . . . . . . . . 24
83 ordsucss 6653 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8469, 83syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
8584ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24
8682, 85sylbid 215 . . . . . . . . . . . . . . . . . . . . . . 23
8786ralimdva 2865 . . . . . . . . . . . . . . . . . . . . . 22
88 iunss 4371 . . . . . . . . . . . . . . . . . . . . . 22
8987, 88syl6ibr 227 . . . . . . . . . . . . . . . . . . . . 21
90893impia 1193 . . . . . . . . . . . . . . . . . . . 20
91 onelon 4908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
9291ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
9392ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9482, 93sylbid 215 . . . . . . . . . . . . . . . . . . . . . . . . . 26
95 suceloni 6648 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9694, 95syl6 33 . . . . . . . . . . . . . . . . . . . . . . . . 25
9796ralimdva 2865 . . . . . . . . . . . . . . . . . . . . . . . 24
98973impia 1193 . . . . . . . . . . . . . . . . . . . . . . 23
99 fvex 5881 . . . . . . . . . . . . . . . . . . . . . . . . 25
10099sucex 6646 . . . . . . . . . . . . . . . . . . . . . . . 24
10127, 100iunonOLD 7029 . . . . . . . . . . . . . . . . . . . . . . 23
10298, 101syl 16 . . . . . . . . . . . . . . . . . . . . . 22
103 simp1 996 . . . . . . . . . . . . . . . . . . . . . 22
104 onsseleq 4924 . . . . . . . . . . . . . . . . . . . . . 22
105102, 103, 104syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21
106 idd 24 . . . . . . . . . . . . . . . . . . . . . 22
107 simpll 753 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
108 simprr 757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1093ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1103, 49syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
111110adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
11279ancoms 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
113 fvres 5885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
114113adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
115112, 114eqtr4d 2501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
116115eleq1d 2526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
117116ralbidva 2893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
118117biimpa 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
119 ffnfv 6057 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
120111, 118, 119sylanbrc 664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
121120adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
122 eleq2 2530 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
123122biimpar 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
124123adantrl 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
1251243adant1 1014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
126 onelon 4908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
127126adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
128113adantl 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
129 ffvelrn 6029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
130128, 129eqeltrrd 2546 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
131130, 91sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
132131adantlr 714 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
133 onsssuc 4970 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
134127, 132, 133syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
135134anassrs 648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
136135rexbidva 2965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
137 eliun 4335 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
138136, 137syl6bbr 263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
139138ancoms 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
1401393adant2 1015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
141125, 140mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
1421413expa 1196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
143142anassrs 648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
144143ralrimiva 2871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
145144expl 618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
146120, 145syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
147146imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
148 feq1 5718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
149 fveq1 5870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
150149sseq2d 3531 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
151150rexbidv 2968 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
152113sseq2d 3531 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
153152rexbiia 2958 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
154151, 153syl6bb 261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
155154ralbidv 2896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
156148, 155anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
15729, 156spcev 3201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
158121, 147, 157syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
159 cfflb 8660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
160159imp 429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
161108, 109, 158, 160syl21anc 1227 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
162 ontri1 4917 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
1632, 3, 162sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
164163ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
165161, 164mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
166107, 165pm2.21dd 174 . . . . . . . . . . . . . . . . . . . . . . . . . 26
167166ex 434 . . . . . . . . . . . . . . . . . . . . . . . . 25