Step | Hyp | Ref
| Expression |
1 | | fmfnfm.l |
. . . . . 6
⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋)) |
2 | 1 | ad2antrr 723 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → 𝐿 ∈ (Fil‘𝑋)) |
3 | | simplr 766 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → 𝑥 ∈ 𝐿) |
4 | | fmfnfm.fm |
. . . . . . . 8
⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿) |
5 | | fmfnfm.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝑌⟶𝑋) |
6 | | ffn 6600 |
. . . . . . . . . . 11
⊢ (𝐹:𝑌⟶𝑋 → 𝐹 Fn 𝑌) |
7 | | dffn4 6694 |
. . . . . . . . . . 11
⊢ (𝐹 Fn 𝑌 ↔ 𝐹:𝑌–onto→ran 𝐹) |
8 | 6, 7 | sylib 217 |
. . . . . . . . . 10
⊢ (𝐹:𝑌⟶𝑋 → 𝐹:𝑌–onto→ran 𝐹) |
9 | | foima 6693 |
. . . . . . . . . 10
⊢ (𝐹:𝑌–onto→ran 𝐹 → (𝐹 “ 𝑌) = ran 𝐹) |
10 | 5, 8, 9 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 “ 𝑌) = ran 𝐹) |
11 | | filtop 23006 |
. . . . . . . . . . 11
⊢ (𝐿 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐿) |
12 | 1, 11 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ 𝐿) |
13 | | fmfnfm.b |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌)) |
14 | | fgcl 23029 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (fBas‘𝑌) → (𝑌filGen𝐵) ∈ (Fil‘𝑌)) |
15 | | filtop 23006 |
. . . . . . . . . . 11
⊢ ((𝑌filGen𝐵) ∈ (Fil‘𝑌) → 𝑌 ∈ (𝑌filGen𝐵)) |
16 | 13, 14, 15 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ (𝑌filGen𝐵)) |
17 | | eqid 2738 |
. . . . . . . . . . 11
⊢ (𝑌filGen𝐵) = (𝑌filGen𝐵) |
18 | 17 | imaelfm 23102 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑌 ∈ (𝑌filGen𝐵)) → (𝐹 “ 𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝐵)) |
19 | 12, 13, 5, 16, 18 | syl31anc 1372 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 “ 𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝐵)) |
20 | 10, 19 | eqeltrrd 2840 |
. . . . . . . 8
⊢ (𝜑 → ran 𝐹 ∈ ((𝑋 FilMap 𝐹)‘𝐵)) |
21 | 4, 20 | sseldd 3922 |
. . . . . . 7
⊢ (𝜑 → ran 𝐹 ∈ 𝐿) |
22 | 21 | ad2antrr 723 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → ran 𝐹 ∈ 𝐿) |
23 | | filin 23005 |
. . . . . 6
⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝐿 ∧ ran 𝐹 ∈ 𝐿) → (𝑥 ∩ ran 𝐹) ∈ 𝐿) |
24 | 2, 3, 22, 23 | syl3anc 1370 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝑥 ∩ ran 𝐹) ∈ 𝐿) |
25 | | simprr 770 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → 𝑡 ⊆ 𝑋) |
26 | | elin 3903 |
. . . . . . 7
⊢ (𝑦 ∈ (𝑥 ∩ ran 𝐹) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ran 𝐹)) |
27 | | fvelrnb 6830 |
. . . . . . . . . . . 12
⊢ (𝐹 Fn 𝑌 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦)) |
28 | 5, 6, 27 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦)) |
29 | 28 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ (𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦)) |
30 | 5 | ffund 6604 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → Fun 𝐹) |
31 | 30 | ad2antrr 723 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → Fun 𝐹) |
32 | | simprr 770 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → 𝑧 ∈ 𝑌) |
33 | 5 | fdmd 6611 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom 𝐹 = 𝑌) |
34 | 33 | ad2antrr 723 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → dom 𝐹 = 𝑌) |
35 | 32, 34 | eleqtrrd 2842 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → 𝑧 ∈ dom 𝐹) |
36 | | fvimacnv 6930 |
. . . . . . . . . . . . . . 15
⊢ ((Fun
𝐹 ∧ 𝑧 ∈ dom 𝐹) → ((𝐹‘𝑧) ∈ 𝑥 ↔ 𝑧 ∈ (◡𝐹 “ 𝑥))) |
37 | 31, 35, 36 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → ((𝐹‘𝑧) ∈ 𝑥 ↔ 𝑧 ∈ (◡𝐹 “ 𝑥))) |
38 | | cnvimass 5989 |
. . . . . . . . . . . . . . . 16
⊢ (◡𝐹 “ 𝑥) ⊆ dom 𝐹 |
39 | | funfvima2 7107 |
. . . . . . . . . . . . . . . 16
⊢ ((Fun
𝐹 ∧ (◡𝐹 “ 𝑥) ⊆ dom 𝐹) → (𝑧 ∈ (◡𝐹 “ 𝑥) → (𝐹‘𝑧) ∈ (𝐹 “ (◡𝐹 “ 𝑥)))) |
40 | 31, 38, 39 | sylancl 586 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → (𝑧 ∈ (◡𝐹 “ 𝑥) → (𝐹‘𝑧) ∈ (𝐹 “ (◡𝐹 “ 𝑥)))) |
41 | | ssel 3914 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 → ((𝐹‘𝑧) ∈ (𝐹 “ (◡𝐹 “ 𝑥)) → (𝐹‘𝑧) ∈ 𝑡)) |
42 | 41 | ad2antrl 725 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → ((𝐹‘𝑧) ∈ (𝐹 “ (◡𝐹 “ 𝑥)) → (𝐹‘𝑧) ∈ 𝑡)) |
43 | 40, 42 | syld 47 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → (𝑧 ∈ (◡𝐹 “ 𝑥) → (𝐹‘𝑧) ∈ 𝑡)) |
44 | 37, 43 | sylbid 239 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → ((𝐹‘𝑧) ∈ 𝑥 → (𝐹‘𝑧) ∈ 𝑡)) |
45 | | eleq1 2826 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑧) = 𝑦 → ((𝐹‘𝑧) ∈ 𝑥 ↔ 𝑦 ∈ 𝑥)) |
46 | | eleq1 2826 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑧) = 𝑦 → ((𝐹‘𝑧) ∈ 𝑡 ↔ 𝑦 ∈ 𝑡)) |
47 | 45, 46 | imbi12d 345 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑧) = 𝑦 → (((𝐹‘𝑧) ∈ 𝑥 → (𝐹‘𝑧) ∈ 𝑡) ↔ (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑡))) |
48 | 44, 47 | syl5ibcom 244 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → ((𝐹‘𝑧) = 𝑦 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑡))) |
49 | 48 | expr 457 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ (𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡) → (𝑧 ∈ 𝑌 → ((𝐹‘𝑧) = 𝑦 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑡)))) |
50 | 49 | rexlimdv 3212 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ (𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡) → (∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑡))) |
51 | 29, 50 | sylbid 239 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ (𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡) → (𝑦 ∈ ran 𝐹 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑡))) |
52 | 51 | impcomd 412 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ (𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡) → ((𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ 𝑡)) |
53 | 52 | adantrr 714 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → ((𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ 𝑡)) |
54 | 26, 53 | syl5bi 241 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝑦 ∈ (𝑥 ∩ ran 𝐹) → 𝑦 ∈ 𝑡)) |
55 | 54 | ssrdv 3927 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝑥 ∩ ran 𝐹) ⊆ 𝑡) |
56 | | filss 23004 |
. . . . 5
⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ ((𝑥 ∩ ran 𝐹) ∈ 𝐿 ∧ 𝑡 ⊆ 𝑋 ∧ (𝑥 ∩ ran 𝐹) ⊆ 𝑡)) → 𝑡 ∈ 𝐿) |
57 | 2, 24, 25, 55, 56 | syl13anc 1371 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → 𝑡 ∈ 𝐿) |
58 | 57 | exp32 421 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))) |
59 | | imaeq2 5965 |
. . . . 5
⊢ (𝑠 = (◡𝐹 “ 𝑥) → (𝐹 “ 𝑠) = (𝐹 “ (◡𝐹 “ 𝑥))) |
60 | 59 | sseq1d 3952 |
. . . 4
⊢ (𝑠 = (◡𝐹 “ 𝑥) → ((𝐹 “ 𝑠) ⊆ 𝑡 ↔ (𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡)) |
61 | 60 | imbi1d 342 |
. . 3
⊢ (𝑠 = (◡𝐹 “ 𝑥) → (((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)) ↔ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
62 | 58, 61 | syl5ibrcom 246 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐿) → (𝑠 = (◡𝐹 “ 𝑥) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
63 | 62 | rexlimdva 3213 |
1
⊢ (𝜑 → (∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |