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 ⊢ ( 𝜑 → 𝐵 ∈ ( fBas ‘ 𝑌 ) )
fmfnfm.l ⊢ ( 𝜑 → 𝐿 ∈ ( Fil ‘ 𝑋 ) )
fmfnfm.f ⊢ ( 𝜑 → 𝐹 : 𝑌 ⟶ 𝑋 )
fmfnfm.fm ⊢ ( 𝜑 → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ⊆ 𝐿 )
Assertion fmfnfmlem3 ( 𝜑 → ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) = ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 fmfnfm.b ⊢ ( 𝜑 → 𝐵 ∈ ( fBas ‘ 𝑌 ) )
2 fmfnfm.l ⊢ ( 𝜑 → 𝐿 ∈ ( Fil ‘ 𝑋 ) )
3 fmfnfm.f ⊢ ( 𝜑 → 𝐹 : 𝑌 ⟶ 𝑋 )
4 fmfnfm.fm ⊢ ( 𝜑 → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ⊆ 𝐿 )
5 filin ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑦 ∈ 𝐿 ∧ 𝑧 ∈ 𝐿 ) → ( 𝑦 ∩ 𝑧 ) ∈ 𝐿 )
6 5 3expb ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝐿 ∧ 𝑧 ∈ 𝐿 ) ) → ( 𝑦 ∩ 𝑧 ) ∈ 𝐿 )
7 2 6 sylan ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐿 ∧ 𝑧 ∈ 𝐿 ) ) → ( 𝑦 ∩ 𝑧 ) ∈ 𝐿 )
8 ffun ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → Fun 𝐹 )
9 funcnvcnv ⊢ ( Fun 𝐹 → Fun ◡ ◡ 𝐹 )
10 imain ⊢ ( Fun ◡ ◡ 𝐹 → ( ◡ 𝐹 “ ( 𝑦 ∩ 𝑧 ) ) = ( ( ◡ 𝐹 “ 𝑦 ) ∩ ( ◡ 𝐹 “ 𝑧 ) ) )
11 10 eqcomd ⊢ ( Fun ◡ ◡ 𝐹 → ( ( ◡ 𝐹 “ 𝑦 ) ∩ ( ◡ 𝐹 “ 𝑧 ) ) = ( ◡ 𝐹 “ ( 𝑦 ∩ 𝑧 ) ) )
12 3 8 9 11 4syl ⊢ ( 𝜑 → ( ( ◡ 𝐹 “ 𝑦 ) ∩ ( ◡ 𝐹 “ 𝑧 ) ) = ( ◡ 𝐹 “ ( 𝑦 ∩ 𝑧 ) ) )
13 12 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐿 ∧ 𝑧 ∈ 𝐿 ) ) → ( ( ◡ 𝐹 “ 𝑦 ) ∩ ( ◡ 𝐹 “ 𝑧 ) ) = ( ◡ 𝐹 “ ( 𝑦 ∩ 𝑧 ) ) )
14 imaeq2 ⊢ ( 𝑥 = ( 𝑦 ∩ 𝑧 ) → ( ◡ 𝐹 “ 𝑥 ) = ( ◡ 𝐹 “ ( 𝑦 ∩ 𝑧 ) ) )
15 14 rspceeqv ⊢ ( ( ( 𝑦 ∩ 𝑧 ) ∈ 𝐿 ∧ ( ( ◡ 𝐹 “ 𝑦 ) ∩ ( ◡ 𝐹 “ 𝑧 ) ) = ( ◡ 𝐹 “ ( 𝑦 ∩ 𝑧 ) ) ) → ∃ 𝑥 ∈ 𝐿 ( ( ◡ 𝐹 “ 𝑦 ) ∩ ( ◡ 𝐹 “ 𝑧 ) ) = ( ◡ 𝐹 “ 𝑥 ) )
16 7 13 15 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐿 ∧ 𝑧 ∈ 𝐿 ) ) → ∃ 𝑥 ∈ 𝐿 ( ( ◡ 𝐹 “ 𝑦 ) ∩ ( ◡ 𝐹 “ 𝑧 ) ) = ( ◡ 𝐹 “ 𝑥 ) )
17 ineq12 ⊢ ( ( 𝑠 = ( ◡ 𝐹 “ 𝑦 ) ∧ 𝑡 = ( ◡ 𝐹 “ 𝑧 ) ) → ( 𝑠 ∩ 𝑡 ) = ( ( ◡ 𝐹 “ 𝑦 ) ∩ ( ◡ 𝐹 “ 𝑧 ) ) )
18 17 eqeq1d ⊢ ( ( 𝑠 = ( ◡ 𝐹 “ 𝑦 ) ∧ 𝑡 = ( ◡ 𝐹 “ 𝑧 ) ) → ( ( 𝑠 ∩ 𝑡 ) = ( ◡ 𝐹 “ 𝑥 ) ↔ ( ( ◡ 𝐹 “ 𝑦 ) ∩ ( ◡ 𝐹 “ 𝑧 ) ) = ( ◡ 𝐹 “ 𝑥 ) ) )
19 18 rexbidv ⊢ ( ( 𝑠 = ( ◡ 𝐹 “ 𝑦 ) ∧ 𝑡 = ( ◡ 𝐹 “ 𝑧 ) ) → ( ∃ 𝑥 ∈ 𝐿 ( 𝑠 ∩ 𝑡 ) = ( ◡ 𝐹 “ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐿 ( ( ◡ 𝐹 “ 𝑦 ) ∩ ( ◡ 𝐹 “ 𝑧 ) ) = ( ◡ 𝐹 “ 𝑥 ) ) )
20 16 19 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐿 ∧ 𝑧 ∈ 𝐿 ) ) → ( ( 𝑠 = ( ◡ 𝐹 “ 𝑦 ) ∧ 𝑡 = ( ◡ 𝐹 “ 𝑧 ) ) → ∃ 𝑥 ∈ 𝐿 ( 𝑠 ∩ 𝑡 ) = ( ◡ 𝐹 “ 𝑥 ) ) )
21 20 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝐿 ∃ 𝑧 ∈ 𝐿 ( 𝑠 = ( ◡ 𝐹 “ 𝑦 ) ∧ 𝑡 = ( ◡ 𝐹 “ 𝑧 ) ) → ∃ 𝑥 ∈ 𝐿 ( 𝑠 ∩ 𝑡 ) = ( ◡ 𝐹 “ 𝑥 ) ) )
22 imaeq2 ⊢ ( 𝑥 = 𝑦 → ( ◡ 𝐹 “ 𝑥 ) = ( ◡ 𝐹 “ 𝑦 ) )
23 22 eqeq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑠 = ( ◡ 𝐹 “ 𝑥 ) ↔ 𝑠 = ( ◡ 𝐹 “ 𝑦 ) ) )
24 23 cbvrexvw ⊢ ( ∃ 𝑥 ∈ 𝐿 𝑠 = ( ◡ 𝐹 “ 𝑥 ) ↔ ∃ 𝑦 ∈ 𝐿 𝑠 = ( ◡ 𝐹 “ 𝑦 ) )
25 imaeq2 ⊢ ( 𝑥 = 𝑧 → ( ◡ 𝐹 “ 𝑥 ) = ( ◡ 𝐹 “ 𝑧 ) )
26 25 eqeq2d ⊢ ( 𝑥 = 𝑧 → ( 𝑡 = ( ◡ 𝐹 “ 𝑥 ) ↔ 𝑡 = ( ◡ 𝐹 “ 𝑧 ) ) )
27 26 cbvrexvw ⊢ ( ∃ 𝑥 ∈ 𝐿 𝑡 = ( ◡ 𝐹 “ 𝑥 ) ↔ ∃ 𝑧 ∈ 𝐿 𝑡 = ( ◡ 𝐹 “ 𝑧 ) )
28 24 27 anbi12i ⊢ ( ( ∃ 𝑥 ∈ 𝐿 𝑠 = ( ◡ 𝐹 “ 𝑥 ) ∧ ∃ 𝑥 ∈ 𝐿 𝑡 = ( ◡ 𝐹 “ 𝑥 ) ) ↔ ( ∃ 𝑦 ∈ 𝐿 𝑠 = ( ◡ 𝐹 “ 𝑦 ) ∧ ∃ 𝑧 ∈ 𝐿 𝑡 = ( ◡ 𝐹 “ 𝑧 ) ) )
29 eqid ⊢ ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) = ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) )
30 29 elrnmpt ⊢ ( 𝑠 ∈ V → ( 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 𝑠 = ( ◡ 𝐹 “ 𝑥 ) ) )
31 30 elv ⊢ ( 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 𝑠 = ( ◡ 𝐹 “ 𝑥 ) )
32 29 elrnmpt ⊢ ( 𝑡 ∈ V → ( 𝑡 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 𝑡 = ( ◡ 𝐹 “ 𝑥 ) ) )
33 32 elv ⊢ ( 𝑡 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 𝑡 = ( ◡ 𝐹 “ 𝑥 ) )
34 31 33 anbi12i ⊢ ( ( 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∧ 𝑡 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ↔ ( ∃ 𝑥 ∈ 𝐿 𝑠 = ( ◡ 𝐹 “ 𝑥 ) ∧ ∃ 𝑥 ∈ 𝐿 𝑡 = ( ◡ 𝐹 “ 𝑥 ) ) )
35 reeanv ⊢ ( ∃ 𝑦 ∈ 𝐿 ∃ 𝑧 ∈ 𝐿 ( 𝑠 = ( ◡ 𝐹 “ 𝑦 ) ∧ 𝑡 = ( ◡ 𝐹 “ 𝑧 ) ) ↔ ( ∃ 𝑦 ∈ 𝐿 𝑠 = ( ◡ 𝐹 “ 𝑦 ) ∧ ∃ 𝑧 ∈ 𝐿 𝑡 = ( ◡ 𝐹 “ 𝑧 ) ) )
36 28 34 35 3bitr4i ⊢ ( ( 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∧ 𝑡 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) ↔ ∃ 𝑦 ∈ 𝐿 ∃ 𝑧 ∈ 𝐿 ( 𝑠 = ( ◡ 𝐹 “ 𝑦 ) ∧ 𝑡 = ( ◡ 𝐹 “ 𝑧 ) ) )
37 vex ⊢ 𝑠 ∈ V
38 37 inex1 ⊢ ( 𝑠 ∩ 𝑡 ) ∈ V
39 29 elrnmpt ⊢ ( ( 𝑠 ∩ 𝑡 ) ∈ V → ( ( 𝑠 ∩ 𝑡 ) ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 ( 𝑠 ∩ 𝑡 ) = ( ◡ 𝐹 “ 𝑥 ) ) )
40 38 39 ax-mp ⊢ ( ( 𝑠 ∩ 𝑡 ) ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐿 ( 𝑠 ∩ 𝑡 ) = ( ◡ 𝐹 “ 𝑥 ) )
41 21 36 40 3imtr4g ⊢ ( 𝜑 → ( ( 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∧ 𝑡 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) → ( 𝑠 ∩ 𝑡 ) ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) )
42 41 ralrimivv ⊢ ( 𝜑 → ∀ 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∀ 𝑡 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ( 𝑠 ∩ 𝑡 ) ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) )
43 mptexg ⊢ ( 𝐿 ∈ ( Fil ‘ 𝑋 ) → ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ V )
44 rnexg ⊢ ( ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ V → ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ V )
45 inficl ⊢ ( ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∈ V → ( ∀ 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∀ 𝑡 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ( 𝑠 ∩ 𝑡 ) ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) = ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) )
46 2 43 44 45 4syl ⊢ ( 𝜑 → ( ∀ 𝑠 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ∀ 𝑡 ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ( 𝑠 ∩ 𝑡 ) ∈ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ↔ ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) = ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) )
47 42 46 mpbid ⊢ ( 𝜑 → ( fi ‘ ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) ) = ran ( 𝑥 ∈ 𝐿 ↦ ( ◡ 𝐹 “ 𝑥 ) ) )