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