Step | Hyp | Ref
| Expression |
1 | | fmfnfm.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌)) |
2 | | fbsspw 21446 |
. . . . . 6
⊢ (𝐵 ∈ (fBas‘𝑌) → 𝐵 ⊆ 𝒫 𝑌) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐵 ⊆ 𝒫 𝑌) |
4 | | elfvdm 6130 |
. . . . . . . 8
⊢ (𝐵 ∈ (fBas‘𝑌) → 𝑌 ∈ dom fBas) |
5 | 1, 4 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ dom fBas) |
6 | | fmfnfm.l |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ (Fil‘𝑋)) |
7 | | fmfnfm.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝑌⟶𝑋) |
8 | | fmfnfm.fm |
. . . . . . . 8
⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿) |
9 | | ffn 5958 |
. . . . . . . . . . 11
⊢ (𝐹:𝑌⟶𝑋 → 𝐹 Fn 𝑌) |
10 | | dffn4 6034 |
. . . . . . . . . . 11
⊢ (𝐹 Fn 𝑌 ↔ 𝐹:𝑌–onto→ran 𝐹) |
11 | 9, 10 | sylib 207 |
. . . . . . . . . 10
⊢ (𝐹:𝑌⟶𝑋 → 𝐹:𝑌–onto→ran 𝐹) |
12 | | foima 6033 |
. . . . . . . . . 10
⊢ (𝐹:𝑌–onto→ran 𝐹 → (𝐹 “ 𝑌) = ran 𝐹) |
13 | 7, 11, 12 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 “ 𝑌) = ran 𝐹) |
14 | | filtop 21469 |
. . . . . . . . . . 11
⊢ (𝐿 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐿) |
15 | 6, 14 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ 𝐿) |
16 | | fgcl 21492 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (fBas‘𝑌) → (𝑌filGen𝐵) ∈ (Fil‘𝑌)) |
17 | | filtop 21469 |
. . . . . . . . . . 11
⊢ ((𝑌filGen𝐵) ∈ (Fil‘𝑌) → 𝑌 ∈ (𝑌filGen𝐵)) |
18 | 1, 16, 17 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ (𝑌filGen𝐵)) |
19 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑌filGen𝐵) = (𝑌filGen𝐵) |
20 | 19 | imaelfm 21565 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑌 ∈ (𝑌filGen𝐵)) → (𝐹 “ 𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝐵)) |
21 | 15, 1, 7, 18, 20 | syl31anc 1321 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 “ 𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝐵)) |
22 | 13, 21 | eqeltrrd 2689 |
. . . . . . . 8
⊢ (𝜑 → ran 𝐹 ∈ ((𝑋 FilMap 𝐹)‘𝐵)) |
23 | 8, 22 | sseldd 3569 |
. . . . . . 7
⊢ (𝜑 → ran 𝐹 ∈ 𝐿) |
24 | | rnelfmlem 21566 |
. . . . . . 7
⊢ (((𝑌 ∈ dom fBas ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌)) |
25 | 5, 6, 7, 23, 24 | syl31anc 1321 |
. . . . . 6
⊢ (𝜑 → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌)) |
26 | | fbsspw 21446 |
. . . . . 6
⊢ (ran
(𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌) → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ⊆ 𝒫 𝑌) |
27 | 25, 26 | syl 17 |
. . . . 5
⊢ (𝜑 → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ⊆ 𝒫 𝑌) |
28 | 3, 27 | unssd 3751 |
. . . 4
⊢ (𝜑 → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ⊆ 𝒫 𝑌) |
29 | | ssun1 3738 |
. . . . 5
⊢ 𝐵 ⊆ (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) |
30 | | fbasne0 21444 |
. . . . . 6
⊢ (𝐵 ∈ (fBas‘𝑌) → 𝐵 ≠ ∅) |
31 | 1, 30 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐵 ≠ ∅) |
32 | | ssn0 3928 |
. . . . 5
⊢ ((𝐵 ⊆ (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∧ 𝐵 ≠ ∅) → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ≠ ∅) |
33 | 29, 31, 32 | sylancr 694 |
. . . 4
⊢ (𝜑 → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ≠ ∅) |
34 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑡 ∈ V |
35 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) = (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) |
36 | 35 | elrnmpt 5293 |
. . . . . . . . 9
⊢ (𝑡 ∈ V → (𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑡 = (◡𝐹 “ 𝑥))) |
37 | 34, 36 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑡 = (◡𝐹 “ 𝑥)) |
38 | | 0nelfil 21463 |
. . . . . . . . . . . . . 14
⊢ (𝐿 ∈ (Fil‘𝑋) → ¬ ∅ ∈
𝐿) |
39 | 6, 38 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ¬ ∅ ∈ 𝐿) |
40 | 39 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → ¬ ∅ ∈ 𝐿) |
41 | 6 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝐿 ∈ (Fil‘𝑋)) |
42 | 8 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿) |
43 | 15, 1, 7 | 3jca 1235 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋)) |
44 | 43 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋)) |
45 | | ssfg 21486 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈ (fBas‘𝑌) → 𝐵 ⊆ (𝑌filGen𝐵)) |
46 | 1, 45 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐵 ⊆ (𝑌filGen𝐵)) |
47 | 46 | sselda 3568 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ∈ (𝑌filGen𝐵)) |
48 | 19 | imaelfm 21565 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑠 ∈ (𝑌filGen𝐵)) → (𝐹 “ 𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵)) |
49 | 44, 47, 48 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝐹 “ 𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵)) |
50 | 42, 49 | sseldd 3569 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝐹 “ 𝑠) ∈ 𝐿) |
51 | 41, 50 | jca 553 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝐿 ∈ (Fil‘𝑋) ∧ (𝐹 “ 𝑠) ∈ 𝐿)) |
52 | | filin 21468 |
. . . . . . . . . . . . . . 15
⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹 “ 𝑠) ∈ 𝐿 ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿) |
53 | 52 | 3expa 1257 |
. . . . . . . . . . . . . 14
⊢ (((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹 “ 𝑠) ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿) |
54 | 51, 53 | sylan 487 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿) |
55 | | eleq1 2676 |
. . . . . . . . . . . . 13
⊢ (((𝐹 “ 𝑠) ∩ 𝑥) = ∅ → (((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿 ↔ ∅ ∈ 𝐿)) |
56 | 54, 55 | syl5ibcom 234 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (((𝐹 “ 𝑠) ∩ 𝑥) = ∅ → ∅ ∈ 𝐿)) |
57 | 40, 56 | mtod 188 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → ¬ ((𝐹 “ 𝑠) ∩ 𝑥) = ∅) |
58 | | neq0 3889 |
. . . . . . . . . . . 12
⊢ (¬
((𝐹 “ 𝑠) ∩ 𝑥) = ∅ ↔ ∃𝑡 𝑡 ∈ ((𝐹 “ 𝑠) ∩ 𝑥)) |
59 | | elin 3758 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ ((𝐹 “ 𝑠) ∩ 𝑥) ↔ (𝑡 ∈ (𝐹 “ 𝑠) ∧ 𝑡 ∈ 𝑥)) |
60 | | ffun 5961 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹:𝑌⟶𝑋 → Fun 𝐹) |
61 | | fvelima 6158 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Fun
𝐹 ∧ 𝑡 ∈ (𝐹 “ 𝑠)) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑡) |
62 | 61 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢ (Fun
𝐹 → (𝑡 ∈ (𝐹 “ 𝑠) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑡)) |
63 | 7, 60, 62 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑡 ∈ (𝐹 “ 𝑠) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑡)) |
64 | 63 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (𝑡 ∈ (𝐹 “ 𝑠) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑡)) |
65 | 7, 60 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → Fun 𝐹) |
66 | 65 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) ∧ 𝑦 ∈ 𝑠) → Fun 𝐹) |
67 | | fbelss 21447 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ 𝑠 ∈ 𝐵) → 𝑠 ⊆ 𝑌) |
68 | 1, 67 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ⊆ 𝑌) |
69 | | fdm 5964 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐹:𝑌⟶𝑋 → dom 𝐹 = 𝑌) |
70 | 7, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → dom 𝐹 = 𝑌) |
71 | 70 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → dom 𝐹 = 𝑌) |
72 | 68, 71 | sseqtr4d 3605 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ⊆ dom 𝐹) |
73 | 72 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → 𝑠 ⊆ dom 𝐹) |
74 | 73 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) ∧ 𝑦 ∈ 𝑠) → 𝑦 ∈ dom 𝐹) |
75 | | fvimacnv 6240 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑦 ∈ (◡𝐹 “ 𝑥))) |
76 | 66, 74, 75 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑦 ∈ (◡𝐹 “ 𝑥))) |
77 | | inelcm 3984 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ 𝑠 ∧ 𝑦 ∈ (◡𝐹 “ 𝑥)) → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅) |
78 | 77 | ex 449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ 𝑠 → (𝑦 ∈ (◡𝐹 “ 𝑥) → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅)) |
79 | 78 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) ∧ 𝑦 ∈ 𝑠) → (𝑦 ∈ (◡𝐹 “ 𝑥) → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅)) |
80 | 76, 79 | sylbid 229 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) ∈ 𝑥 → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅)) |
81 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑦) = 𝑡 → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑡 ∈ 𝑥)) |
82 | 81 | imbi1d 330 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑦) = 𝑡 → (((𝐹‘𝑦) ∈ 𝑥 → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅) ↔ (𝑡 ∈ 𝑥 → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅))) |
83 | 80, 82 | syl5ibcom 234 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) = 𝑡 → (𝑡 ∈ 𝑥 → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅))) |
84 | 83 | rexlimdva 3013 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑡 → (𝑡 ∈ 𝑥 → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅))) |
85 | 64, 84 | syld 46 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (𝑡 ∈ (𝐹 “ 𝑠) → (𝑡 ∈ 𝑥 → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅))) |
86 | 85 | impd 446 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → ((𝑡 ∈ (𝐹 “ 𝑠) ∧ 𝑡 ∈ 𝑥) → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅)) |
87 | 59, 86 | syl5bi 231 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (𝑡 ∈ ((𝐹 “ 𝑠) ∩ 𝑥) → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅)) |
88 | 87 | exlimdv 1848 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (∃𝑡 𝑡 ∈ ((𝐹 “ 𝑠) ∩ 𝑥) → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅)) |
89 | 58, 88 | syl5bi 231 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (¬ ((𝐹 “ 𝑠) ∩ 𝑥) = ∅ → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅)) |
90 | 57, 89 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅) |
91 | | ineq2 3770 |
. . . . . . . . . . 11
⊢ (𝑡 = (◡𝐹 “ 𝑥) → (𝑠 ∩ 𝑡) = (𝑠 ∩ (◡𝐹 “ 𝑥))) |
92 | 91 | neeq1d 2841 |
. . . . . . . . . 10
⊢ (𝑡 = (◡𝐹 “ 𝑥) → ((𝑠 ∩ 𝑡) ≠ ∅ ↔ (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅)) |
93 | 90, 92 | syl5ibrcom 236 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (𝑡 = (◡𝐹 “ 𝑥) → (𝑠 ∩ 𝑡) ≠ ∅)) |
94 | 93 | rexlimdva 3013 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (∃𝑥 ∈ 𝐿 𝑡 = (◡𝐹 “ 𝑥) → (𝑠 ∩ 𝑡) ≠ ∅)) |
95 | 37, 94 | syl5bi 231 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅)) |
96 | 95 | expimpd 627 |
. . . . . 6
⊢ (𝜑 → ((𝑠 ∈ 𝐵 ∧ 𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) → (𝑠 ∩ 𝑡) ≠ ∅)) |
97 | 96 | ralrimivv 2953 |
. . . . 5
⊢ (𝜑 → ∀𝑠 ∈ 𝐵 ∀𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))(𝑠 ∩ 𝑡) ≠ ∅) |
98 | | fbunfip 21483 |
. . . . . 6
⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌)) → (¬ ∅ ∈
(fi‘(𝐵 ∪ ran
(𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ↔ ∀𝑠 ∈ 𝐵 ∀𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))(𝑠 ∩ 𝑡) ≠ ∅)) |
99 | 1, 25, 98 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (¬ ∅ ∈
(fi‘(𝐵 ∪ ran
(𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ↔ ∀𝑠 ∈ 𝐵 ∀𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))(𝑠 ∩ 𝑡) ≠ ∅)) |
100 | 97, 99 | mpbird 246 |
. . . 4
⊢ (𝜑 → ¬ ∅ ∈
(fi‘(𝐵 ∪ ran
(𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) |
101 | | fsubbas 21481 |
. . . . 5
⊢ (𝑌 ∈ dom fBas →
((fi‘(𝐵 ∪ ran
(𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌) ↔ ((𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ⊆ 𝒫 𝑌 ∧ (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ≠ ∅ ∧ ¬ ∅ ∈
(fi‘(𝐵 ∪ ran
(𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))))) |
102 | 1, 4, 101 | 3syl 18 |
. . . 4
⊢ (𝜑 → ((fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌) ↔ ((𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ⊆ 𝒫 𝑌 ∧ (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ≠ ∅ ∧ ¬ ∅ ∈
(fi‘(𝐵 ∪ ran
(𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))))) |
103 | 28, 33, 100, 102 | mpbir3and 1238 |
. . 3
⊢ (𝜑 → (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌)) |
104 | | fgcl 21492 |
. . 3
⊢
((fi‘(𝐵 ∪
ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌) → (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) ∈ (Fil‘𝑌)) |
105 | 103, 104 | syl 17 |
. 2
⊢ (𝜑 → (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) ∈ (Fil‘𝑌)) |
106 | | unexg 6857 |
. . . . . 6
⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌)) → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∈ V) |
107 | 1, 25, 106 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∈ V) |
108 | | ssfii 8208 |
. . . . 5
⊢ ((𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∈ V → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) |
109 | 107, 108 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) |
110 | 109 | unssad 3752 |
. . 3
⊢ (𝜑 → 𝐵 ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) |
111 | | ssfg 21486 |
. . . 4
⊢
((fi‘(𝐵 ∪
ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌) → (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))))) |
112 | 103, 111 | syl 17 |
. . 3
⊢ (𝜑 → (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))))) |
113 | 110, 112 | sstrd 3578 |
. 2
⊢ (𝜑 → 𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))))) |
114 | 1, 6, 7, 8 | fmfnfmlem4 21571 |
. . . . 5
⊢ (𝜑 → (𝑡 ∈ 𝐿 ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡))) |
115 | | elfm 21561 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐿 ∧ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝑡 ∈ ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡))) |
116 | 15, 103, 7, 115 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → (𝑡 ∈ ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡))) |
117 | 114, 116 | bitr4d 270 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ 𝐿 ↔ 𝑡 ∈ ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))))) |
118 | 117 | eqrdv 2608 |
. . 3
⊢ (𝜑 → 𝐿 = ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))))) |
119 | | eqid 2610 |
. . . . 5
⊢ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) |
120 | 119 | fmfg 21563 |
. . . 4
⊢ ((𝑋 ∈ 𝐿 ∧ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))))) |
121 | 15, 103, 7, 120 | syl3anc 1318 |
. . 3
⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))))) |
122 | 118, 121 | eqtrd 2644 |
. 2
⊢ (𝜑 → 𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))))) |
123 | | sseq2 3590 |
. . . 4
⊢ (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) → (𝐵 ⊆ 𝑓 ↔ 𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))))) |
124 | | fveq2 6103 |
. . . . 5
⊢ (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) → ((𝑋 FilMap 𝐹)‘𝑓) = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))))) |
125 | 124 | eqeq2d 2620 |
. . . 4
⊢ (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) → (𝐿 = ((𝑋 FilMap 𝐹)‘𝑓) ↔ 𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))))))) |
126 | 123, 125 | anbi12d 743 |
. . 3
⊢ (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) → ((𝐵 ⊆ 𝑓 ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘𝑓)) ↔ (𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))))))) |
127 | 126 | rspcev 3282 |
. 2
⊢ (((𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) ∈ (Fil‘𝑌) ∧ (𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))))))) → ∃𝑓 ∈ (Fil‘𝑌)(𝐵 ⊆ 𝑓 ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘𝑓))) |
128 | 105, 113,
122, 127 | syl12anc 1316 |
1
⊢ (𝜑 → ∃𝑓 ∈ (Fil‘𝑌)(𝐵 ⊆ 𝑓 ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘𝑓))) |