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

Theorem fmfnfm 22041
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 21915 . . . . . 6 (𝐵 ∈ (fBas‘𝑌) → 𝐵 ⊆ 𝒫 𝑌)
31, 2syl 17 . . . . 5 (𝜑𝐵 ⊆ 𝒫 𝑌)
4 elfvdm 6407 . . . . . . . 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 6223 . . . . . . . . . . 11 (𝐹:𝑌𝑋𝐹 Fn 𝑌)
10 dffn4 6304 . . . . . . . . . . 11 (𝐹 Fn 𝑌𝐹:𝑌onto→ran 𝐹)
119, 10sylib 209 . . . . . . . . . 10 (𝐹:𝑌𝑋𝐹:𝑌onto→ran 𝐹)
12 foima 6303 . . . . . . . . . 10 (𝐹:𝑌onto→ran 𝐹 → (𝐹𝑌) = ran 𝐹)
137, 11, 123syl 18 . . . . . . . . 9 (𝜑 → (𝐹𝑌) = ran 𝐹)
14 filtop 21938 . . . . . . . . . . 11 (𝐿 ∈ (Fil‘𝑋) → 𝑋𝐿)
156, 14syl 17 . . . . . . . . . 10 (𝜑𝑋𝐿)
16 fgcl 21961 . . . . . . . . . . 11 (𝐵 ∈ (fBas‘𝑌) → (𝑌filGen𝐵) ∈ (Fil‘𝑌))
17 filtop 21938 . . . . . . . . . . 11 ((𝑌filGen𝐵) ∈ (Fil‘𝑌) → 𝑌 ∈ (𝑌filGen𝐵))
181, 16, 173syl 18 . . . . . . . . . 10 (𝜑𝑌 ∈ (𝑌filGen𝐵))
19 eqid 2765 . . . . . . . . . . 11 (𝑌filGen𝐵) = (𝑌filGen𝐵)
2019imaelfm 22034 . . . . . . . . . 10 (((𝑋𝐿𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑌 ∈ (𝑌filGen𝐵)) → (𝐹𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
2115, 1, 7, 18, 20syl31anc 1492 . . . . . . . . 9 (𝜑 → (𝐹𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
2213, 21eqeltrrd 2845 . . . . . . . 8 (𝜑 → ran 𝐹 ∈ ((𝑋 FilMap 𝐹)‘𝐵))
238, 22sseldd 3762 . . . . . . 7 (𝜑 → ran 𝐹𝐿)
24 rnelfmlem 22035 . . . . . . 7 (((𝑌 ∈ dom fBas ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌𝑋) ∧ ran 𝐹𝐿) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌))
255, 6, 7, 23, 24syl31anc 1492 . . . . . 6 (𝜑 → ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌))
26 fbsspw 21915 . . . . . 6 (ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌) → ran (𝑥𝐿 ↦ (𝐹𝑥)) ⊆ 𝒫 𝑌)
2725, 26syl 17 . . . . 5 (𝜑 → ran (𝑥𝐿 ↦ (𝐹𝑥)) ⊆ 𝒫 𝑌)
283, 27unssd 3951 . . . 4 (𝜑 → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ⊆ 𝒫 𝑌)
29 ssun1 3938 . . . . 5 𝐵 ⊆ (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))
30 fbasne0 21913 . . . . . 6 (𝐵 ∈ (fBas‘𝑌) → 𝐵 ≠ ∅)
311, 30syl 17 . . . . 5 (𝜑𝐵 ≠ ∅)
32 ssn0 4138 . . . . 5 ((𝐵 ⊆ (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∧ 𝐵 ≠ ∅) → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ≠ ∅)
3329, 31, 32sylancr 581 . . . 4 (𝜑 → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ≠ ∅)
34 vex 3353 . . . . . . . . 9 𝑡 ∈ V
35 eqid 2765 . . . . . . . . . 10 (𝑥𝐿 ↦ (𝐹𝑥)) = (𝑥𝐿 ↦ (𝐹𝑥))
3635elrnmpt 5541 . . . . . . . . 9 (𝑡 ∈ V → (𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑡 = (𝐹𝑥)))
3734, 36ax-mp 5 . . . . . . . 8 (𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) ↔ ∃𝑥𝐿 𝑡 = (𝐹𝑥))
38 0nelfil 21932 . . . . . . . . . . . . . 14 (𝐿 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝐿)
396, 38syl 17 . . . . . . . . . . . . 13 (𝜑 → ¬ ∅ ∈ 𝐿)
4039ad2antrr 717 . . . . . . . . . . . 12 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → ¬ ∅ ∈ 𝐿)
416adantr 472 . . . . . . . . . . . . . . 15 ((𝜑𝑠𝐵) → 𝐿 ∈ (Fil‘𝑋))
428adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑠𝐵) → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)
4315, 1, 73jca 1158 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋𝐿𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋))
4443adantr 472 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠𝐵) → (𝑋𝐿𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋))
45 ssfg 21955 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ (fBas‘𝑌) → 𝐵 ⊆ (𝑌filGen𝐵))
461, 45syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ⊆ (𝑌filGen𝐵))
4746sselda 3761 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠𝐵) → 𝑠 ∈ (𝑌filGen𝐵))
4819imaelfm 22034 . . . . . . . . . . . . . . . . 17 (((𝑋𝐿𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) ∧ 𝑠 ∈ (𝑌filGen𝐵)) → (𝐹𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
4944, 47, 48syl2anc 579 . . . . . . . . . . . . . . . 16 ((𝜑𝑠𝐵) → (𝐹𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
5042, 49sseldd 3762 . . . . . . . . . . . . . . 15 ((𝜑𝑠𝐵) → (𝐹𝑠) ∈ 𝐿)
5141, 50jca 507 . . . . . . . . . . . . . 14 ((𝜑𝑠𝐵) → (𝐿 ∈ (Fil‘𝑋) ∧ (𝐹𝑠) ∈ 𝐿))
52 filin 21937 . . . . . . . . . . . . . . 15 ((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹𝑠) ∈ 𝐿𝑥𝐿) → ((𝐹𝑠) ∩ 𝑥) ∈ 𝐿)
53523expa 1147 . . . . . . . . . . . . . 14 (((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹𝑠) ∈ 𝐿) ∧ 𝑥𝐿) → ((𝐹𝑠) ∩ 𝑥) ∈ 𝐿)
5451, 53sylan 575 . . . . . . . . . . . . 13 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → ((𝐹𝑠) ∩ 𝑥) ∈ 𝐿)
55 eleq1 2832 . . . . . . . . . . . . 13 (((𝐹𝑠) ∩ 𝑥) = ∅ → (((𝐹𝑠) ∩ 𝑥) ∈ 𝐿 ↔ ∅ ∈ 𝐿))
5654, 55syl5ibcom 236 . . . . . . . . . . . 12 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (((𝐹𝑠) ∩ 𝑥) = ∅ → ∅ ∈ 𝐿))
5740, 56mtod 189 . . . . . . . . . . 11 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → ¬ ((𝐹𝑠) ∩ 𝑥) = ∅)
58 neq0 4094 . . . . . . . . . . . 12 (¬ ((𝐹𝑠) ∩ 𝑥) = ∅ ↔ ∃𝑡 𝑡 ∈ ((𝐹𝑠) ∩ 𝑥))
59 elin 3958 . . . . . . . . . . . . . 14 (𝑡 ∈ ((𝐹𝑠) ∩ 𝑥) ↔ (𝑡 ∈ (𝐹𝑠) ∧ 𝑡𝑥))
60 ffun 6226 . . . . . . . . . . . . . . . . . 18 (𝐹:𝑌𝑋 → Fun 𝐹)
61 fvelima 6437 . . . . . . . . . . . . . . . . . . 19 ((Fun 𝐹𝑡 ∈ (𝐹𝑠)) → ∃𝑦𝑠 (𝐹𝑦) = 𝑡)
6261ex 401 . . . . . . . . . . . . . . . . . 18 (Fun 𝐹 → (𝑡 ∈ (𝐹𝑠) → ∃𝑦𝑠 (𝐹𝑦) = 𝑡))
637, 60, 623syl 18 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑡 ∈ (𝐹𝑠) → ∃𝑦𝑠 (𝐹𝑦) = 𝑡))
6463ad2antrr 717 . . . . . . . . . . . . . . . 16 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (𝑡 ∈ (𝐹𝑠) → ∃𝑦𝑠 (𝐹𝑦) = 𝑡))
657, 60syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → Fun 𝐹)
6665ad3antrrr 721 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑠𝐵) ∧ 𝑥𝐿) ∧ 𝑦𝑠) → Fun 𝐹)
67 fbelss 21916 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐵 ∈ (fBas‘𝑌) ∧ 𝑠𝐵) → 𝑠𝑌)
681, 67sylan 575 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑠𝐵) → 𝑠𝑌)
697fdmd 6232 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → dom 𝐹 = 𝑌)
7069adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑠𝐵) → dom 𝐹 = 𝑌)
7168, 70sseqtr4d 3802 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑠𝐵) → 𝑠 ⊆ dom 𝐹)
7271adantr 472 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → 𝑠 ⊆ dom 𝐹)
7372sselda 3761 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑠𝐵) ∧ 𝑥𝐿) ∧ 𝑦𝑠) → 𝑦 ∈ dom 𝐹)
74 fvimacnv 6522 . . . . . . . . . . . . . . . . . . . 20 ((Fun 𝐹𝑦 ∈ dom 𝐹) → ((𝐹𝑦) ∈ 𝑥𝑦 ∈ (𝐹𝑥)))
7566, 73, 74syl2anc 579 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑠𝐵) ∧ 𝑥𝐿) ∧ 𝑦𝑠) → ((𝐹𝑦) ∈ 𝑥𝑦 ∈ (𝐹𝑥)))
76 inelcm 4193 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦𝑠𝑦 ∈ (𝐹𝑥)) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅)
7776ex 401 . . . . . . . . . . . . . . . . . . . 20 (𝑦𝑠 → (𝑦 ∈ (𝐹𝑥) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
7877adantl 473 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑠𝐵) ∧ 𝑥𝐿) ∧ 𝑦𝑠) → (𝑦 ∈ (𝐹𝑥) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
7975, 78sylbid 231 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑠𝐵) ∧ 𝑥𝐿) ∧ 𝑦𝑠) → ((𝐹𝑦) ∈ 𝑥 → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
80 eleq1 2832 . . . . . . . . . . . . . . . . . . 19 ((𝐹𝑦) = 𝑡 → ((𝐹𝑦) ∈ 𝑥𝑡𝑥))
8180imbi1d 332 . . . . . . . . . . . . . . . . . 18 ((𝐹𝑦) = 𝑡 → (((𝐹𝑦) ∈ 𝑥 → (𝑠 ∩ (𝐹𝑥)) ≠ ∅) ↔ (𝑡𝑥 → (𝑠 ∩ (𝐹𝑥)) ≠ ∅)))
8279, 81syl5ibcom 236 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑠𝐵) ∧ 𝑥𝐿) ∧ 𝑦𝑠) → ((𝐹𝑦) = 𝑡 → (𝑡𝑥 → (𝑠 ∩ (𝐹𝑥)) ≠ ∅)))
8382rexlimdva 3178 . . . . . . . . . . . . . . . 16 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (∃𝑦𝑠 (𝐹𝑦) = 𝑡 → (𝑡𝑥 → (𝑠 ∩ (𝐹𝑥)) ≠ ∅)))
8464, 83syld 47 . . . . . . . . . . . . . . 15 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (𝑡 ∈ (𝐹𝑠) → (𝑡𝑥 → (𝑠 ∩ (𝐹𝑥)) ≠ ∅)))
8584impd 398 . . . . . . . . . . . . . 14 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → ((𝑡 ∈ (𝐹𝑠) ∧ 𝑡𝑥) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
8659, 85syl5bi 233 . . . . . . . . . . . . 13 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (𝑡 ∈ ((𝐹𝑠) ∩ 𝑥) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
8786exlimdv 2028 . . . . . . . . . . . 12 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (∃𝑡 𝑡 ∈ ((𝐹𝑠) ∩ 𝑥) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
8858, 87syl5bi 233 . . . . . . . . . . 11 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (¬ ((𝐹𝑠) ∩ 𝑥) = ∅ → (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
8957, 88mpd 15 . . . . . . . . . 10 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (𝑠 ∩ (𝐹𝑥)) ≠ ∅)
90 ineq2 3970 . . . . . . . . . . 11 (𝑡 = (𝐹𝑥) → (𝑠𝑡) = (𝑠 ∩ (𝐹𝑥)))
9190neeq1d 2996 . . . . . . . . . 10 (𝑡 = (𝐹𝑥) → ((𝑠𝑡) ≠ ∅ ↔ (𝑠 ∩ (𝐹𝑥)) ≠ ∅))
9289, 91syl5ibrcom 238 . . . . . . . . 9 (((𝜑𝑠𝐵) ∧ 𝑥𝐿) → (𝑡 = (𝐹𝑥) → (𝑠𝑡) ≠ ∅))
9392rexlimdva 3178 . . . . . . . 8 ((𝜑𝑠𝐵) → (∃𝑥𝐿 𝑡 = (𝐹𝑥) → (𝑠𝑡) ≠ ∅))
9437, 93syl5bi 233 . . . . . . 7 ((𝜑𝑠𝐵) → (𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥)) → (𝑠𝑡) ≠ ∅))
9594expimpd 445 . . . . . 6 (𝜑 → ((𝑠𝐵𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))) → (𝑠𝑡) ≠ ∅))
9695ralrimivv 3117 . . . . 5 (𝜑 → ∀𝑠𝐵𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝑠𝑡) ≠ ∅)
97 fbunfip 21952 . . . . . 6 ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌)) → (¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ↔ ∀𝑠𝐵𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝑠𝑡) ≠ ∅))
981, 25, 97syl2anc 579 . . . . 5 (𝜑 → (¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ↔ ∀𝑠𝐵𝑡 ∈ ran (𝑥𝐿 ↦ (𝐹𝑥))(𝑠𝑡) ≠ ∅))
9996, 98mpbird 248 . . . 4 (𝜑 → ¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
100 fsubbas 21950 . . . . 5 (𝑌 ∈ dom fBas → ((fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∈ (fBas‘𝑌) ↔ ((𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ⊆ 𝒫 𝑌 ∧ (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
1011, 4, 1003syl 18 . . . 4 (𝜑 → ((fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∈ (fBas‘𝑌) ↔ ((𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ⊆ 𝒫 𝑌 ∧ (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
10228, 33, 99, 101mpbir3and 1442 . . 3 (𝜑 → (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∈ (fBas‘𝑌))
103 fgcl 21961 . . 3 ((fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∈ (fBas‘𝑌) → (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ∈ (Fil‘𝑌))
104102, 103syl 17 . 2 (𝜑 → (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ∈ (Fil‘𝑌))
105 unexg 7157 . . . . . 6 ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥𝐿 ↦ (𝐹𝑥)) ∈ (fBas‘𝑌)) → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ V)
1061, 25, 105syl2anc 579 . . . . 5 (𝜑 → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ V)
107 ssfii 8532 . . . . 5 ((𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ∈ V → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ⊆ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
108106, 107syl 17 . . . 4 (𝜑 → (𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))) ⊆ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
109108unssad 3952 . . 3 (𝜑𝐵 ⊆ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
110 ssfg 21955 . . . 4 ((fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∈ (fBas‘𝑌) → (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))))
111102, 110syl 17 . . 3 (𝜑 → (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))))
112109, 111sstrd 3771 . 2 (𝜑𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))))
1131, 6, 7, 8fmfnfmlem4 22040 . . . . 5 (𝜑 → (𝑡𝐿 ↔ (𝑡𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡)))
114 elfm 22030 . . . . . 6 ((𝑋𝐿 ∧ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → (𝑡 ∈ ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ↔ (𝑡𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡)))
11515, 102, 7, 114syl3anc 1490 . . . . 5 (𝜑 → (𝑡 ∈ ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ↔ (𝑡𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))(𝐹𝑠) ⊆ 𝑡)))
116113, 115bitr4d 273 . . . 4 (𝜑 → (𝑡𝐿𝑡 ∈ ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
117116eqrdv 2763 . . 3 (𝜑𝐿 = ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))))
118 eqid 2765 . . . . 5 (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))
119118fmfg 22032 . . . 4 ((𝑋𝐿 ∧ (fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))) ∈ (fBas‘𝑌) ∧ 𝐹:𝑌𝑋) → ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
12015, 102, 7, 119syl3anc 1490 . . 3 (𝜑 → ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
121117, 120eqtrd 2799 . 2 (𝜑𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
122 sseq2 3787 . . . 4 (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) → (𝐵𝑓𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
123 fveq2 6375 . . . . 5 (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) → ((𝑋 FilMap 𝐹)‘𝑓) = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))
124123eqeq2d 2775 . . . 4 (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) → (𝐿 = ((𝑋 FilMap 𝐹)‘𝑓) ↔ 𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))))))
125122, 124anbi12d 624 . . 3 (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) → ((𝐵𝑓𝐿 = ((𝑋 FilMap 𝐹)‘𝑓)) ↔ (𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))))
126125rspcev 3461 . 2 (((𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ∈ (Fil‘𝑌) ∧ (𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥))))) ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥𝐿 ↦ (𝐹𝑥)))))))) → ∃𝑓 ∈ (Fil‘𝑌)(𝐵𝑓𝐿 = ((𝑋 FilMap 𝐹)‘𝑓)))
127104, 112, 121, 126syl12anc 865 1 (𝜑 → ∃𝑓 ∈ (Fil‘𝑌)(𝐵𝑓𝐿 = ((𝑋 FilMap 𝐹)‘𝑓)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wex 1874  wcel 2155  wne 2937  wral 3055  wrex 3056  Vcvv 3350  cun 3730  cin 3731  wss 3732  c0 4079  𝒫 cpw 4315  cmpt 4888  ccnv 5276  dom cdm 5277  ran crn 5278  cima 5280  Fun wfun 6062   Fn wfn 6063  wf 6064  ontowfo 6066  cfv 6068  (class class class)co 6842  ficfi 8523  fBascfbas 20007  filGencfg 20008  Filcfil 21928   FilMap cfm 22016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-int 4634  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-om 7264  df-wrecs 7610  df-recs 7672  df-rdg 7710  df-1o 7764  df-oadd 7768  df-er 7947  df-en 8161  df-fin 8164  df-fi 8524  df-fbas 20016  df-fg 20017  df-fil 21929  df-fm 22021
This theorem is referenced by:  fmufil  22042  cnpfcf  22124
  Copyright terms: Public domain W3C validator