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

Theorem fmfnfmlem1 17988
 Description: Lemma for fmfnfm 17992. (Contributed by Jeff Hankins, 18-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
Hypotheses
Ref Expression
fmfnfm.b
fmfnfm.l
fmfnfm.f
fmfnfm.fm
Assertion
Ref Expression
fmfnfmlem1
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,   ,,

Proof of Theorem fmfnfmlem1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 fmfnfm.b . . . . 5
2 fbssfi 17871 . . . . 5
31, 2sylan 459 . . . 4
4 imass2 5242 . . . . . . 7
5 sstr2 3357 . . . . . . 7
64, 5syl 16 . . . . . 6
76com12 30 . . . . 5
87reximdv 2819 . . . 4
93, 8syl5com 29 . . 3
10 fmfnfm.l . . . . . . . 8
11 filtop 17889 . . . . . . . 8
1210, 11syl 16 . . . . . . 7
13 fmfnfm.f . . . . . . 7
14 elfm 17981 . . . . . . 7
1512, 1, 13, 14syl3anc 1185 . . . . . 6
16 fmfnfm.fm . . . . . . 7
1716sseld 3349 . . . . . 6
1815, 17sylbird 228 . . . . 5
1918exp3acom23 1382 . . . 4