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

Theorem indexfi 7250
 Description: If for every element of a finite indexing set there exists a corresponding element of another set , then there exists a finite subset of consisting only of those elements which are indexed by . Proven without the Axiom of Choice, unlike indexdom 25737. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
Assertion
Ref Expression
indexfi
Distinct variable groups:   ,,,   ,,,   ,
Allowed substitution hints:   (,)   (,,)

Proof of Theorem indexfi
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1619 . . . . . 6
2 nfsbc1v 3086 . . . . . 6
3 sbceq1a 3077 . . . . . 6
41, 2, 3cbvrex 2837 . . . . 5
54ralbii 2643 . . . 4
6 dfsbcq 3069 . . . . 5
76ac6sfi 7188 . . . 4
85, 7sylan2b 461 . . 3
9 simpll 730 . . . . . . 7
10 ffn 5469 . . . . . . . . 9
1110ad2antrl 708 . . . . . . . 8
12 dffn4 5537 . . . . . . . 8
1311, 12sylib 188 . . . . . . 7
14 fofi 7229 . . . . . . 7
159, 13, 14syl2anc 642 . . . . . 6
16 frn 5475 . . . . . . 7
1716ad2antrl 708 . . . . . 6
18 fnfvelrn 5742 . . . . . . . . . . 11
1910, 18sylan 457 . . . . . . . . . 10
20 rspesbca 3147 . . . . . . . . . . 11
2120ex 423 . . . . . . . . . 10
2219, 21syl 15 . . . . . . . . 9
2322ralimdva 2697 . . . . . . . 8
2423imp 418 . . . . . . 7
2524adantl 452 . . . . . 6
26 simpr 447 . . . . . . . . . 10
27 simprr 733 . . . . . . . . . . . 12
28 nfv 1619 . . . . . . . . . . . . 13
29 nfsbc1v 3086 . . . . . . . . . . . . 13
30 fveq2 5605 . . . . . . . . . . . . . . 15
31 dfsbcq 3069 . . . . . . . . . . . . . . 15
3230, 31syl 15 . . . . . . . . . . . . . 14
33 sbceq1a 3077 . . . . . . . . . . . . . 14
3432, 33bitrd 244 . . . . . . . . . . . . 13
3528, 29, 34cbvral 2836 . . . . . . . . . . . 12
3627, 35sylib 188 . . . . . . . . . . 11
3736r19.21bi 2717 . . . . . . . . . 10
38 rspesbca 3147 . . . . . . . . . 10
3926, 37, 38syl2anc 642 . . . . . . . . 9
4039ralrimiva 2702 . . . . . . . 8
41 dfsbcq 3069 . . . . . . . . . . 11
4241rexbidv 2640 . . . . . . . . . 10
4342ralrn 5748 . . . . . . . . 9
4411, 43syl 15 . . . . . . . 8
4540, 44mpbird 223 . . . . . . 7
46 nfv 1619 . . . . . . . 8
47 nfcv 2494 . . . . . . . . 9
4847, 2nfrex 2674 . . . . . . . 8
493rexbidv 2640 . . . . . . . 8
5046, 48, 49cbvral 2836 . . . . . . 7
5145, 50sylibr 203 . . . . . 6
52 sseq1 3275 . . . . . . . 8
53 rexeq 2813 . . . . . . . . 9
5453ralbidv 2639 . . . . . . . 8
55 raleq 2812 . . . . . . . 8
5652, 54, 553anbi123d 1252 . . . . . . 7
5756rspcev 2960 . . . . . 6
5815, 17, 25, 51, 57syl13anc 1184 . . . . 5
5958ex 423 . . . 4
6059exlimdv 1636 . . 3
618, 60mpd 14 . 2