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

Theorem fmfnfm 22254
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 22128 . . . . . 6 (𝐵 ∈ (fBas‘𝑌) → 𝐵 ⊆ 𝒫 𝑌)
31, 2syl 17 . . . . 5 (𝜑𝐵 ⊆ 𝒫 𝑌)
4 elfvdm 6577 . . . . . . . 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 6389 . . . . . . . . . . 11 (𝐹:𝑌𝑋𝐹 Fn 𝑌)
10 dffn4 6471 . . . . . . . . . . 11 (𝐹 Fn 𝑌𝐹:𝑌onto→ran 𝐹)
119, 10sylib 219 . . . . . . . . . 10 (𝐹:𝑌𝑋𝐹:𝑌onto→ran 𝐹)
12 foima 6470 . . . . . . . . . 10 (𝐹:𝑌onto→ran 𝐹 → (𝐹𝑌) = ran 𝐹)
137, 11, 123syl 18 . . . . . . . . 9 (𝜑 → (𝐹𝑌) = ran 𝐹)
14 filtop 22151 . . . . . . . . . . 11 (𝐿 ∈ (Fil‘𝑋) → 𝑋𝐿)
156, 14syl 17 . . . . . . . . . 10 (𝜑𝑋𝐿)
16 fgcl 22174 . . . . . . . . . . 11 (𝐵 ∈ (fBas‘𝑌) → (𝑌filGen𝐵) ∈ (Fil‘𝑌))
17 filtop 22151 . . . . . . . . . . 11 ((𝑌filGen𝐵) ∈ (Fil‘𝑌) → 𝑌 ∈ (𝑌filGen𝐵))
181, 16, 173syl 18 . . . . . . . . . 10 (𝜑𝑌 ∈ (𝑌filGen𝐵))
19 eqid 2797 . . . . . . . . . . 11 (𝑌filGen𝐵) = (𝑌filGen𝐵)
2019imaelfm 22247 . . . . . . . . . 10 (((𝑋𝐿𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑌 ∈ (𝑌filGen𝐵)) → (𝐹𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
2115, 1, 7, 18, 20syl31anc 1366 . . . . . . . . 9 (𝜑 → (𝐹𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
2213, 21eqeltrrd 2886 . . . . . . . 8 (𝜑 → ran 𝐹 ∈ ((𝑋 FilMap 𝐹)‘𝐵))
238, 22sseldd 3896 . . . . . . 7 (𝜑 → ran 𝐹𝐿)
24 rnelfmlem 22248 . . . . . . 7 (((𝑌 ∈ dom fBas ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌))
255, 6, 7, 23, 24syl31anc 1366 . . . . . 6 (𝜑 → ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌))
26 fbsspw 22128 . . . . . 6 (ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ⊆ 𝒫 𝑌)
2725, 26syl 17 . . . . 5 (𝜑 → ran (𝑥𝐿 ↦ (𝐹𝑥)) ⊆ 𝒫 𝑌)
283, 27unssd 4089 . . . 4 (𝜑 → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ⊆ 𝒫 𝑌)
29 ssun1 4075 . . . . 5 𝐵 ⊆ (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))
30 fbasne0 22126 . . . . . 6 (𝐵 ∈ (fBas‘𝑌) → 𝐵 ≠ ∅)
311, 30syl 17 . . . . 5 (𝜑𝐵 ≠ ∅)
32 ssn0 4280 . . . . 5 ((𝐵 ⊆ (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∧ 𝐵 ≠ ∅) → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ≠ ∅)
3329, 31, 32sylancr 587 . . . 4 (𝜑 → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ≠ ∅)
34 eqid 2797 . . . . . . . . . 10 (𝑥𝐿 ↦ (𝐹𝑥)) = (𝑥𝐿 ↦ (𝐹𝑥))
3534elrnmpt 5717 . . . . . . . . 9 (𝑡 ∈ V → (𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑡 = (𝐹𝑥)))
3635elv 3445 . . . . . . . 8 (𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑡 = (𝐹𝑥))
37 0nelfil 22145 . . . . . . . . . . . . . 14 (𝐿 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝐿)
386, 37syl 17 . . . . . . . . . . . . 13 (𝜑 → ¬ ∅ ∈ 𝐿)
3938ad2antrr 722 . . . . . . . . . . . 12 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → ¬ ∅ ∈ 𝐿)
406adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑠𝐵) → 𝐿 ∈ (Fil‘𝑋))
418adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑠𝐵) → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)
4215, 1, 73jca 1121 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋𝐿𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋))
4342adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠𝐵) → (𝑋𝐿𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋))
44 ssfg 22168 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ (fBas‘𝑌) → 𝐵 ⊆ (𝑌filGen𝐵))
451, 44syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ⊆ (𝑌filGen𝐵))
4645sselda 3895 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠𝐵) → 𝑠 ∈ (𝑌filGen𝐵))
4719imaelfm 22247 . . . . . . . . . . . . . . . . 17 (((𝑋𝐿𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑠 ∈ (𝑌filGen𝐵)) → (𝐹𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
4843, 46, 47syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑𝑠𝐵) → (𝐹𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
4941, 48sseldd 3896 . . . . . . . . . . . . . . 15 ((𝜑𝑠𝐵) → (𝐹𝑠) ∈ 𝐿)
5040, 49jca 512 . . . . . . . . . . . . . 14 ((𝜑𝑠𝐵) → (𝐿 ∈ (Fil‘𝑋) ∧ (𝐹𝑠) ∈ 𝐿))
51 filin 22150 . . . . . . . . . . . . . . 15 ((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹𝑠) ∈ 𝐿𝑥𝐿) → ((𝐹𝑠) ∩ 𝑥) ∈ 𝐿)
52513expa 1111 . . . . . . . . . . . . . 14 (((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹𝑠) ∈ 𝐿) ∧ 𝑥𝐿) → ((𝐹𝑠) ∩ 𝑥) ∈ 𝐿)
5350, 52sylan 580 . . . . . . . . . . . . 13 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → ((𝐹𝑠) ∩ 𝑥) ∈ 𝐿)
54 eleq1 2872 . . . . . . . . . . . . 13 (((𝐹𝑠) ∩ 𝑥) = ∅ → (((𝐹𝑠) ∩ 𝑥) ∈ 𝐿 ↔ ∅ ∈ 𝐿))
5553, 54syl5ibcom 246 . . . . . . . . . . . 12 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (((𝐹𝑠) ∩ 𝑥) = ∅ → ∅ ∈ 𝐿))
5639, 55mtod 199 . . . . . . . . . . 11 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → ¬ ((𝐹𝑠) ∩ 𝑥) = ∅)
57 neq0 4235 . . . . . . . . . . . 12 (¬ ((𝐹𝑠) ∩ 𝑥) = ∅ ↔ ∃𝑡 𝑡 ∈ ((𝐹𝑠) ∩ 𝑥))
58 elin 4096 . . . . . . . . . . . . . 14 (𝑡 ∈ ((𝐹𝑠) ∩ 𝑥) ↔ (𝑡 ∈ (𝐹𝑠) ∧ 𝑡𝑥))
59 ffun 6392 . . . . . . . . . . . . . . . . . 18 (𝐹:𝑌𝑋 → Fun 𝐹)
60 fvelima 6606 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝐹𝑡 ∈ (𝐹𝑠)) → ∃𝑦𝑠 (𝐹𝑦) = 𝑡)
6160ex 413 . . . . . . . . . . . . . . . . . 18 (Fun 𝐹 → (𝑡 ∈ (𝐹𝑠) → ∃𝑦𝑠 (𝐹𝑦) = 𝑡))
627, 59, 613syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑡 ∈ (𝐹𝑠) → ∃𝑦𝑠 (𝐹𝑦) = 𝑡))
6362ad2antrr 722 . . . . . . . . . . . . . . . 16 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (𝑡 ∈ (𝐹𝑠) → ∃𝑦𝑠 (𝐹𝑦) = 𝑡))
647, 59syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → Fun 𝐹)
6564ad3antrrr 726 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑠𝐵) ∧ 𝑥𝐿) ∧ 𝑦𝑠) → Fun 𝐹)
66 fbelss 22129 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐵 ∈ (fBas‘𝑌) ∧ 𝑠𝐵) → 𝑠𝑌)
671, 66sylan 580 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑠𝐵) → 𝑠𝑌)
687fdmd 6398 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → dom 𝐹 = 𝑌)
6968adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑠𝐵) → dom 𝐹 = 𝑌)
7067, 69sseqtr4d 3935 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑠𝐵) → 𝑠 ⊆ dom 𝐹)
7170adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → 𝑠 ⊆ dom 𝐹)
7271sselda 3895 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑠𝐵) ∧ 𝑥𝐿) ∧ 𝑦𝑠) → 𝑦 ∈ dom 𝐹)
73 fvimacnv 6695 . . . . . . . . . . . . . . . . . . . 20 ((Fun 𝐹𝑦 ∈ dom 𝐹) → ((𝐹𝑦) ∈ 𝑥𝑦 ∈ (𝐹𝑥)))
7465, 72, 73syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑠𝐵) ∧ 𝑥𝐿) ∧ 𝑦𝑠) → ((𝐹𝑦) ∈ 𝑥𝑦 ∈ (𝐹𝑥)))
75 inelcm 4334 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦𝑠𝑦 ∈ (𝐹𝑥)) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅)
7675ex 413 . . . . . . . . . . . . . . . . . . . 20 (𝑦𝑠 → (𝑦 ∈ (𝐹𝑥) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
7776adantl 482 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑠𝐵) ∧ 𝑥𝐿) ∧ 𝑦𝑠) → (𝑦 ∈ (𝐹𝑥) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
7874, 77sylbid 241 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑠𝐵) ∧ 𝑥𝐿) ∧ 𝑦𝑠) → ((𝐹𝑦) ∈ 𝑥 → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
79 eleq1 2872 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑦) = 𝑡 → ((𝐹𝑦) ∈ 𝑥𝑡𝑥))
8079imbi1d 343 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑦) = 𝑡 → (((𝐹𝑦) ∈ 𝑥 → (𝑠 ∩ (𝐹𝑥)) ≠ ∅) ↔ (𝑡𝑥 → (𝑠 ∩ (𝐹𝑥)) ≠ ∅)))
8178, 80syl5ibcom 246 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑠𝐵) ∧ 𝑥𝐿) ∧ 𝑦𝑠) → ((𝐹𝑦) = 𝑡 → (𝑡𝑥 → (𝑠 ∩ (𝐹𝑥)) ≠ ∅)))
8281rexlimdva 3249 . . . . . . . . . . . . . . . 16 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (∃𝑦𝑠 (𝐹𝑦) = 𝑡 → (𝑡𝑥 → (𝑠 ∩ (𝐹𝑥)) ≠ ∅)))
8363, 82syld 47 . . . . . . . . . . . . . . 15 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (𝑡 ∈ (𝐹𝑠) → (𝑡𝑥 → (𝑠 ∩ (𝐹𝑥)) ≠ ∅)))
8483impd 411 . . . . . . . . . . . . . 14 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → ((𝑡 ∈ (𝐹𝑠) ∧ 𝑡𝑥) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
8558, 84syl5bi 243 . . . . . . . . . . . . 13 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (𝑡 ∈ ((𝐹𝑠) ∩ 𝑥) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
8685exlimdv 1915 . . . . . . . . . . . 12 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (∃𝑡 𝑡 ∈ ((𝐹𝑠) ∩ 𝑥) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
8757, 86syl5bi 243 . . . . . . . . . . 11 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (¬ ((𝐹𝑠) ∩ 𝑥) = ∅ → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
8856, 87mpd 15 . . . . . . . . . 10 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅)
89 ineq2 4109 . . . . . . . . . . 11 (𝑡 = (𝐹𝑥) → (𝑠𝑡) = (𝑠 ∩ (𝐹𝑥)))
9089neeq1d 3045 . . . . . . . . . 10 (𝑡 = (𝐹𝑥) → ((𝑠𝑡) ≠ ∅ ↔ (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
9188, 90syl5ibrcom 248 . . . . . . . . 9 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (𝑡 = (𝐹𝑥) → (𝑠𝑡) ≠ ∅))
9291rexlimdva 3249 . . . . . . . 8 ((𝜑𝑠𝐵) → (∃𝑥𝐿 𝑡 = (𝐹𝑥) → (𝑠𝑡) ≠ ∅))
9336, 92syl5bi 243 . . . . . . 7 ((𝜑𝑠𝐵) → (𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) → (𝑠𝑡) ≠ ∅))
9493expimpd 454 . . . . . 6 (𝜑 → ((𝑠𝐵𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))) → (𝑠𝑡) ≠ ∅))
9594ralrimivv 3159 . . . . 5 (𝜑 → ∀𝑠𝐵𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝑠𝑡) ≠ ∅)
96 fbunfip 22165 . . . . . 6 ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌)) → (¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ↔ ∀𝑠𝐵𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝑠𝑡) ≠ ∅))
971, 25, 96syl2anc 584 . . . . 5 (𝜑 → (¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ↔ ∀𝑠𝐵𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝑠𝑡) ≠ ∅))
9895, 97mpbird 258 . . . 4 (𝜑 → ¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
99 fsubbas 22163 . . . . 5 (𝑌 ∈ dom fBas → ((fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∈ (fBas‘𝑌) ↔ ((𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ⊆ 𝒫 𝑌 ∧ (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
1001, 4, 993syl 18 . . . 4 (𝜑 → ((fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∈ (fBas‘𝑌) ↔ ((𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ⊆ 𝒫 𝑌 ∧ (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
10128, 33, 98, 100mpbir3and 1335 . . 3 (𝜑 → (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∈ (fBas‘𝑌))
102 fgcl 22174 . . 3 ((fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∈ (fBas‘𝑌) → (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ∈ (Fil‘𝑌))
103101, 102syl 17 . 2 (𝜑 → (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ∈ (Fil‘𝑌))
104 unexg 7336 . . . . . 6 ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌)) → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ V)
1051, 25, 104syl2anc 584 . . . . 5 (𝜑 → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ V)
106 ssfii 8736 . . . . 5 ((𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ V → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ⊆ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
107105, 106syl 17 . . . 4 (𝜑 → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ⊆ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
108107unssad 4090 . . 3 (𝜑𝐵 ⊆ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
109 ssfg 22168 . . . 4 ((fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∈ (fBas‘𝑌) → (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))))
110101, 109syl 17 . . 3 (𝜑 → (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))))
111108, 110sstrd 3905 . 2 (𝜑𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))))
1121, 6, 7, 8fmfnfmlem4 22253 . . . . 5 (𝜑 → (𝑡𝐿 ↔ (𝑡𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡)))
113 elfm 22243 . . . . . 6 ((𝑋𝐿 ∧ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝑡 ∈ ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ↔ (𝑡𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡)))
11415, 101, 7, 113syl3anc 1364 . . . . 5 (𝜑 → (𝑡 ∈ ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ↔ (𝑡𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡)))
115112, 114bitr4d 283 . . . 4 (𝜑 → (𝑡𝐿𝑡 ∈ ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
116115eqrdv 2795 . . 3 (𝜑𝐿 = ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))))
117 eqid 2797 . . . . 5 (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
118117fmfg 22245 . . . 4 ((𝑋𝐿 ∧ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
11915, 101, 7, 118syl3anc 1364 . . 3 (𝜑 → ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
120116, 119eqtrd 2833 . 2 (𝜑𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
121 sseq2 3920 . . . 4 (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) → (𝐵𝑓𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
122 fveq2 6545 . . . . 5 (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) → ((𝑋 FilMap 𝐹)‘𝑓) = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
123122eqeq2d 2807 . . . 4 (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) → (𝐿 = ((𝑋 FilMap 𝐹)‘𝑓) ↔ 𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))))))
124121, 123anbi12d 630 . . 3 (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) → ((𝐵𝑓𝐿 = ((𝑋 FilMap 𝐹)‘𝑓)) ↔ (𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))))
125124rspcev 3561 . 2 (((𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ∈ (Fil‘𝑌) ∧ (𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))) → ∃𝑓 ∈ (Fil‘𝑌)(𝐵𝑓𝐿 = ((𝑋 FilMap 𝐹)‘𝑓)))
126103, 111, 120, 125syl12anc 833 1 (𝜑 → ∃𝑓 ∈ (Fil‘𝑌)(𝐵𝑓𝐿 = ((𝑋 FilMap 𝐹)‘𝑓)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  w3a 1080   = wceq 1525  wex 1765  wcel 2083  wne 2986  wral 3107  wrex 3108  Vcvv 3440  cun 3863  cin 3864  wss 3865  c0 4217  𝒫 cpw 4459  cmpt 5047  ccnv 5449  dom cdm 5450  ran crn 5451  cima 5453  Fun wfun 6226   Fn wfn 6227  wf 6228  ontowfo 6230  cfv 6232  (class class class)co 7023  ficfi 8727  fBascfbas 20219  filGencfg 20220  Filcfil 22141   FilMap cfm 22229
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-rep 5088  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-int 4789  df-iun 4833  df-br 4969  df-opab 5031  df-mpt 5048  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-pred 6030  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-ov 7026  df-oprab 7027  df-mpo 7028  df-om 7444  df-wrecs 7805  df-recs 7867  df-rdg 7905  df-1o 7960  df-oadd 7964  df-er 8146  df-en 8365  df-fin 8368  df-fi 8728  df-fbas 20228  df-fg 20229  df-fil 22142  df-fm 22234
This theorem is referenced by:  fmufil  22255  cnpfcf  22337
  Copyright terms: Public domain W3C validator