Metamath Proof Explorer

Theorem fmfnfmlem3

Description: Lemma for fmfnfm . (Contributed by Jeff Hankins, 19-Nov-2009) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Hypotheses fmfnfm.b ⊢φ→B∈fBas⁡Y
fmfnfm.l ⊢φ→L∈Fil⁡X
fmfnfm.f ⊢φ→F:Y⟶X
fmfnfm.fm ⊢φ→XFilMapF⁡B⊆L
Assertion fmfnfmlem3 ⊢φ→fi⁡ran⁡x∈L⟼F-1x=ran⁡x∈L⟼F-1x

Proof

Step Hyp Ref Expression
1 fmfnfm.b ⊢φ→B∈fBas⁡Y
2 fmfnfm.l ⊢φ→L∈Fil⁡X
3 fmfnfm.f ⊢φ→F:Y⟶X
4 fmfnfm.fm ⊢φ→XFilMapF⁡B⊆L
5 filin ⊢L∈Fil⁡X∧y∈L∧z∈L→y∩z∈L
6 5 3expb ⊢L∈Fil⁡X∧y∈L∧z∈L→y∩z∈L
7 2 6 sylan ⊢φ∧y∈L∧z∈L→y∩z∈L
8 ffun ⊢F:Y⟶X→Fun⁡F
9 funcnvcnv ⊢Fun⁡F→Fun⁡F-1-1
10 imain ⊢Fun⁡F-1-1→F-1y∩z=F-1y∩F-1z
11 10 eqcomd ⊢Fun⁡F-1-1→F-1y∩F-1z=F-1y∩z
12 3 8 9 11 4syl ⊢φ→F-1y∩F-1z=F-1y∩z
13 12 adantr ⊢φ∧y∈L∧z∈L→F-1y∩F-1z=F-1y∩z
14 imaeq2 ⊢x=y∩z→F-1x=F-1y∩z
15 14 rspceeqv ⊢y∩z∈L∧F-1y∩F-1z=F-1y∩z→∃x∈LF-1y∩F-1z=F-1x
16 7 13 15 syl2anc ⊢φ∧y∈L∧z∈L→∃x∈LF-1y∩F-1z=F-1x
17 ineq12 ⊢s=F-1y∧t=F-1z→s∩t=F-1y∩F-1z
18 17 eqeq1d ⊢s=F-1y∧t=F-1z→s∩t=F-1x↔F-1y∩F-1z=F-1x
19 18 rexbidv ⊢s=F-1y∧t=F-1z→∃x∈Ls∩t=F-1x↔∃x∈LF-1y∩F-1z=F-1x
20 16 19 syl5ibrcom ⊢φ∧y∈L∧z∈L→s=F-1y∧t=F-1z→∃x∈Ls∩t=F-1x
21 20 rexlimdvva ⊢φ→∃y∈L∃z∈Ls=F-1y∧t=F-1z→∃x∈Ls∩t=F-1x
22 imaeq2 ⊢x=y→F-1x=F-1y
23 22 eqeq2d ⊢x=y→s=F-1x↔s=F-1y
24 23 cbvrexvw ⊢∃x∈Ls=F-1x↔∃y∈Ls=F-1y
25 imaeq2 ⊢x=z→F-1x=F-1z
26 25 eqeq2d ⊢x=z→t=F-1x↔t=F-1z
27 26 cbvrexvw ⊢∃x∈Lt=F-1x↔∃z∈Lt=F-1z
28 24 27 anbi12i ⊢∃x∈Ls=F-1x∧∃x∈Lt=F-1x↔∃y∈Ls=F-1y∧∃z∈Lt=F-1z
29 eqid ⊢x∈L⟼F-1x=x∈L⟼F-1x
30 29 elrnmpt ⊢s∈V→s∈ran⁡x∈L⟼F-1x↔∃x∈Ls=F-1x
31 30 elv ⊢s∈ran⁡x∈L⟼F-1x↔∃x∈Ls=F-1x
32 29 elrnmpt ⊢t∈V→t∈ran⁡x∈L⟼F-1x↔∃x∈Lt=F-1x
33 32 elv ⊢t∈ran⁡x∈L⟼F-1x↔∃x∈Lt=F-1x
34 31 33 anbi12i ⊢s∈ran⁡x∈L⟼F-1x∧t∈ran⁡x∈L⟼F-1x↔∃x∈Ls=F-1x∧∃x∈Lt=F-1x
35 reeanv ⊢∃y∈L∃z∈Ls=F-1y∧t=F-1z↔∃y∈Ls=F-1y∧∃z∈Lt=F-1z
36 28 34 35 3bitr4i ⊢s∈ran⁡x∈L⟼F-1x∧t∈ran⁡x∈L⟼F-1x↔∃y∈L∃z∈Ls=F-1y∧t=F-1z
37 vex ⊢s∈V
38 37 inex1 ⊢s∩t∈V
39 29 elrnmpt ⊢s∩t∈V→s∩t∈ran⁡x∈L⟼F-1x↔∃x∈Ls∩t=F-1x
40 38 39 ax-mp ⊢s∩t∈ran⁡x∈L⟼F-1x↔∃x∈Ls∩t=F-1x
41 21 36 40 3imtr4g ⊢φ→s∈ran⁡x∈L⟼F-1x∧t∈ran⁡x∈L⟼F-1x→s∩t∈ran⁡x∈L⟼F-1x
42 41 ralrimivv ⊢φ→∀s∈ran⁡x∈L⟼F-1x∀t∈ran⁡x∈L⟼F-1xs∩t∈ran⁡x∈L⟼F-1x
43 mptexg ⊢L∈Fil⁡X→x∈L⟼F-1x∈V
44 rnexg ⊢x∈L⟼F-1x∈V→ran⁡x∈L⟼F-1x∈V
45 inficl ⊢ran⁡x∈L⟼F-1x∈V→∀s∈ran⁡x∈L⟼F-1x∀t∈ran⁡x∈L⟼F-1xs∩t∈ran⁡x∈L⟼F-1x↔fi⁡ran⁡x∈L⟼F-1x=ran⁡x∈L⟼F-1x
46 2 43 44 45 4syl ⊢φ→∀s∈ran⁡x∈L⟼F-1x∀t∈ran⁡x∈L⟼F-1xs∩t∈ran⁡x∈L⟼F-1x↔fi⁡ran⁡x∈L⟼F-1x=ran⁡x∈L⟼F-1x
47 42 46 mpbid ⊢φ→fi⁡ran⁡x∈L⟼F-1x=ran⁡x∈L⟼F-1x