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

Theorem indexfi 7846
 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 30387. (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 1708 . . . . . 6
2 nfsbc1v 3347 . . . . . 6
3 sbceq1a 3338 . . . . . 6
41, 2, 3cbvrex 3081 . . . . 5
54ralbii 2888 . . . 4
6 dfsbcq 3329 . . . . 5
76ac6sfi 7782 . . . 4
85, 7sylan2b 475 . . 3
9 simpll 753 . . . . 5
10 ffn 5737 . . . . . . 7
1110ad2antrl 727 . . . . . 6
12 dffn4 5807 . . . . . 6
1311, 12sylib 196 . . . . 5
14 fofi 7824 . . . . 5
159, 13, 14syl2anc 661 . . . 4
16 frn 5743 . . . . 5
1716ad2antrl 727 . . . 4
18 fnfvelrn 6029 . . . . . . . . 9
1910, 18sylan 471 . . . . . . . 8
20 rspesbca 3415 . . . . . . . . 9
2120ex 434 . . . . . . . 8
2219, 21syl 16 . . . . . . 7
2322ralimdva 2865 . . . . . 6
2423imp 429 . . . . 5
2524adantl 466 . . . 4
26 simpr 461 . . . . . . . 8
27 simprr 757 . . . . . . . . . 10
28 nfv 1708 . . . . . . . . . . 11
29 nfsbc1v 3347 . . . . . . . . . . 11
30 fveq2 5872 . . . . . . . . . . . . 13
3130sbceq1d 3332 . . . . . . . . . . . 12
32 sbceq1a 3338 . . . . . . . . . . . 12
3331, 32bitrd 253 . . . . . . . . . . 11
3428, 29, 33cbvral 3080 . . . . . . . . . 10
3527, 34sylib 196 . . . . . . . . 9
3635r19.21bi 2826 . . . . . . . 8
37 rspesbca 3415 . . . . . . . 8
3826, 36, 37syl2anc 661 . . . . . . 7
3938ralrimiva 2871 . . . . . 6
40 dfsbcq 3329 . . . . . . . . 9
4140rexbidv 2968 . . . . . . . 8
4241ralrn 6035 . . . . . . 7
4311, 42syl 16 . . . . . 6
4439, 43mpbird 232 . . . . 5
45 nfv 1708 . . . . . 6
46 nfcv 2619 . . . . . . 7
4746, 2nfrex 2920 . . . . . 6
483rexbidv 2968 . . . . . 6
4945, 47, 48cbvral 3080 . . . . 5
5044, 49sylibr 212 . . . 4
51 sseq1 3520 . . . . . 6
52 rexeq 3055 . . . . . . 7
5352ralbidv 2896 . . . . . 6
54 raleq 3054 . . . . . 6
5551, 53, 543anbi123d 1299 . . . . 5
5655rspcev 3210 . . . 4
5715, 17, 25, 50, 56syl13anc 1230 . . 3
588, 57exlimddv 1727 . 2