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

Theorem fmfnfm 21675
 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 21549 . . . . . 6 (𝐵 ∈ (fBas‘𝑌) → 𝐵 ⊆ 𝒫 𝑌)
31, 2syl 17 . . . . 5 (𝜑𝐵 ⊆ 𝒫 𝑌)
4 elfvdm 6179 . . . . . . . 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 6004 . . . . . . . . . . 11 (𝐹:𝑌𝑋𝐹 Fn 𝑌)
10 dffn4 6080 . . . . . . . . . . 11 (𝐹 Fn 𝑌𝐹:𝑌onto→ran 𝐹)
119, 10sylib 208 . . . . . . . . . 10 (𝐹:𝑌𝑋𝐹:𝑌onto→ran 𝐹)
12 foima 6079 . . . . . . . . . 10 (𝐹:𝑌onto→ran 𝐹 → (𝐹𝑌) = ran 𝐹)
137, 11, 123syl 18 . . . . . . . . 9 (𝜑 → (𝐹𝑌) = ran 𝐹)
14 filtop 21572 . . . . . . . . . . 11 (𝐿 ∈ (Fil‘𝑋) → 𝑋𝐿)
156, 14syl 17 . . . . . . . . . 10 (𝜑𝑋𝐿)
16 fgcl 21595 . . . . . . . . . . 11 (𝐵 ∈ (fBas‘𝑌) → (𝑌filGen𝐵) ∈ (Fil‘𝑌))
17 filtop 21572 . . . . . . . . . . 11 ((𝑌filGen𝐵) ∈ (Fil‘𝑌) → 𝑌 ∈ (𝑌filGen𝐵))
181, 16, 173syl 18 . . . . . . . . . 10 (𝜑𝑌 ∈ (𝑌filGen𝐵))
19 eqid 2621 . . . . . . . . . . 11 (𝑌filGen𝐵) = (𝑌filGen𝐵)
2019imaelfm 21668 . . . . . . . . . 10 (((𝑋𝐿𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑌 ∈ (𝑌filGen𝐵)) → (𝐹𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
2115, 1, 7, 18, 20syl31anc 1326 . . . . . . . . 9 (𝜑 → (𝐹𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
2213, 21eqeltrrd 2699 . . . . . . . 8 (𝜑 → ran 𝐹 ∈ ((𝑋 FilMap 𝐹)‘𝐵))
238, 22sseldd 3585 . . . . . . 7 (𝜑 → ran 𝐹𝐿)
24 rnelfmlem 21669 . . . . . . 7 (((𝑌 ∈ dom fBas ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌))
255, 6, 7, 23, 24syl31anc 1326 . . . . . 6 (𝜑 → ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌))
26 fbsspw 21549 . . . . . 6 (ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ⊆ 𝒫 𝑌)
2725, 26syl 17 . . . . 5 (𝜑 → ran (𝑥𝐿 ↦ (𝐹𝑥)) ⊆ 𝒫 𝑌)
283, 27unssd 3769 . . . 4 (𝜑 → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ⊆ 𝒫 𝑌)
29 ssun1 3756 . . . . 5 𝐵 ⊆ (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))
30 fbasne0 21547 . . . . . 6 (𝐵 ∈ (fBas‘𝑌) → 𝐵 ≠ ∅)
311, 30syl 17 . . . . 5 (𝜑𝐵 ≠ ∅)
32 ssn0 3950 . . . . 5 ((𝐵 ⊆ (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∧ 𝐵 ≠ ∅) → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ≠ ∅)
3329, 31, 32sylancr 694 . . . 4 (𝜑 → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ≠ ∅)
34 vex 3189 . . . . . . . . 9 𝑡 ∈ V
35 eqid 2621 . . . . . . . . . 10 (𝑥𝐿 ↦ (𝐹𝑥)) = (𝑥𝐿 ↦ (𝐹𝑥))
3635elrnmpt 5334 . . . . . . . . 9 (𝑡 ∈ V → (𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑡 = (𝐹𝑥)))
3734, 36ax-mp 5 . . . . . . . 8 (𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑡 = (𝐹𝑥))
38 0nelfil 21566 . . . . . . . . . . . . . 14 (𝐿 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝐿)
396, 38syl 17 . . . . . . . . . . . . 13 (𝜑 → ¬ ∅ ∈ 𝐿)
4039ad2antrr 761 . . . . . . . . . . . 12 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → ¬ ∅ ∈ 𝐿)
416adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑠𝐵) → 𝐿 ∈ (Fil‘𝑋))
428adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑠𝐵) → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)
4315, 1, 73jca 1240 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋𝐿𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋))
4443adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠𝐵) → (𝑋𝐿𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋))
45 ssfg 21589 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ (fBas‘𝑌) → 𝐵 ⊆ (𝑌filGen𝐵))
461, 45syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ⊆ (𝑌filGen𝐵))
4746sselda 3584 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠𝐵) → 𝑠 ∈ (𝑌filGen𝐵))
4819imaelfm 21668 . . . . . . . . . . . . . . . . 17 (((𝑋𝐿𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑠 ∈ (𝑌filGen𝐵)) → (𝐹𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
4944, 47, 48syl2anc 692 . . . . . . . . . . . . . . . 16 ((𝜑𝑠𝐵) → (𝐹𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
5042, 49sseldd 3585 . . . . . . . . . . . . . . 15 ((𝜑𝑠𝐵) → (𝐹𝑠) ∈ 𝐿)
5141, 50jca 554 . . . . . . . . . . . . . 14 ((𝜑𝑠𝐵) → (𝐿 ∈ (Fil‘𝑋) ∧ (𝐹𝑠) ∈ 𝐿))
52 filin 21571 . . . . . . . . . . . . . . 15 ((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹𝑠) ∈ 𝐿𝑥𝐿) → ((𝐹𝑠) ∩ 𝑥) ∈ 𝐿)
53523expa 1262 . . . . . . . . . . . . . 14 (((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹𝑠) ∈ 𝐿) ∧ 𝑥𝐿) → ((𝐹𝑠) ∩ 𝑥) ∈ 𝐿)
5451, 53sylan 488 . . . . . . . . . . . . 13 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → ((𝐹𝑠) ∩ 𝑥) ∈ 𝐿)
55 eleq1 2686 . . . . . . . . . . . . 13 (((𝐹𝑠) ∩ 𝑥) = ∅ → (((𝐹𝑠) ∩ 𝑥) ∈ 𝐿 ↔ ∅ ∈ 𝐿))
5654, 55syl5ibcom 235 . . . . . . . . . . . 12 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (((𝐹𝑠) ∩ 𝑥) = ∅ → ∅ ∈ 𝐿))
5740, 56mtod 189 . . . . . . . . . . 11 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → ¬ ((𝐹𝑠) ∩ 𝑥) = ∅)
58 neq0 3908 . . . . . . . . . . . 12 (¬ ((𝐹𝑠) ∩ 𝑥) = ∅ ↔ ∃𝑡 𝑡 ∈ ((𝐹𝑠) ∩ 𝑥))
59 elin 3776 . . . . . . . . . . . . . 14 (𝑡 ∈ ((𝐹𝑠) ∩ 𝑥) ↔ (𝑡 ∈ (𝐹𝑠) ∧ 𝑡𝑥))
60 ffun 6007 . . . . . . . . . . . . . . . . . 18 (𝐹:𝑌𝑋 → Fun 𝐹)
61 fvelima 6207 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝐹𝑡 ∈ (𝐹𝑠)) → ∃𝑦𝑠 (𝐹𝑦) = 𝑡)
6261ex 450 . . . . . . . . . . . . . . . . . 18 (Fun 𝐹 → (𝑡 ∈ (𝐹𝑠) → ∃𝑦𝑠 (𝐹𝑦) = 𝑡))
637, 60, 623syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑡 ∈ (𝐹𝑠) → ∃𝑦𝑠 (𝐹𝑦) = 𝑡))
6463ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (𝑡 ∈ (𝐹𝑠) → ∃𝑦𝑠 (𝐹𝑦) = 𝑡))
657, 60syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → Fun 𝐹)
6665ad3antrrr 765 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑠𝐵) ∧ 𝑥𝐿) ∧ 𝑦𝑠) → Fun 𝐹)
67 fbelss 21550 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐵 ∈ (fBas‘𝑌) ∧ 𝑠𝐵) → 𝑠𝑌)
681, 67sylan 488 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑠𝐵) → 𝑠𝑌)
69 fdm 6010 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹:𝑌𝑋 → dom 𝐹 = 𝑌)
707, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → dom 𝐹 = 𝑌)
7170adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑠𝐵) → dom 𝐹 = 𝑌)
7268, 71sseqtr4d 3623 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑠𝐵) → 𝑠 ⊆ dom 𝐹)
7372adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → 𝑠 ⊆ dom 𝐹)
7473sselda 3584 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑠𝐵) ∧ 𝑥𝐿) ∧ 𝑦𝑠) → 𝑦 ∈ dom 𝐹)
75 fvimacnv 6290 . . . . . . . . . . . . . . . . . . . 20 ((Fun 𝐹𝑦 ∈ dom 𝐹) → ((𝐹𝑦) ∈ 𝑥𝑦 ∈ (𝐹𝑥)))
7666, 74, 75syl2anc 692 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑠𝐵) ∧ 𝑥𝐿) ∧ 𝑦𝑠) → ((𝐹𝑦) ∈ 𝑥𝑦 ∈ (𝐹𝑥)))
77 inelcm 4006 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦𝑠𝑦 ∈ (𝐹𝑥)) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅)
7877ex 450 . . . . . . . . . . . . . . . . . . . 20 (𝑦𝑠 → (𝑦 ∈ (𝐹𝑥) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
7978adantl 482 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑠𝐵) ∧ 𝑥𝐿) ∧ 𝑦𝑠) → (𝑦 ∈ (𝐹𝑥) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
8076, 79sylbid 230 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑠𝐵) ∧ 𝑥𝐿) ∧ 𝑦𝑠) → ((𝐹𝑦) ∈ 𝑥 → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
81 eleq1 2686 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑦) = 𝑡 → ((𝐹𝑦) ∈ 𝑥𝑡𝑥))
8281imbi1d 331 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑦) = 𝑡 → (((𝐹𝑦) ∈ 𝑥 → (𝑠 ∩ (𝐹𝑥)) ≠ ∅) ↔ (𝑡𝑥 → (𝑠 ∩ (𝐹𝑥)) ≠ ∅)))
8380, 82syl5ibcom 235 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑠𝐵) ∧ 𝑥𝐿) ∧ 𝑦𝑠) → ((𝐹𝑦) = 𝑡 → (𝑡𝑥 → (𝑠 ∩ (𝐹𝑥)) ≠ ∅)))
8483rexlimdva 3024 . . . . . . . . . . . . . . . 16 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (∃𝑦𝑠 (𝐹𝑦) = 𝑡 → (𝑡𝑥 → (𝑠 ∩ (𝐹𝑥)) ≠ ∅)))
8564, 84syld 47 . . . . . . . . . . . . . . 15 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (𝑡 ∈ (𝐹𝑠) → (𝑡𝑥 → (𝑠 ∩ (𝐹𝑥)) ≠ ∅)))
8685impd 447 . . . . . . . . . . . . . 14 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → ((𝑡 ∈ (𝐹𝑠) ∧ 𝑡𝑥) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
8759, 86syl5bi 232 . . . . . . . . . . . . 13 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (𝑡 ∈ ((𝐹𝑠) ∩ 𝑥) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
8887exlimdv 1858 . . . . . . . . . . . 12 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (∃𝑡 𝑡 ∈ ((𝐹𝑠) ∩ 𝑥) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
8958, 88syl5bi 232 . . . . . . . . . . 11 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (¬ ((𝐹𝑠) ∩ 𝑥) = ∅ → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
9057, 89mpd 15 . . . . . . . . . 10 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅)
91 ineq2 3788 . . . . . . . . . . 11 (𝑡 = (𝐹𝑥) → (𝑠𝑡) = (𝑠 ∩ (𝐹𝑥)))
9291neeq1d 2849 . . . . . . . . . 10 (𝑡 = (𝐹𝑥) → ((𝑠𝑡) ≠ ∅ ↔ (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
9390, 92syl5ibrcom 237 . . . . . . . . 9 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (𝑡 = (𝐹𝑥) → (𝑠𝑡) ≠ ∅))
9493rexlimdva 3024 . . . . . . . 8 ((𝜑𝑠𝐵) → (∃𝑥𝐿 𝑡 = (𝐹𝑥) → (𝑠𝑡) ≠ ∅))
9537, 94syl5bi 232 . . . . . . 7 ((𝜑𝑠𝐵) → (𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) → (𝑠𝑡) ≠ ∅))
9695expimpd 628 . . . . . 6 (𝜑 → ((𝑠𝐵𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))) → (𝑠𝑡) ≠ ∅))
9796ralrimivv 2964 . . . . 5 (𝜑 → ∀𝑠𝐵𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝑠𝑡) ≠ ∅)
98 fbunfip 21586 . . . . . 6 ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌)) → (¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ↔ ∀𝑠𝐵𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝑠𝑡) ≠ ∅))
991, 25, 98syl2anc 692 . . . . 5 (𝜑 → (¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ↔ ∀𝑠𝐵𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝑠𝑡) ≠ ∅))
10097, 99mpbird 247 . . . 4 (𝜑 → ¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
101 fsubbas 21584 . . . . 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 1243 . . 3 (𝜑 → (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∈ (fBas‘𝑌))
104 fgcl 21595 . . 3 ((fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∈ (fBas‘𝑌) → (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ∈ (Fil‘𝑌))
105103, 104syl 17 . 2 (𝜑 → (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ∈ (Fil‘𝑌))
106 unexg 6915 . . . . . 6 ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌)) → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ V)
1071, 25, 106syl2anc 692 . . . . 5 (𝜑 → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ V)
108 ssfii 8272 . . . . 5 ((𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ V → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ⊆ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
109107, 108syl 17 . . . 4 (𝜑 → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ⊆ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
110109unssad 3770 . . 3 (𝜑𝐵 ⊆ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
111 ssfg 21589 . . . 4 ((fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∈ (fBas‘𝑌) → (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))))
112103, 111syl 17 . . 3 (𝜑 → (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))))
113110, 112sstrd 3594 . 2 (𝜑𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))))
1141, 6, 7, 8fmfnfmlem4 21674 . . . . 5 (𝜑 → (𝑡𝐿 ↔ (𝑡𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡)))
115 elfm 21664 . . . . . 6 ((𝑋𝐿 ∧ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝑡 ∈ ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ↔ (𝑡𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡)))
11615, 103, 7, 115syl3anc 1323 . . . . 5 (𝜑 → (𝑡 ∈ ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ↔ (𝑡𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡)))
117114, 116bitr4d 271 . . . 4 (𝜑 → (𝑡𝐿𝑡 ∈ ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
118117eqrdv 2619 . . 3 (𝜑𝐿 = ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))))
119 eqid 2621 . . . . 5 (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
120119fmfg 21666 . . . 4 ((𝑋𝐿 ∧ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
12115, 103, 7, 120syl3anc 1323 . . 3 (𝜑 → ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
122118, 121eqtrd 2655 . 2 (𝜑𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
123 sseq2 3608 . . . 4 (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) → (𝐵𝑓𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
124 fveq2 6150 . . . . 5 (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) → ((𝑋 FilMap 𝐹)‘𝑓) = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
125124eqeq2d 2631 . . . 4 (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) → (𝐿 = ((𝑋 FilMap 𝐹)‘𝑓) ↔ 𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))))))
126123, 125anbi12d 746 . . 3 (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) → ((𝐵𝑓𝐿 = ((𝑋 FilMap 𝐹)‘𝑓)) ↔ (𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))))
127126rspcev 3295 . 2 (((𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ∈ (Fil‘𝑌) ∧ (𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))) → ∃𝑓 ∈ (Fil‘𝑌)(𝐵𝑓𝐿 = ((𝑋 FilMap 𝐹)‘𝑓)))
128105, 113, 122, 127syl12anc 1321 1 (𝜑 → ∃𝑓 ∈ (Fil‘𝑌)(𝐵𝑓𝐿 = ((𝑋 FilMap 𝐹)‘𝑓)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480  ∃wex 1701   ∈ wcel 1987   ≠ wne 2790  ∀wral 2907  ∃wrex 2908  Vcvv 3186   ∪ cun 3554   ∩ cin 3555   ⊆ wss 3556  ∅c0 3893  𝒫 cpw 4132   ↦ cmpt 4675  ◡ccnv 5075  dom cdm 5076  ran crn 5077   “ cima 5079  Fun wfun 5843   Fn wfn 5844  ⟶wf 5845  –onto→wfo 5847  ‘cfv 5849  (class class class)co 6607  ficfi 8263  fBascfbas 19656  filGencfg 19657  Filcfil 21562   FilMap cfm 21650 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4733  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-pss 3572  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-tp 4155  df-op 4157  df-uni 4405  df-int 4443  df-iun 4489  df-br 4616  df-opab 4676  df-mpt 4677  df-tr 4715  df-eprel 4987  df-id 4991  df-po 4997  df-so 4998  df-fr 5035  df-we 5037  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-pred 5641  df-ord 5687  df-on 5688  df-lim 5689  df-suc 5690  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-om 7016  df-wrecs 7355  df-recs 7416  df-rdg 7454  df-1o 7508  df-oadd 7512  df-er 7690  df-en 7903  df-fin 7906  df-fi 8264  df-fbas 19665  df-fg 19666  df-fil 21563  df-fm 21655 This theorem is referenced by:  fmufil  21676  cnpfcf  21758
 Copyright terms: Public domain W3C validator