MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fmfnfm Structured version   Visualization version   GIF version

Theorem fmfnfm 21983
Description: A filter finer than an image filter is an image filter of the same function. (Contributed by Jeff Hankins, 13-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.)
Hypotheses
Ref Expression
fmfnfm.b (𝜑𝐵 ∈ (fBas‘𝑌))
fmfnfm.l (𝜑𝐿 ∈ (Fil‘𝑋))
fmfnfm.f (𝜑𝐹:𝑌𝑋)
fmfnfm.fm (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)
Assertion
Ref Expression
fmfnfm (𝜑 → ∃𝑓 ∈ (Fil‘𝑌)(𝐵𝑓𝐿 = ((𝑋 FilMap 𝐹)‘𝑓)))
Distinct variable groups:   𝐵,𝑓   𝑓,𝐹   𝑓,𝐿   𝑓,𝑋   𝑓,𝑌
Allowed substitution hint:   𝜑(𝑓)

Proof of Theorem fmfnfm
Dummy variables 𝑠 𝑡 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fmfnfm.b . . . . . 6 (𝜑𝐵 ∈ (fBas‘𝑌))
2 fbsspw 21857 . . . . . 6 (𝐵 ∈ (fBas‘𝑌) → 𝐵 ⊆ 𝒫 𝑌)
31, 2syl 17 . . . . 5 (𝜑𝐵 ⊆ 𝒫 𝑌)
4 elfvdm 6362 . . . . . . . 8 (𝐵 ∈ (fBas‘𝑌) → 𝑌 ∈ dom fBas)
51, 4syl 17 . . . . . . 7 (𝜑𝑌 ∈ dom fBas)
6 fmfnfm.l . . . . . . 7 (𝜑𝐿 ∈ (Fil‘𝑋))
7 fmfnfm.f . . . . . . 7 (𝜑𝐹:𝑌𝑋)
8 fmfnfm.fm . . . . . . . 8 (𝜑 → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)
9 ffn 6186 . . . . . . . . . . 11 (𝐹:𝑌𝑋𝐹 Fn 𝑌)
10 dffn4 6263 . . . . . . . . . . 11 (𝐹 Fn 𝑌𝐹:𝑌onto→ran 𝐹)
119, 10sylib 208 . . . . . . . . . 10 (𝐹:𝑌𝑋𝐹:𝑌onto→ran 𝐹)
12 foima 6262 . . . . . . . . . 10 (𝐹:𝑌onto→ran 𝐹 → (𝐹𝑌) = ran 𝐹)
137, 11, 123syl 18 . . . . . . . . 9 (𝜑 → (𝐹𝑌) = ran 𝐹)
14 filtop 21880 . . . . . . . . . . 11 (𝐿 ∈ (Fil‘𝑋) → 𝑋𝐿)
156, 14syl 17 . . . . . . . . . 10 (𝜑𝑋𝐿)
16 fgcl 21903 . . . . . . . . . . 11 (𝐵 ∈ (fBas‘𝑌) → (𝑌filGen𝐵) ∈ (Fil‘𝑌))
17 filtop 21880 . . . . . . . . . . 11 ((𝑌filGen𝐵) ∈ (Fil‘𝑌) → 𝑌 ∈ (𝑌filGen𝐵))
181, 16, 173syl 18 . . . . . . . . . 10 (𝜑𝑌 ∈ (𝑌filGen𝐵))
19 eqid 2771 . . . . . . . . . . 11 (𝑌filGen𝐵) = (𝑌filGen𝐵)
2019imaelfm 21976 . . . . . . . . . 10 (((𝑋𝐿𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑌 ∈ (𝑌filGen𝐵)) → (𝐹𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
2115, 1, 7, 18, 20syl31anc 1479 . . . . . . . . 9 (𝜑 → (𝐹𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
2213, 21eqeltrrd 2851 . . . . . . . 8 (𝜑 → ran 𝐹 ∈ ((𝑋 FilMap 𝐹)‘𝐵))
238, 22sseldd 3754 . . . . . . 7 (𝜑 → ran 𝐹𝐿)
24 rnelfmlem 21977 . . . . . . 7 (((𝑌 ∈ dom fBas ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌))
255, 6, 7, 23, 24syl31anc 1479 . . . . . 6 (𝜑 → ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌))
26 fbsspw 21857 . . . . . 6 (ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ⊆ 𝒫 𝑌)
2725, 26syl 17 . . . . 5 (𝜑 → ran (𝑥𝐿 ↦ (𝐹𝑥)) ⊆ 𝒫 𝑌)
283, 27unssd 3941 . . . 4 (𝜑 → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ⊆ 𝒫 𝑌)
29 ssun1 3928 . . . . 5 𝐵 ⊆ (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))
30 fbasne0 21855 . . . . . 6 (𝐵 ∈ (fBas‘𝑌) → 𝐵 ≠ ∅)
311, 30syl 17 . . . . 5 (𝜑𝐵 ≠ ∅)
32 ssn0 4121 . . . . 5 ((𝐵 ⊆ (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∧ 𝐵 ≠ ∅) → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ≠ ∅)
3329, 31, 32sylancr 569 . . . 4 (𝜑 → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ≠ ∅)
34 vex 3354 . . . . . . . . 9 𝑡 ∈ V
35 eqid 2771 . . . . . . . . . 10 (𝑥𝐿 ↦ (𝐹𝑥)) = (𝑥𝐿 ↦ (𝐹𝑥))
3635elrnmpt 5511 . . . . . . . . 9 (𝑡 ∈ V → (𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑡 = (𝐹𝑥)))
3734, 36ax-mp 5 . . . . . . . 8 (𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑡 = (𝐹𝑥))
38 0nelfil 21874 . . . . . . . . . . . . . 14 (𝐿 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝐿)
396, 38syl 17 . . . . . . . . . . . . 13 (𝜑 → ¬ ∅ ∈ 𝐿)
4039ad2antrr 699 . . . . . . . . . . . 12 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → ¬ ∅ ∈ 𝐿)
416adantr 466 . . . . . . . . . . . . . . 15 ((𝜑𝑠𝐵) → 𝐿 ∈ (Fil‘𝑋))
428adantr 466 . . . . . . . . . . . . . . . 16 ((𝜑𝑠𝐵) → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)
4315, 1, 73jca 1122 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋𝐿𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋))
4443adantr 466 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠𝐵) → (𝑋𝐿𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋))
45 ssfg 21897 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ (fBas‘𝑌) → 𝐵 ⊆ (𝑌filGen𝐵))
461, 45syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ⊆ (𝑌filGen𝐵))
4746sselda 3753 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠𝐵) → 𝑠 ∈ (𝑌filGen𝐵))
4819imaelfm 21976 . . . . . . . . . . . . . . . . 17 (((𝑋𝐿𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑠 ∈ (𝑌filGen𝐵)) → (𝐹𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
4944, 47, 48syl2anc 567 . . . . . . . . . . . . . . . 16 ((𝜑𝑠𝐵) → (𝐹𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
5042, 49sseldd 3754 . . . . . . . . . . . . . . 15 ((𝜑𝑠𝐵) → (𝐹𝑠) ∈ 𝐿)
5141, 50jca 497 . . . . . . . . . . . . . 14 ((𝜑𝑠𝐵) → (𝐿 ∈ (Fil‘𝑋) ∧ (𝐹𝑠) ∈ 𝐿))
52 filin 21879 . . . . . . . . . . . . . . 15 ((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹𝑠) ∈ 𝐿𝑥𝐿) → ((𝐹𝑠) ∩ 𝑥) ∈ 𝐿)
53523expa 1111 . . . . . . . . . . . . . 14 (((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹𝑠) ∈ 𝐿) ∧ 𝑥𝐿) → ((𝐹𝑠) ∩ 𝑥) ∈ 𝐿)
5451, 53sylan 563 . . . . . . . . . . . . 13 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → ((𝐹𝑠) ∩ 𝑥) ∈ 𝐿)
55 eleq1 2838 . . . . . . . . . . . . 13 (((𝐹𝑠) ∩ 𝑥) = ∅ → (((𝐹𝑠) ∩ 𝑥) ∈ 𝐿 ↔ ∅ ∈ 𝐿))
5654, 55syl5ibcom 235 . . . . . . . . . . . 12 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (((𝐹𝑠) ∩ 𝑥) = ∅ → ∅ ∈ 𝐿))
5740, 56mtod 189 . . . . . . . . . . 11 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → ¬ ((𝐹𝑠) ∩ 𝑥) = ∅)
58 neq0 4078 . . . . . . . . . . . 12 (¬ ((𝐹𝑠) ∩ 𝑥) = ∅ ↔ ∃𝑡 𝑡 ∈ ((𝐹𝑠) ∩ 𝑥))
59 elin 3948 . . . . . . . . . . . . . 14 (𝑡 ∈ ((𝐹𝑠) ∩ 𝑥) ↔ (𝑡 ∈ (𝐹𝑠) ∧ 𝑡𝑥))
60 ffun 6189 . . . . . . . . . . . . . . . . . 18 (𝐹:𝑌𝑋 → Fun 𝐹)
61 fvelima 6391 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝐹𝑡 ∈ (𝐹𝑠)) → ∃𝑦𝑠 (𝐹𝑦) = 𝑡)
6261ex 397 . . . . . . . . . . . . . . . . . 18 (Fun 𝐹 → (𝑡 ∈ (𝐹𝑠) → ∃𝑦𝑠 (𝐹𝑦) = 𝑡))
637, 60, 623syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑡 ∈ (𝐹𝑠) → ∃𝑦𝑠 (𝐹𝑦) = 𝑡))
6463ad2antrr 699 . . . . . . . . . . . . . . . 16 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (𝑡 ∈ (𝐹𝑠) → ∃𝑦𝑠 (𝐹𝑦) = 𝑡))
657, 60syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → Fun 𝐹)
6665ad3antrrr 703 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑠𝐵) ∧ 𝑥𝐿) ∧ 𝑦𝑠) → Fun 𝐹)
67 fbelss 21858 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐵 ∈ (fBas‘𝑌) ∧ 𝑠𝐵) → 𝑠𝑌)
681, 67sylan 563 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑠𝐵) → 𝑠𝑌)
69 fdm 6192 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹:𝑌𝑋 → dom 𝐹 = 𝑌)
707, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → dom 𝐹 = 𝑌)
7170adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑠𝐵) → dom 𝐹 = 𝑌)
7268, 71sseqtr4d 3792 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑠𝐵) → 𝑠 ⊆ dom 𝐹)
7372adantr 466 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → 𝑠 ⊆ dom 𝐹)
7473sselda 3753 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑠𝐵) ∧ 𝑥𝐿) ∧ 𝑦𝑠) → 𝑦 ∈ dom 𝐹)
75 fvimacnv 6476 . . . . . . . . . . . . . . . . . . . 20 ((Fun 𝐹𝑦 ∈ dom 𝐹) → ((𝐹𝑦) ∈ 𝑥𝑦 ∈ (𝐹𝑥)))
7666, 74, 75syl2anc 567 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑠𝐵) ∧ 𝑥𝐿) ∧ 𝑦𝑠) → ((𝐹𝑦) ∈ 𝑥𝑦 ∈ (𝐹𝑥)))
77 inelcm 4176 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦𝑠𝑦 ∈ (𝐹𝑥)) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅)
7877ex 397 . . . . . . . . . . . . . . . . . . . 20 (𝑦𝑠 → (𝑦 ∈ (𝐹𝑥) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
7978adantl 467 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑠𝐵) ∧ 𝑥𝐿) ∧ 𝑦𝑠) → (𝑦 ∈ (𝐹𝑥) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
8076, 79sylbid 230 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑠𝐵) ∧ 𝑥𝐿) ∧ 𝑦𝑠) → ((𝐹𝑦) ∈ 𝑥 → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
81 eleq1 2838 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑦) = 𝑡 → ((𝐹𝑦) ∈ 𝑥𝑡𝑥))
8281imbi1d 330 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑦) = 𝑡 → (((𝐹𝑦) ∈ 𝑥 → (𝑠 ∩ (𝐹𝑥)) ≠ ∅) ↔ (𝑡𝑥 → (𝑠 ∩ (𝐹𝑥)) ≠ ∅)))
8380, 82syl5ibcom 235 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑠𝐵) ∧ 𝑥𝐿) ∧ 𝑦𝑠) → ((𝐹𝑦) = 𝑡 → (𝑡𝑥 → (𝑠 ∩ (𝐹𝑥)) ≠ ∅)))
8483rexlimdva 3179 . . . . . . . . . . . . . . . 16 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (∃𝑦𝑠 (𝐹𝑦) = 𝑡 → (𝑡𝑥 → (𝑠 ∩ (𝐹𝑥)) ≠ ∅)))
8564, 84syld 47 . . . . . . . . . . . . . . 15 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (𝑡 ∈ (𝐹𝑠) → (𝑡𝑥 → (𝑠 ∩ (𝐹𝑥)) ≠ ∅)))
8685impd 396 . . . . . . . . . . . . . 14 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → ((𝑡 ∈ (𝐹𝑠) ∧ 𝑡𝑥) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
8759, 86syl5bi 232 . . . . . . . . . . . . 13 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (𝑡 ∈ ((𝐹𝑠) ∩ 𝑥) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
8887exlimdv 2013 . . . . . . . . . . . 12 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (∃𝑡 𝑡 ∈ ((𝐹𝑠) ∩ 𝑥) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
8958, 88syl5bi 232 . . . . . . . . . . 11 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (¬ ((𝐹𝑠) ∩ 𝑥) = ∅ → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
9057, 89mpd 15 . . . . . . . . . 10 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅)
91 ineq2 3960 . . . . . . . . . . 11 (𝑡 = (𝐹𝑥) → (𝑠𝑡) = (𝑠 ∩ (𝐹𝑥)))
9291neeq1d 3002 . . . . . . . . . 10 (𝑡 = (𝐹𝑥) → ((𝑠𝑡) ≠ ∅ ↔ (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
9390, 92syl5ibrcom 237 . . . . . . . . 9 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (𝑡 = (𝐹𝑥) → (𝑠𝑡) ≠ ∅))
9493rexlimdva 3179 . . . . . . . 8 ((𝜑𝑠𝐵) → (∃𝑥𝐿 𝑡 = (𝐹𝑥) → (𝑠𝑡) ≠ ∅))
9537, 94syl5bi 232 . . . . . . 7 ((𝜑𝑠𝐵) → (𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) → (𝑠𝑡) ≠ ∅))
9695expimpd 441 . . . . . 6 (𝜑 → ((𝑠𝐵𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))) → (𝑠𝑡) ≠ ∅))
9796ralrimivv 3119 . . . . 5 (𝜑 → ∀𝑠𝐵𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝑠𝑡) ≠ ∅)
98 fbunfip 21894 . . . . . 6 ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌)) → (¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ↔ ∀𝑠𝐵𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝑠𝑡) ≠ ∅))
991, 25, 98syl2anc 567 . . . . 5 (𝜑 → (¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ↔ ∀𝑠𝐵𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝑠𝑡) ≠ ∅))
10097, 99mpbird 247 . . . 4 (𝜑 → ¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
101 fsubbas 21892 . . . . 5 (𝑌 ∈ dom fBas → ((fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∈ (fBas‘𝑌) ↔ ((𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ⊆ 𝒫 𝑌 ∧ (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
1021, 4, 1013syl 18 . . . 4 (𝜑 → ((fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∈ (fBas‘𝑌) ↔ ((𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ⊆ 𝒫 𝑌 ∧ (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
10328, 33, 100, 102mpbir3and 1427 . . 3 (𝜑 → (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∈ (fBas‘𝑌))
104 fgcl 21903 . . 3 ((fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∈ (fBas‘𝑌) → (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ∈ (Fil‘𝑌))
105103, 104syl 17 . 2 (𝜑 → (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ∈ (Fil‘𝑌))
106 unexg 7107 . . . . . 6 ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌)) → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ V)
1071, 25, 106syl2anc 567 . . . . 5 (𝜑 → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ V)
108 ssfii 8482 . . . . 5 ((𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ V → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ⊆ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
109107, 108syl 17 . . . 4 (𝜑 → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ⊆ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
110109unssad 3942 . . 3 (𝜑𝐵 ⊆ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
111 ssfg 21897 . . . 4 ((fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∈ (fBas‘𝑌) → (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))))
112103, 111syl 17 . . 3 (𝜑 → (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))))
113110, 112sstrd 3763 . 2 (𝜑𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))))
1141, 6, 7, 8fmfnfmlem4 21982 . . . . 5 (𝜑 → (𝑡𝐿 ↔ (𝑡𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡)))
115 elfm 21972 . . . . . 6 ((𝑋𝐿 ∧ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝑡 ∈ ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ↔ (𝑡𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡)))
11615, 103, 7, 115syl3anc 1476 . . . . 5 (𝜑 → (𝑡 ∈ ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ↔ (𝑡𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡)))
117114, 116bitr4d 271 . . . 4 (𝜑 → (𝑡𝐿𝑡 ∈ ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
118117eqrdv 2769 . . 3 (𝜑𝐿 = ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))))
119 eqid 2771 . . . . 5 (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
120119fmfg 21974 . . . 4 ((𝑋𝐿 ∧ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
12115, 103, 7, 120syl3anc 1476 . . 3 (𝜑 → ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
122118, 121eqtrd 2805 . 2 (𝜑𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
123 sseq2 3777 . . . 4 (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) → (𝐵𝑓𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
124 fveq2 6333 . . . . 5 (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) → ((𝑋 FilMap 𝐹)‘𝑓) = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
125124eqeq2d 2781 . . . 4 (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) → (𝐿 = ((𝑋 FilMap 𝐹)‘𝑓) ↔ 𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))))))
126123, 125anbi12d 610 . . 3 (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) → ((𝐵𝑓𝐿 = ((𝑋 FilMap 𝐹)‘𝑓)) ↔ (𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))))
127126rspcev 3461 . 2 (((𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ∈ (Fil‘𝑌) ∧ (𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))) → ∃𝑓 ∈ (Fil‘𝑌)(𝐵𝑓𝐿 = ((𝑋 FilMap 𝐹)‘𝑓)))
128105, 113, 122, 127syl12anc 1474 1 (𝜑 → ∃𝑓 ∈ (Fil‘𝑌)(𝐵𝑓𝐿 = ((𝑋 FilMap 𝐹)‘𝑓)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wex 1852  wcel 2145  wne 2943  wral 3061  wrex 3062  Vcvv 3351  cun 3722  cin 3723  wss 3724  c0 4064  𝒫 cpw 4298  cmpt 4864  ccnv 5249  dom cdm 5250  ran crn 5251  cima 5253  Fun wfun 6026   Fn wfn 6027  wf 6028  ontowfo 6030  cfv 6032  (class class class)co 6794  ficfi 8473  fBascfbas 19950  filGencfg 19951  Filcfil 21870   FilMap cfm 21958
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7097
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3589  df-csb 3684  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-pss 3740  df-nul 4065  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5824  df-ord 5870  df-on 5871  df-lim 5872  df-suc 5873  df-iota 5995  df-fun 6034  df-fn 6035  df-f 6036  df-f1 6037  df-fo 6038  df-f1o 6039  df-fv 6040  df-ov 6797  df-oprab 6798  df-mpt2 6799  df-om 7214  df-wrecs 7560  df-recs 7622  df-rdg 7660  df-1o 7714  df-oadd 7718  df-er 7897  df-en 8111  df-fin 8114  df-fi 8474  df-fbas 19959  df-fg 19960  df-fil 21871  df-fm 21963
This theorem is referenced by:  fmufil  21984  cnpfcf  22066
  Copyright terms: Public domain W3C validator