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 ⊢ φ → X FilMap F ⁡ B ⊆ L
Assertion fmfnfmlem3 ⊢ φ → fi ⁡ ran ⁡ x ∈ L ⟼ F -1 x = ran ⁡ x ∈ L ⟼ F -1 x

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 ⊢ φ → X FilMap F ⁡ 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 -1 y ∩ z = F -1 y ∩ F -1 z
11 10 eqcomd ⊢ Fun ⁡ F -1 -1 → F -1 y ∩ F -1 z = F -1 y ∩ z
12 3 8 9 11 4syl ⊢ φ → F -1 y ∩ F -1 z = F -1 y ∩ z
13 12 adantr ⊢ φ ∧ y ∈ L ∧ z ∈ L → F -1 y ∩ F -1 z = F -1 y ∩ z
14 imaeq2 ⊢ x = y ∩ z → F -1 x = F -1 y ∩ z
15 14 rspceeqv ⊢ y ∩ z ∈ L ∧ F -1 y ∩ F -1 z = F -1 y ∩ z → ∃ x ∈ L F -1 y ∩ F -1 z = F -1 x
16 7 13 15 syl2anc ⊢ φ ∧ y ∈ L ∧ z ∈ L → ∃ x ∈ L F -1 y ∩ F -1 z = F -1 x
17 ineq12 ⊢ s = F -1 y ∧ t = F -1 z → s ∩ t = F -1 y ∩ F -1 z
18 17 eqeq1d ⊢ s = F -1 y ∧ t = F -1 z → s ∩ t = F -1 x ↔ F -1 y ∩ F -1 z = F -1 x
19 18 rexbidv ⊢ s = F -1 y ∧ t = F -1 z → ∃ x ∈ L s ∩ t = F -1 x ↔ ∃ x ∈ L F -1 y ∩ F -1 z = F -1 x
20 16 19 syl5ibrcom ⊢ φ ∧ y ∈ L ∧ z ∈ L → s = F -1 y ∧ t = F -1 z → ∃ x ∈ L s ∩ t = F -1 x
21 20 rexlimdvva ⊢ φ → ∃ y ∈ L ∃ z ∈ L s = F -1 y ∧ t = F -1 z → ∃ x ∈ L s ∩ t = F -1 x
22 imaeq2 ⊢ x = y → F -1 x = F -1 y
23 22 eqeq2d ⊢ x = y → s = F -1 x ↔ s = F -1 y
24 23 cbvrexvw ⊢ ∃ x ∈ L s = F -1 x ↔ ∃ y ∈ L s = F -1 y
25 imaeq2 ⊢ x = z → F -1 x = F -1 z
26 25 eqeq2d ⊢ x = z → t = F -1 x ↔ t = F -1 z
27 26 cbvrexvw ⊢ ∃ x ∈ L t = F -1 x ↔ ∃ z ∈ L t = F -1 z
28 24 27 anbi12i ⊢ ∃ x ∈ L s = F -1 x ∧ ∃ x ∈ L t = F -1 x ↔ ∃ y ∈ L s = F -1 y ∧ ∃ z ∈ L t = F -1 z
29 eqid ⊢ x ∈ L ⟼ F -1 x = x ∈ L ⟼ F -1 x
30 29 elrnmpt ⊢ s ∈ V → s ∈ ran ⁡ x ∈ L ⟼ F -1 x ↔ ∃ x ∈ L s = F -1 x
31 30 elv ⊢ s ∈ ran ⁡ x ∈ L ⟼ F -1 x ↔ ∃ x ∈ L s = F -1 x
32 29 elrnmpt ⊢ t ∈ V → t ∈ ran ⁡ x ∈ L ⟼ F -1 x ↔ ∃ x ∈ L t = F -1 x
33 32 elv ⊢ t ∈ ran ⁡ x ∈ L ⟼ F -1 x ↔ ∃ x ∈ L t = F -1 x
34 31 33 anbi12i ⊢ s ∈ ran ⁡ x ∈ L ⟼ F -1 x ∧ t ∈ ran ⁡ x ∈ L ⟼ F -1 x ↔ ∃ x ∈ L s = F -1 x ∧ ∃ x ∈ L t = F -1 x
35 reeanv ⊢ ∃ y ∈ L ∃ z ∈ L s = F -1 y ∧ t = F -1 z ↔ ∃ y ∈ L s = F -1 y ∧ ∃ z ∈ L t = F -1 z
36 28 34 35 3bitr4i ⊢ s ∈ ran ⁡ x ∈ L ⟼ F -1 x ∧ t ∈ ran ⁡ x ∈ L ⟼ F -1 x ↔ ∃ y ∈ L ∃ z ∈ L s = F -1 y ∧ t = F -1 z
37 vex ⊢ s ∈ V
38 37 inex1 ⊢ s ∩ t ∈ V
39 29 elrnmpt ⊢ s ∩ t ∈ V → s ∩ t ∈ ran ⁡ x ∈ L ⟼ F -1 x ↔ ∃ x ∈ L s ∩ t = F -1 x
40 38 39 ax-mp ⊢ s ∩ t ∈ ran ⁡ x ∈ L ⟼ F -1 x ↔ ∃ x ∈ L s ∩ t = F -1 x
41 21 36 40 3imtr4g ⊢ φ → s ∈ ran ⁡ x ∈ L ⟼ F -1 x ∧ t ∈ ran ⁡ x ∈ L ⟼ F -1 x → s ∩ t ∈ ran ⁡ x ∈ L ⟼ F -1 x
42 41 ralrimivv ⊢ φ → ∀ s ∈ ran ⁡ x ∈ L ⟼ F -1 x ∀ t ∈ ran ⁡ x ∈ L ⟼ F -1 x s ∩ t ∈ ran ⁡ x ∈ L ⟼ F -1 x
43 mptexg ⊢ L ∈ Fil ⁡ X → x ∈ L ⟼ F -1 x ∈ V
44 rnexg ⊢ x ∈ L ⟼ F -1 x ∈ V → ran ⁡ x ∈ L ⟼ F -1 x ∈ V
45 inficl ⊢ ran ⁡ x ∈ L ⟼ F -1 x ∈ V → ∀ s ∈ ran ⁡ x ∈ L ⟼ F -1 x ∀ t ∈ ran ⁡ x ∈ L ⟼ F -1 x s ∩ t ∈ ran ⁡ x ∈ L ⟼ F -1 x ↔ fi ⁡ ran ⁡ x ∈ L ⟼ F -1 x = ran ⁡ x ∈ L ⟼ F -1 x
46 2 43 44 45 4syl ⊢ φ → ∀ s ∈ ran ⁡ x ∈ L ⟼ F -1 x ∀ t ∈ ran ⁡ x ∈ L ⟼ F -1 x s ∩ t ∈ ran ⁡ x ∈ L ⟼ F -1 x ↔ fi ⁡ ran ⁡ x ∈ L ⟼ F -1 x = ran ⁡ x ∈ L ⟼ F -1 x
47 42 46 mpbid ⊢ φ → fi ⁡ ran ⁡ x ∈ L ⟼ F -1 x = ran ⁡ x ∈ L ⟼ F -1 x