| Step | Hyp | Ref
| Expression |
| 1 | | fmfnfm.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌)) |
| 2 | | fbsspw 23840 |
. . . . . 6
⊢ (𝐵 ∈ (fBas‘𝑌) → 𝐵 ⊆ 𝒫 𝑌) |
| 3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐵 ⊆ 𝒫 𝑌) |
| 4 | | elfvdm 6943 |
. . . . . . . 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 6736 |
. . . . . . . . . . 11
⊢ (𝐹:𝑌⟶𝑋 → 𝐹 Fn 𝑌) |
| 10 | | dffn4 6826 |
. . . . . . . . . . 11
⊢ (𝐹 Fn 𝑌 ↔ 𝐹:𝑌–onto→ran 𝐹) |
| 11 | 9, 10 | sylib 218 |
. . . . . . . . . 10
⊢ (𝐹:𝑌⟶𝑋 → 𝐹:𝑌–onto→ran 𝐹) |
| 12 | | foima 6825 |
. . . . . . . . . 10
⊢ (𝐹:𝑌–onto→ran 𝐹 → (𝐹 “ 𝑌) = ran 𝐹) |
| 13 | 7, 11, 12 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 “ 𝑌) = ran 𝐹) |
| 14 | | filtop 23863 |
. . . . . . . . . . 11
⊢ (𝐿 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐿) |
| 15 | 6, 14 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ 𝐿) |
| 16 | | fgcl 23886 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (fBas‘𝑌) → (𝑌filGen𝐵) ∈ (Fil‘𝑌)) |
| 17 | | filtop 23863 |
. . . . . . . . . . 11
⊢ ((𝑌filGen𝐵) ∈ (Fil‘𝑌) → 𝑌 ∈ (𝑌filGen𝐵)) |
| 18 | 1, 16, 17 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ (𝑌filGen𝐵)) |
| 19 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑌filGen𝐵) = (𝑌filGen𝐵) |
| 20 | 19 | imaelfm 23959 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑌 ∈ (𝑌filGen𝐵)) → (𝐹 “ 𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝐵)) |
| 21 | 15, 1, 7, 18, 20 | syl31anc 1375 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹 “ 𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝐵)) |
| 22 | 13, 21 | eqeltrrd 2842 |
. . . . . . . 8
⊢ (𝜑 → ran 𝐹 ∈ ((𝑋 FilMap 𝐹)‘𝐵)) |
| 23 | 8, 22 | sseldd 3984 |
. . . . . . 7
⊢ (𝜑 → ran 𝐹 ∈ 𝐿) |
| 24 | | rnelfmlem 23960 |
. . . . . . 7
⊢ (((𝑌 ∈ dom fBas ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌)) |
| 25 | 5, 6, 7, 23, 24 | syl31anc 1375 |
. . . . . 6
⊢ (𝜑 → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌)) |
| 26 | | fbsspw 23840 |
. . . . . 6
⊢ (ran
(𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌) → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ⊆ 𝒫 𝑌) |
| 27 | 25, 26 | syl 17 |
. . . . 5
⊢ (𝜑 → ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ⊆ 𝒫 𝑌) |
| 28 | 3, 27 | unssd 4192 |
. . . 4
⊢ (𝜑 → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ⊆ 𝒫 𝑌) |
| 29 | | ssun1 4178 |
. . . . 5
⊢ 𝐵 ⊆ (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) |
| 30 | | fbasne0 23838 |
. . . . . 6
⊢ (𝐵 ∈ (fBas‘𝑌) → 𝐵 ≠ ∅) |
| 31 | 1, 30 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐵 ≠ ∅) |
| 32 | | ssn0 4404 |
. . . . 5
⊢ ((𝐵 ⊆ (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∧ 𝐵 ≠ ∅) → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ≠ ∅) |
| 33 | 29, 31, 32 | sylancr 587 |
. . . 4
⊢ (𝜑 → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ≠ ∅) |
| 34 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) = (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) |
| 35 | 34 | elrnmpt 5969 |
. . . . . . . . 9
⊢ (𝑡 ∈ V → (𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑡 = (◡𝐹 “ 𝑥))) |
| 36 | 35 | elv 3485 |
. . . . . . . 8
⊢ (𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑡 = (◡𝐹 “ 𝑥)) |
| 37 | | 0nelfil 23857 |
. . . . . . . . . . . . . 14
⊢ (𝐿 ∈ (Fil‘𝑋) → ¬ ∅ ∈
𝐿) |
| 38 | 6, 37 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ¬ ∅ ∈ 𝐿) |
| 39 | 38 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → ¬ ∅ ∈ 𝐿) |
| 40 | 6 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝐿 ∈ (Fil‘𝑋)) |
| 41 | 8 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿) |
| 42 | 15, 1, 7 | 3jca 1129 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋)) |
| 43 | 42 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋)) |
| 44 | | ssfg 23880 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈ (fBas‘𝑌) → 𝐵 ⊆ (𝑌filGen𝐵)) |
| 45 | 1, 44 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐵 ⊆ (𝑌filGen𝐵)) |
| 46 | 45 | sselda 3983 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ∈ (𝑌filGen𝐵)) |
| 47 | 19 | imaelfm 23959 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑠 ∈ (𝑌filGen𝐵)) → (𝐹 “ 𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵)) |
| 48 | 43, 46, 47 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝐹 “ 𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵)) |
| 49 | 41, 48 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝐹 “ 𝑠) ∈ 𝐿) |
| 50 | 40, 49 | jca 511 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝐿 ∈ (Fil‘𝑋) ∧ (𝐹 “ 𝑠) ∈ 𝐿)) |
| 51 | | filin 23862 |
. . . . . . . . . . . . . . 15
⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹 “ 𝑠) ∈ 𝐿 ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿) |
| 52 | 51 | 3expa 1119 |
. . . . . . . . . . . . . 14
⊢ (((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹 “ 𝑠) ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿) |
| 53 | 50, 52 | sylan 580 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿) |
| 54 | | eleq1 2829 |
. . . . . . . . . . . . 13
⊢ (((𝐹 “ 𝑠) ∩ 𝑥) = ∅ → (((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿 ↔ ∅ ∈ 𝐿)) |
| 55 | 53, 54 | syl5ibcom 245 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (((𝐹 “ 𝑠) ∩ 𝑥) = ∅ → ∅ ∈ 𝐿)) |
| 56 | 39, 55 | mtod 198 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → ¬ ((𝐹 “ 𝑠) ∩ 𝑥) = ∅) |
| 57 | | neq0 4352 |
. . . . . . . . . . . 12
⊢ (¬
((𝐹 “ 𝑠) ∩ 𝑥) = ∅ ↔ ∃𝑡 𝑡 ∈ ((𝐹 “ 𝑠) ∩ 𝑥)) |
| 58 | | elin 3967 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ ((𝐹 “ 𝑠) ∩ 𝑥) ↔ (𝑡 ∈ (𝐹 “ 𝑠) ∧ 𝑡 ∈ 𝑥)) |
| 59 | | ffun 6739 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹:𝑌⟶𝑋 → Fun 𝐹) |
| 60 | | fvelima 6974 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Fun
𝐹 ∧ 𝑡 ∈ (𝐹 “ 𝑠)) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑡) |
| 61 | 60 | ex 412 |
. . . . . . . . . . . . . . . . . 18
⊢ (Fun
𝐹 → (𝑡 ∈ (𝐹 “ 𝑠) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑡)) |
| 62 | 7, 59, 61 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑡 ∈ (𝐹 “ 𝑠) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑡)) |
| 63 | 62 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (𝑡 ∈ (𝐹 “ 𝑠) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑡)) |
| 64 | 7, 59 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → Fun 𝐹) |
| 65 | 64 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) ∧ 𝑦 ∈ 𝑠) → Fun 𝐹) |
| 66 | | fbelss 23841 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ 𝑠 ∈ 𝐵) → 𝑠 ⊆ 𝑌) |
| 67 | 1, 66 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ⊆ 𝑌) |
| 68 | 7 | fdmd 6746 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → dom 𝐹 = 𝑌) |
| 69 | 68 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → dom 𝐹 = 𝑌) |
| 70 | 67, 69 | sseqtrrd 4021 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ⊆ dom 𝐹) |
| 71 | 70 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → 𝑠 ⊆ dom 𝐹) |
| 72 | 71 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) ∧ 𝑦 ∈ 𝑠) → 𝑦 ∈ dom 𝐹) |
| 73 | | fvimacnv 7073 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ dom 𝐹) → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑦 ∈ (◡𝐹 “ 𝑥))) |
| 74 | 65, 72, 73 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑦 ∈ (◡𝐹 “ 𝑥))) |
| 75 | | inelcm 4465 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ 𝑠 ∧ 𝑦 ∈ (◡𝐹 “ 𝑥)) → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅) |
| 76 | 75 | ex 412 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ 𝑠 → (𝑦 ∈ (◡𝐹 “ 𝑥) → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅)) |
| 77 | 76 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) ∧ 𝑦 ∈ 𝑠) → (𝑦 ∈ (◡𝐹 “ 𝑥) → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅)) |
| 78 | 74, 77 | sylbid 240 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) ∈ 𝑥 → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅)) |
| 79 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑦) = 𝑡 → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑡 ∈ 𝑥)) |
| 80 | 79 | imbi1d 341 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹‘𝑦) = 𝑡 → (((𝐹‘𝑦) ∈ 𝑥 → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅) ↔ (𝑡 ∈ 𝑥 → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅))) |
| 81 | 78, 80 | syl5ibcom 245 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) = 𝑡 → (𝑡 ∈ 𝑥 → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅))) |
| 82 | 81 | rexlimdva 3155 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑡 → (𝑡 ∈ 𝑥 → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅))) |
| 83 | 63, 82 | syld 47 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (𝑡 ∈ (𝐹 “ 𝑠) → (𝑡 ∈ 𝑥 → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅))) |
| 84 | 83 | impd 410 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → ((𝑡 ∈ (𝐹 “ 𝑠) ∧ 𝑡 ∈ 𝑥) → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅)) |
| 85 | 58, 84 | biimtrid 242 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (𝑡 ∈ ((𝐹 “ 𝑠) ∩ 𝑥) → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅)) |
| 86 | 85 | exlimdv 1933 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (∃𝑡 𝑡 ∈ ((𝐹 “ 𝑠) ∩ 𝑥) → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅)) |
| 87 | 57, 86 | biimtrid 242 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (¬ ((𝐹 “ 𝑠) ∩ 𝑥) = ∅ → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅)) |
| 88 | 56, 87 | mpd 15 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅) |
| 89 | | ineq2 4214 |
. . . . . . . . . . 11
⊢ (𝑡 = (◡𝐹 “ 𝑥) → (𝑠 ∩ 𝑡) = (𝑠 ∩ (◡𝐹 “ 𝑥))) |
| 90 | 89 | neeq1d 3000 |
. . . . . . . . . 10
⊢ (𝑡 = (◡𝐹 “ 𝑥) → ((𝑠 ∩ 𝑡) ≠ ∅ ↔ (𝑠 ∩ (◡𝐹 “ 𝑥)) ≠ ∅)) |
| 91 | 88, 90 | syl5ibrcom 247 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (𝑡 = (◡𝐹 “ 𝑥) → (𝑠 ∩ 𝑡) ≠ ∅)) |
| 92 | 91 | rexlimdva 3155 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (∃𝑥 ∈ 𝐿 𝑡 = (◡𝐹 “ 𝑥) → (𝑠 ∩ 𝑡) ≠ ∅)) |
| 93 | 36, 92 | biimtrid 242 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅)) |
| 94 | 93 | expimpd 453 |
. . . . . 6
⊢ (𝜑 → ((𝑠 ∈ 𝐵 ∧ 𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) → (𝑠 ∩ 𝑡) ≠ ∅)) |
| 95 | 94 | ralrimivv 3200 |
. . . . 5
⊢ (𝜑 → ∀𝑠 ∈ 𝐵 ∀𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))(𝑠 ∩ 𝑡) ≠ ∅) |
| 96 | | fbunfip 23877 |
. . . . . 6
⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌)) → (¬ ∅ ∈
(fi‘(𝐵 ∪ ran
(𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ↔ ∀𝑠 ∈ 𝐵 ∀𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))(𝑠 ∩ 𝑡) ≠ ∅)) |
| 97 | 1, 25, 96 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (¬ ∅ ∈
(fi‘(𝐵 ∪ ran
(𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ↔ ∀𝑠 ∈ 𝐵 ∀𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))(𝑠 ∩ 𝑡) ≠ ∅)) |
| 98 | 95, 97 | mpbird 257 |
. . . 4
⊢ (𝜑 → ¬ ∅ ∈
(fi‘(𝐵 ∪ ran
(𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) |
| 99 | | fsubbas 23875 |
. . . . 5
⊢ (𝑌 ∈ dom fBas →
((fi‘(𝐵 ∪ ran
(𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌) ↔ ((𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ⊆ 𝒫 𝑌 ∧ (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ≠ ∅ ∧ ¬ ∅ ∈
(fi‘(𝐵 ∪ ran
(𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))))) |
| 100 | 1, 4, 99 | 3syl 18 |
. . . 4
⊢ (𝜑 → ((fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌) ↔ ((𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ⊆ 𝒫 𝑌 ∧ (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ≠ ∅ ∧ ¬ ∅ ∈
(fi‘(𝐵 ∪ ran
(𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))))) |
| 101 | 28, 33, 98, 100 | mpbir3and 1343 |
. . 3
⊢ (𝜑 → (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌)) |
| 102 | | fgcl 23886 |
. . 3
⊢
((fi‘(𝐵 ∪
ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌) → (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) ∈ (Fil‘𝑌)) |
| 103 | 101, 102 | syl 17 |
. 2
⊢ (𝜑 → (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) ∈ (Fil‘𝑌)) |
| 104 | | unexg 7763 |
. . . . . 6
⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌)) → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∈ V) |
| 105 | 1, 25, 104 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∈ V) |
| 106 | | ssfii 9459 |
. . . . 5
⊢ ((𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ∈ V → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) |
| 107 | 105, 106 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) |
| 108 | 107 | unssad 4193 |
. . 3
⊢ (𝜑 → 𝐵 ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) |
| 109 | | ssfg 23880 |
. . . 4
⊢
((fi‘(𝐵 ∪
ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌) → (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))))) |
| 110 | 101, 109 | syl 17 |
. . 3
⊢ (𝜑 → (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))))) |
| 111 | 108, 110 | sstrd 3994 |
. 2
⊢ (𝜑 → 𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))))) |
| 112 | 1, 6, 7, 8 | fmfnfmlem4 23965 |
. . . . 5
⊢ (𝜑 → (𝑡 ∈ 𝐿 ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡))) |
| 113 | | elfm 23955 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐿 ∧ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝑡 ∈ ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡))) |
| 114 | 15, 101, 7, 113 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (𝑡 ∈ ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡))) |
| 115 | 112, 114 | bitr4d 282 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ 𝐿 ↔ 𝑡 ∈ ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))))) |
| 116 | 115 | eqrdv 2735 |
. . 3
⊢ (𝜑 → 𝐿 = ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))))) |
| 117 | | eqid 2737 |
. . . . 5
⊢ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) |
| 118 | 117 | fmfg 23957 |
. . . 4
⊢ ((𝑋 ∈ 𝐿 ∧ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))))) |
| 119 | 15, 101, 7, 118 | syl3anc 1373 |
. . 3
⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))))) |
| 120 | 116, 119 | eqtrd 2777 |
. 2
⊢ (𝜑 → 𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))))) |
| 121 | | sseq2 4010 |
. . . 4
⊢ (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) → (𝐵 ⊆ 𝑓 ↔ 𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))))) |
| 122 | | fveq2 6906 |
. . . . 5
⊢ (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) → ((𝑋 FilMap 𝐹)‘𝑓) = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))))) |
| 123 | 122 | eqeq2d 2748 |
. . . 4
⊢ (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) → (𝐿 = ((𝑋 FilMap 𝐹)‘𝑓) ↔ 𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))))))) |
| 124 | 121, 123 | anbi12d 632 |
. . 3
⊢ (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) → ((𝐵 ⊆ 𝑓 ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘𝑓)) ↔ (𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))))))) |
| 125 | 124 | rspcev 3622 |
. 2
⊢ (((𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) ∈ (Fil‘𝑌) ∧ (𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥))))) ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (◡𝐹 “ 𝑥)))))))) → ∃𝑓 ∈ (Fil‘𝑌)(𝐵 ⊆ 𝑓 ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘𝑓))) |
| 126 | 103, 111,
120, 125 | syl12anc 837 |
1
⊢ (𝜑 → ∃𝑓 ∈ (Fil‘𝑌)(𝐵 ⊆ 𝑓 ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘𝑓))) |