Step | Hyp | Ref
| Expression |
1 | | fmfnfm.l |
. . . . . 6
⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋)) |
2 | 1 | ad2antrr 758 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → 𝐿 ∈ (Fil‘𝑋)) |
3 | | simplr 788 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → 𝑥 ∈ 𝐿) |
4 | | fmfnfm.fm |
. . . . . . . 8
⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿) |
5 | | fmfnfm.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝑌⟶𝑋) |
6 | | ffn 5958 |
. . . . . . . . . . 11
⊢ (𝐹:𝑌⟶𝑋 → 𝐹 Fn 𝑌) |
7 | | dffn4 6034 |
. . . . . . . . . . 11
⊢ (𝐹 Fn 𝑌 ↔ 𝐹:𝑌–onto→ran 𝐹) |
8 | 6, 7 | sylib 207 |
. . . . . . . . . 10
⊢ (𝐹:𝑌⟶𝑋 → 𝐹:𝑌–onto→ran 𝐹) |
9 | | foima 6033 |
. . . . . . . . . 10
⊢ (𝐹:𝑌–onto→ran 𝐹 → (𝐹 “ 𝑌) = ran 𝐹) |
10 | 5, 8, 9 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 “ 𝑌) = ran 𝐹) |
11 | | filtop 21469 |
. . . . . . . . . . 11
⊢ (𝐿 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐿) |
12 | 1, 11 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ 𝐿) |
13 | | fmfnfm.b |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌)) |
14 | | fgcl 21492 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (fBas‘𝑌) → (𝑌filGen𝐵) ∈ (Fil‘𝑌)) |
15 | | filtop 21469 |
. . . . . . . . . . 11
⊢ ((𝑌filGen𝐵) ∈ (Fil‘𝑌) → 𝑌 ∈ (𝑌filGen𝐵)) |
16 | 13, 14, 15 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ (𝑌filGen𝐵)) |
17 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑌filGen𝐵) = (𝑌filGen𝐵) |
18 | 17 | imaelfm 21565 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑌 ∈ (𝑌filGen𝐵)) → (𝐹 “ 𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝐵)) |
19 | 12, 13, 5, 16, 18 | syl31anc 1321 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 “ 𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝐵)) |
20 | 10, 19 | eqeltrrd 2689 |
. . . . . . . 8
⊢ (𝜑 → ran 𝐹 ∈ ((𝑋 FilMap 𝐹)‘𝐵)) |
21 | 4, 20 | sseldd 3569 |
. . . . . . 7
⊢ (𝜑 → ran 𝐹 ∈ 𝐿) |
22 | 21 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → ran 𝐹 ∈ 𝐿) |
23 | | filin 21468 |
. . . . . 6
⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝐿 ∧ ran 𝐹 ∈ 𝐿) → (𝑥 ∩ ran 𝐹) ∈ 𝐿) |
24 | 2, 3, 22, 23 | syl3anc 1318 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝑥 ∩ ran 𝐹) ∈ 𝐿) |
25 | | simprr 792 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → 𝑡 ⊆ 𝑋) |
26 | | elin 3758 |
. . . . . . 7
⊢ (𝑦 ∈ (𝑥 ∩ ran 𝐹) ↔ (𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ran 𝐹)) |
27 | | fvelrnb 6153 |
. . . . . . . . . . . . 13
⊢ (𝐹 Fn 𝑌 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦)) |
28 | 5, 6, 27 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦)) |
29 | 28 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ (𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦)) |
30 | | ffun 5961 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹:𝑌⟶𝑋 → Fun 𝐹) |
31 | 5, 30 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → Fun 𝐹) |
32 | 31 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → Fun 𝐹) |
33 | | simprr 792 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → 𝑧 ∈ 𝑌) |
34 | | fdm 5964 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹:𝑌⟶𝑋 → dom 𝐹 = 𝑌) |
35 | 5, 34 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → dom 𝐹 = 𝑌) |
36 | 35 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → dom 𝐹 = 𝑌) |
37 | 33, 36 | eleqtrrd 2691 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → 𝑧 ∈ dom 𝐹) |
38 | | fvimacnv 6240 |
. . . . . . . . . . . . . . . 16
⊢ ((Fun
𝐹 ∧ 𝑧 ∈ dom 𝐹) → ((𝐹‘𝑧) ∈ 𝑥 ↔ 𝑧 ∈ (◡𝐹 “ 𝑥))) |
39 | 32, 37, 38 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → ((𝐹‘𝑧) ∈ 𝑥 ↔ 𝑧 ∈ (◡𝐹 “ 𝑥))) |
40 | | cnvimass 5404 |
. . . . . . . . . . . . . . . . 17
⊢ (◡𝐹 “ 𝑥) ⊆ dom 𝐹 |
41 | | funfvima2 6397 |
. . . . . . . . . . . . . . . . 17
⊢ ((Fun
𝐹 ∧ (◡𝐹 “ 𝑥) ⊆ dom 𝐹) → (𝑧 ∈ (◡𝐹 “ 𝑥) → (𝐹‘𝑧) ∈ (𝐹 “ (◡𝐹 “ 𝑥)))) |
42 | 32, 40, 41 | sylancl 693 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → (𝑧 ∈ (◡𝐹 “ 𝑥) → (𝐹‘𝑧) ∈ (𝐹 “ (◡𝐹 “ 𝑥)))) |
43 | | ssel 3562 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 → ((𝐹‘𝑧) ∈ (𝐹 “ (◡𝐹 “ 𝑥)) → (𝐹‘𝑧) ∈ 𝑡)) |
44 | 43 | ad2antrl 760 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → ((𝐹‘𝑧) ∈ (𝐹 “ (◡𝐹 “ 𝑥)) → (𝐹‘𝑧) ∈ 𝑡)) |
45 | 42, 44 | syld 46 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → (𝑧 ∈ (◡𝐹 “ 𝑥) → (𝐹‘𝑧) ∈ 𝑡)) |
46 | 39, 45 | sylbid 229 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → ((𝐹‘𝑧) ∈ 𝑥 → (𝐹‘𝑧) ∈ 𝑡)) |
47 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑧) = 𝑦 → ((𝐹‘𝑧) ∈ 𝑥 ↔ 𝑦 ∈ 𝑥)) |
48 | | eleq1 2676 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑧) = 𝑦 → ((𝐹‘𝑧) ∈ 𝑡 ↔ 𝑦 ∈ 𝑡)) |
49 | 47, 48 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑧) = 𝑦 → (((𝐹‘𝑧) ∈ 𝑥 → (𝐹‘𝑧) ∈ 𝑡) ↔ (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑡))) |
50 | 46, 49 | syl5ibcom 234 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑧 ∈ 𝑌)) → ((𝐹‘𝑧) = 𝑦 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑡))) |
51 | 50 | expr 641 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ (𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡) → (𝑧 ∈ 𝑌 → ((𝐹‘𝑧) = 𝑦 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑡)))) |
52 | 51 | rexlimdv 3012 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ (𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡) → (∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = 𝑦 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑡))) |
53 | 29, 52 | sylbid 229 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ (𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡) → (𝑦 ∈ ran 𝐹 → (𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑡))) |
54 | 53 | com23 84 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ (𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡) → (𝑦 ∈ 𝑥 → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ 𝑡))) |
55 | 54 | impd 446 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ (𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡) → ((𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ 𝑡)) |
56 | 55 | adantrr 749 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → ((𝑦 ∈ 𝑥 ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ 𝑡)) |
57 | 26, 56 | syl5bi 231 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝑦 ∈ (𝑥 ∩ ran 𝐹) → 𝑦 ∈ 𝑡)) |
58 | 57 | ssrdv 3574 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → (𝑥 ∩ ran 𝐹) ⊆ 𝑡) |
59 | | filss 21467 |
. . . . 5
⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ ((𝑥 ∩ ran 𝐹) ∈ 𝐿 ∧ 𝑡 ⊆ 𝑋 ∧ (𝑥 ∩ ran 𝐹) ⊆ 𝑡)) → 𝑡 ∈ 𝐿) |
60 | 2, 24, 25, 58, 59 | syl13anc 1320 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐿) ∧ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 ∧ 𝑡 ⊆ 𝑋)) → 𝑡 ∈ 𝐿) |
61 | 60 | exp32 629 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿))) |
62 | | imaeq2 5381 |
. . . . 5
⊢ (𝑠 = (◡𝐹 “ 𝑥) → (𝐹 “ 𝑠) = (𝐹 “ (◡𝐹 “ 𝑥))) |
63 | 62 | sseq1d 3595 |
. . . 4
⊢ (𝑠 = (◡𝐹 “ 𝑥) → ((𝐹 “ 𝑠) ⊆ 𝑡 ↔ (𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡)) |
64 | 63 | imbi1d 330 |
. . 3
⊢ (𝑠 = (◡𝐹 “ 𝑥) → (((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)) ↔ ((𝐹 “ (◡𝐹 “ 𝑥)) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
65 | 61, 64 | syl5ibrcom 236 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐿) → (𝑠 = (◡𝐹 “ 𝑥) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |
66 | 65 | rexlimdva 3013 |
1
⊢ (𝜑 → (∃𝑥 ∈ 𝐿 𝑠 = (◡𝐹 “ 𝑥) → ((𝐹 “ 𝑠) ⊆ 𝑡 → (𝑡 ⊆ 𝑋 → 𝑡 ∈ 𝐿)))) |