Metamath Proof Explorer

Theorem fmfnfmlem2

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 fmfnfmlem2 ( 𝜑 → ( ∃ 𝑥 ∈ 𝐿 𝑠 = ( ◡ 𝐹 “ 𝑥 ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) )

Proof

Step Hyp Ref Expression
1 fmfnfm.b ⊢ ( 𝜑 → 𝐵 ∈ ( fBas ‘ 𝑌 ) )
2 fmfnfm.l ⊢ ( 𝜑 → 𝐿 ∈ ( Fil ‘ 𝑋 ) )
3 fmfnfm.f ⊢ ( 𝜑 → 𝐹 : 𝑌 ⟶ 𝑋 )
4 fmfnfm.fm ⊢ ( 𝜑 → ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) ⊆ 𝐿 )
5 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → 𝐿 ∈ ( Fil ‘ 𝑋 ) )
6 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → 𝑥 ∈ 𝐿 )
7 ffn ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → 𝐹 Fn 𝑌 )
8 dffn4 ⊢ ( 𝐹 Fn 𝑌 ↔ 𝐹 : 𝑌 –onto→ ran 𝐹 )
9 7 8 sylib ⊢ ( 𝐹 : 𝑌 ⟶ 𝑋 → 𝐹 : 𝑌 –onto→ ran 𝐹 )
10 foima ⊢ ( 𝐹 : 𝑌 –onto→ ran 𝐹 → ( 𝐹 “ 𝑌 ) = ran 𝐹 )
11 3 9 10 3syl ⊢ ( 𝜑 → ( 𝐹 “ 𝑌 ) = ran 𝐹 )
12 filtop ⊢ ( 𝐿 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐿 )
13 2 12 syl ⊢ ( 𝜑 → 𝑋 ∈ 𝐿 )
14 fgcl ⊢ ( 𝐵 ∈ ( fBas ‘ 𝑌 ) → ( 𝑌 filGen 𝐵 ) ∈ ( Fil ‘ 𝑌 ) )
15 filtop ⊢ ( ( 𝑌 filGen 𝐵 ) ∈ ( Fil ‘ 𝑌 ) → 𝑌 ∈ ( 𝑌 filGen 𝐵 ) )
16 1 14 15 3syl ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑌 filGen 𝐵 ) )
17 eqid ⊢ ( 𝑌 filGen 𝐵 ) = ( 𝑌 filGen 𝐵 )
18 17 imaelfm ⊢ ( ( ( 𝑋 ∈ 𝐿 ∧ 𝐵 ∈ ( fBas ‘ 𝑌 ) ∧ 𝐹 : 𝑌 ⟶ 𝑋 ) ∧ 𝑌 ∈ ( 𝑌 filGen 𝐵 ) ) → ( 𝐹 “ 𝑌 ) ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) )
19 13 1 3 16 18 syl31anc ⊢ ( 𝜑 → ( 𝐹 “ 𝑌 ) ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) )
20 11 19 eqeltrrd ⊢ ( 𝜑 → ran 𝐹 ∈ ( ( 𝑋 FilMap 𝐹 ) ‘ 𝐵 ) )
21 4 20 sseldd ⊢ ( 𝜑 → ran 𝐹 ∈ 𝐿 )
22 21 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ran 𝐹 ∈ 𝐿 )
23 filin ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐿 ∧ ran 𝐹 ∈ 𝐿 ) → ( 𝑥 ∩ ran 𝐹 ) ∈ 𝐿 )
24 5 6 22 23 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ( 𝑥 ∩ ran 𝐹 ) ∈ 𝐿 )
25 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → 𝑡 ⊆ 𝑋 )
26 elin ⊢ ( 𝑦 ∈ ( 𝑥 ∩ ran 𝐹 ) ↔ ( 𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ran 𝐹 ) )
27 fvelrnb ⊢ ( 𝐹 Fn 𝑌 → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑧 ∈ 𝑌 ( 𝐹 ‘ 𝑧 ) = 𝑦 ) )
28 3 7 27 3syl ⊢ ( 𝜑 → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑧 ∈ 𝑌 ( 𝐹 ‘ 𝑧 ) = 𝑦 ) )
29 28 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐿 ) ∧ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ) → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑧 ∈ 𝑌 ( 𝐹 ‘ 𝑧 ) = 𝑦 ) )
30 3 ffund ⊢ ( 𝜑 → Fun 𝐹 )
31 30 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌 ) ) → Fun 𝐹 )
32 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌 ) ) → 𝑧 ∈ 𝑌 )
33 3 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝑌 )
34 33 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌 ) ) → dom 𝐹 = 𝑌 )
35 32 34 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌 ) ) → 𝑧 ∈ dom 𝐹 )
36 fvimacnv ⊢ ( ( Fun 𝐹 ∧ 𝑧 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑥 ↔ 𝑧 ∈ ( ◡ 𝐹 “ 𝑥 ) ) )
37 31 35 36 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌 ) ) → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑥 ↔ 𝑧 ∈ ( ◡ 𝐹 “ 𝑥 ) ) )
38 cnvimass ⊢ ( ◡ 𝐹 “ 𝑥 ) ⊆ dom 𝐹
39 funfvima2 ⊢ ( ( Fun 𝐹 ∧ ( ◡ 𝐹 “ 𝑥 ) ⊆ dom 𝐹 ) → ( 𝑧 ∈ ( ◡ 𝐹 “ 𝑥 ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ) )
40 31 38 39 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌 ) ) → ( 𝑧 ∈ ( ◡ 𝐹 “ 𝑥 ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ) )
41 ssel ⊢ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 → ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ) )
42 41 ad2antrl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌 ) ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ) )
43 40 42 syld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌 ) ) → ( 𝑧 ∈ ( ◡ 𝐹 “ 𝑥 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ) )
44 37 43 sylbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌 ) ) → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑥 → ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ) )
45 eleq1 ⊢ ( ( 𝐹 ‘ 𝑧 ) = 𝑦 → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑥 ↔ 𝑦 ∈ 𝑥 ) )
46 eleq1 ⊢ ( ( 𝐹 ‘ 𝑧 ) = 𝑦 → ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ↔ 𝑦 ∈ 𝑡 ) )
47 45 46 imbi12d ⊢ ( ( 𝐹 ‘ 𝑧 ) = 𝑦 → ( ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑥 → ( 𝐹 ‘ 𝑧 ) ∈ 𝑡 ) ↔ ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑡 ) ) )
48 44 47 syl5ibcom ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌 ) ) → ( ( 𝐹 ‘ 𝑧 ) = 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑡 ) ) )
49 48 expr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐿 ) ∧ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ) → ( 𝑧 ∈ 𝑌 → ( ( 𝐹 ‘ 𝑧 ) = 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑡 ) ) ) )
50 49 rexlimdv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐿 ) ∧ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ) → ( ∃ 𝑧 ∈ 𝑌 ( 𝐹 ‘ 𝑧 ) = 𝑦 → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑡 ) ) )
51 29 50 sylbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐿 ) ∧ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ) → ( 𝑦 ∈ ran 𝐹 → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑡 ) ) )
52 51 impcomd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐿 ) ∧ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ) → ( ( 𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ran 𝐹 ) → 𝑦 ∈ 𝑡 ) )
53 52 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ( ( 𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ran 𝐹 ) → 𝑦 ∈ 𝑡 ) )
54 26 53 syl5bi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ( 𝑦 ∈ ( 𝑥 ∩ ran 𝐹 ) → 𝑦 ∈ 𝑡 ) )
55 54 ssrdv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → ( 𝑥 ∩ ran 𝐹 ) ⊆ 𝑡 )
56 filss ⊢ ( ( 𝐿 ∈ ( Fil ‘ 𝑋 ) ∧ ( ( 𝑥 ∩ ran 𝐹 ) ∈ 𝐿 ∧ 𝑡 ⊆ 𝑋 ∧ ( 𝑥 ∩ ran 𝐹 ) ⊆ 𝑡 ) ) → 𝑡 ∈ 𝐿 )
57 5 24 25 55 56 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐿 ) ∧ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋 ) ) → 𝑡 ∈ 𝐿 )
58 57 exp32 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐿 ) → ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) )
59 imaeq2 ⊢ ( 𝑠 = ( ◡ 𝐹 “ 𝑥 ) → ( 𝐹 “ 𝑠 ) = ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) )
60 59 sseq1d ⊢ ( 𝑠 = ( ◡ 𝐹 “ 𝑥 ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 ↔ ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 ) )
61 60 imbi1d ⊢ ( 𝑠 = ( ◡ 𝐹 “ 𝑥 ) → ( ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ↔ ( ( 𝐹 “ ( ◡ 𝐹 “ 𝑥 ) ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) )
62 58 61 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐿 ) → ( 𝑠 = ( ◡ 𝐹 “ 𝑥 ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) )
63 62 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐿 𝑠 = ( ◡ 𝐹 “ 𝑥 ) → ( ( 𝐹 “ 𝑠 ) ⊆ 𝑡 → ( 𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿 ) ) ) )