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