fmfnfm - Metamath Proof Explorer

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

Theorem fmfnfm 21762

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.

Step	Hyp	Ref	Expression
1		fmfnfm.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌))
2		fbsspw 21636	. . . . . 6 ⊢ (𝐵 ∈ (fBas‘𝑌) → 𝐵 ⊆ 𝒫 𝑌)
3	1, 2	syl 17	. . . . 5 ⊢ (𝜑 → 𝐵 ⊆ 𝒫 𝑌)
4		elfvdm 6220	. . . . . . . 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 6045	. . . . . . . . . . 11 ⊢ (𝐹:𝑌⟶𝑋 → 𝐹 Fn 𝑌)
10		dffn4 6121	. . . . . . . . . . 11 ⊢ (𝐹 Fn 𝑌 ↔ 𝐹:𝑌–onto→ran 𝐹)
11	9, 10	sylib 208	. . . . . . . . . 10 ⊢ (𝐹:𝑌⟶𝑋 → 𝐹:𝑌–onto→ran 𝐹)
12		foima 6120	. . . . . . . . . 10 ⊢ (𝐹:𝑌–onto→ran 𝐹 → (𝐹 “ 𝑌) = ran 𝐹)
13	7, 11, 12	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 “ 𝑌) = ran 𝐹)
14		filtop 21659	. . . . . . . . . . 11 ⊢ (𝐿 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐿)
15	6, 14	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ 𝐿)
16		fgcl 21682	. . . . . . . . . . 11 ⊢ (𝐵 ∈ (fBas‘𝑌) → (𝑌filGen𝐵) ∈ (Fil‘𝑌))
17		filtop 21659	. . . . . . . . . . 11 ⊢ ((𝑌filGen𝐵) ∈ (Fil‘𝑌) → 𝑌 ∈ (𝑌filGen𝐵))
18	1, 16, 17	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ∈ (𝑌filGen𝐵))
19		eqid 2622	. . . . . . . . . . 11 ⊢ (𝑌filGen𝐵) = (𝑌filGen𝐵)
20	19	imaelfm 21755	. . . . . . . . . 10 ⊢ (((𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑌 ∈ (𝑌filGen𝐵)) → (𝐹 “ 𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
21	15, 1, 7, 18, 20	syl31anc 1329	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 “ 𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
22	13, 21	eqeltrrd 2702	. . . . . . . 8 ⊢ (𝜑 → ran 𝐹 ∈ ((𝑋 FilMap 𝐹)‘𝐵))
23	8, 22	sseldd 3604	. . . . . . 7 ⊢ (𝜑 → ran 𝐹 ∈ 𝐿)
24		rnelfmlem 21756	. . . . . . 7 ⊢ (((𝑌 ∈ dom fBas ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌))
25	5, 6, 7, 23, 24	syl31anc 1329	. . . . . 6 ⊢ (𝜑 → ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌))
26		fbsspw 21636	. . . . . 6 ⊢ (ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌) → ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ⊆ 𝒫 𝑌)
27	25, 26	syl 17	. . . . 5 ⊢ (𝜑 → ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ⊆ 𝒫 𝑌)
28	3, 27	unssd 3789	. . . 4 ⊢ (𝜑 → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ⊆ 𝒫 𝑌)
29		ssun1 3776	. . . . 5 ⊢ 𝐵 ⊆ (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))
30		fbasne0 21634	. . . . . 6 ⊢ (𝐵 ∈ (fBas‘𝑌) → 𝐵 ≠ ∅)
31	1, 30	syl 17	. . . . 5 ⊢ (𝜑 → 𝐵 ≠ ∅)
32		ssn0 3976	. . . . 5 ⊢ ((𝐵 ⊆ (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ∧ 𝐵 ≠ ∅) → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ≠ ∅)
33	29, 31, 32	sylancr 695	. . . 4 ⊢ (𝜑 → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ≠ ∅)
34		vex 3203	. . . . . . . . 9 ⊢ 𝑡 ∈ V
35		eqid 2622	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) = (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))
36	35	elrnmpt 5372	. . . . . . . . 9 ⊢ (𝑡 ∈ V → (𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑡 = (^◡𝐹 “ 𝑥)))
37	34, 36	ax-mp 5	. . . . . . . 8 ⊢ (𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑡 = (^◡𝐹 “ 𝑥))
38		0nelfil 21653	. . . . . . . . . . . . . 14 ⊢ (𝐿 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝐿)
39	6, 38	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ ∅ ∈ 𝐿)
40	39	ad2antrr 762	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → ¬ ∅ ∈ 𝐿)
41	6	adantr 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝐿 ∈ (Fil‘𝑋))
42	8	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)
43	15, 1, 7	3jca 1242	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋))
44	43	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋))
45		ssfg 21676	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ (fBas‘𝑌) → 𝐵 ⊆ (𝑌filGen𝐵))
46	1, 45	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ⊆ (𝑌filGen𝐵))
47	46	sselda 3603	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ∈ (𝑌filGen𝐵))
48	19	imaelfm 21755	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑠 ∈ (𝑌filGen𝐵)) → (𝐹 “ 𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
49	44, 47, 48	syl2anc 693	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝐹 “ 𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
50	42, 49	sseldd 3604	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝐹 “ 𝑠) ∈ 𝐿)
51	41, 50	jca 554	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝐿 ∈ (Fil‘𝑋) ∧ (𝐹 “ 𝑠) ∈ 𝐿))
52		filin 21658	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹 “ 𝑠) ∈ 𝐿 ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿)
53	52	3expa 1265	. . . . . . . . . . . . . 14 ⊢ (((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹 “ 𝑠) ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿)
54	51, 53	sylan 488	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿)
55		eleq1 2689	. . . . . . . . . . . . 13 ⊢ (((𝐹 “ 𝑠) ∩ 𝑥) = ∅ → (((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿 ↔ ∅ ∈ 𝐿))
56	54, 55	syl5ibcom 235	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (((𝐹 “ 𝑠) ∩ 𝑥) = ∅ → ∅ ∈ 𝐿))
57	40, 56	mtod 189	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → ¬ ((𝐹 “ 𝑠) ∩ 𝑥) = ∅)
58		neq0 3930	. . . . . . . . . . . 12 ⊢ (¬ ((𝐹 “ 𝑠) ∩ 𝑥) = ∅ ↔ ∃𝑡 𝑡 ∈ ((𝐹 “ 𝑠) ∩ 𝑥))
59		elin 3796	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ ((𝐹 “ 𝑠) ∩ 𝑥) ↔ (𝑡 ∈ (𝐹 “ 𝑠) ∧ 𝑡 ∈ 𝑥))
60		ffun 6048	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹:𝑌⟶𝑋 → Fun 𝐹)
61		fvelima 6248	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝐹 ∧ 𝑡 ∈ (𝐹 “ 𝑠)) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑡)
62	61	ex 450	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun 𝐹 → (𝑡 ∈ (𝐹 “ 𝑠) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑡))
63	7, 60, 62	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑡 ∈ (𝐹 “ 𝑠) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑡))
64	63	ad2antrr 762	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (𝑡 ∈ (𝐹 “ 𝑠) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑡))
65	7, 60	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → Fun 𝐹)
66	65	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) ∧ 𝑦 ∈ 𝑠) → Fun 𝐹)
67		fbelss 21637	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ 𝑠 ∈ 𝐵) → 𝑠 ⊆ 𝑌)
68	1, 67	sylan 488	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ⊆ 𝑌)
69		fdm 6051	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐹:𝑌⟶𝑋 → dom 𝐹 = 𝑌)
70	7, 69	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → dom 𝐹 = 𝑌)
71	70	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → dom 𝐹 = 𝑌)
72	68, 71	sseqtr4d 3642	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ⊆ dom 𝐹)
73	72	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → 𝑠 ⊆ dom 𝐹)
74	73	sselda 3603	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) ∧ 𝑦 ∈ 𝑠) → 𝑦 ∈ dom 𝐹)
75		fvimacnv 6332	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹) → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑦 ∈ (^◡𝐹 “ 𝑥)))
76	66, 74, 75	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑦 ∈ (^◡𝐹 “ 𝑥)))
77		inelcm 4032	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ 𝑠 ∧ 𝑦 ∈ (^◡𝐹 “ 𝑥)) → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅)
78	77	ex 450	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ 𝑠 → (𝑦 ∈ (^◡𝐹 “ 𝑥) → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅))
79	78	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) ∧ 𝑦 ∈ 𝑠) → (𝑦 ∈ (^◡𝐹 “ 𝑥) → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅))
80	76, 79	sylbid 230	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) ∈ 𝑥 → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅))
81		eleq1 2689	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑦) = 𝑡 → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑡 ∈ 𝑥))
82	81	imbi1d 331	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑦) = 𝑡 → (((𝐹‘𝑦) ∈ 𝑥 → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅) ↔ (𝑡 ∈ 𝑥 → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅)))
83	80, 82	syl5ibcom 235	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) = 𝑡 → (𝑡 ∈ 𝑥 → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅)))
84	83	rexlimdva 3031	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑡 → (𝑡 ∈ 𝑥 → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅)))
85	64, 84	syld 47	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (𝑡 ∈ (𝐹 “ 𝑠) → (𝑡 ∈ 𝑥 → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅)))
86	85	impd 447	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → ((𝑡 ∈ (𝐹 “ 𝑠) ∧ 𝑡 ∈ 𝑥) → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅))
87	59, 86	syl5bi 232	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (𝑡 ∈ ((𝐹 “ 𝑠) ∩ 𝑥) → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅))
88	87	exlimdv 1861	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (∃𝑡 𝑡 ∈ ((𝐹 “ 𝑠) ∩ 𝑥) → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅))
89	58, 88	syl5bi 232	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (¬ ((𝐹 “ 𝑠) ∩ 𝑥) = ∅ → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅))
90	57, 89	mpd 15	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅)
91		ineq2 3808	. . . . . . . . . . 11 ⊢ (𝑡 = (^◡𝐹 “ 𝑥) → (𝑠 ∩ 𝑡) = (𝑠 ∩ (^◡𝐹 “ 𝑥)))
92	91	neeq1d 2853	. . . . . . . . . 10 ⊢ (𝑡 = (^◡𝐹 “ 𝑥) → ((𝑠 ∩ 𝑡) ≠ ∅ ↔ (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅))
93	90, 92	syl5ibrcom 237	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (𝑡 = (^◡𝐹 “ 𝑥) → (𝑠 ∩ 𝑡) ≠ ∅))
94	93	rexlimdva 3031	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (∃𝑥 ∈ 𝐿 𝑡 = (^◡𝐹 “ 𝑥) → (𝑠 ∩ 𝑡) ≠ ∅))
95	37, 94	syl5bi 232	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅))
96	95	expimpd 629	. . . . . 6 ⊢ (𝜑 → ((𝑠 ∈ 𝐵 ∧ 𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) → (𝑠 ∩ 𝑡) ≠ ∅))
97	96	ralrimivv 2970	. . . . 5 ⊢ (𝜑 → ∀𝑠 ∈ 𝐵 ∀𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))(𝑠 ∩ 𝑡) ≠ ∅)
98		fbunfip 21673	. . . . . 6 ⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌)) → (¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))) ↔ ∀𝑠 ∈ 𝐵 ∀𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))(𝑠 ∩ 𝑡) ≠ ∅))
99	1, 25, 98	syl2anc 693	. . . . 5 ⊢ (𝜑 → (¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))) ↔ ∀𝑠 ∈ 𝐵 ∀𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))(𝑠 ∩ 𝑡) ≠ ∅))
100	97, 99	mpbird 247	. . . 4 ⊢ (𝜑 → ¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))
101		fsubbas 21671	. . . . 5 ⊢ (𝑌 ∈ dom fBas → ((fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌) ↔ ((𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ⊆ 𝒫 𝑌 ∧ (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))))
102	1, 4, 101	3syl 18	. . . 4 ⊢ (𝜑 → ((fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌) ↔ ((𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ⊆ 𝒫 𝑌 ∧ (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))))
103	28, 33, 100, 102	mpbir3and 1245	. . 3 ⊢ (𝜑 → (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌))
104		fgcl 21682	. . 3 ⊢ ((fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌) → (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) ∈ (Fil‘𝑌))
105	103, 104	syl 17	. 2 ⊢ (𝜑 → (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) ∈ (Fil‘𝑌))
106		unexg 6959	. . . . . 6 ⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌)) → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ∈ V)
107	1, 25, 106	syl2anc 693	. . . . 5 ⊢ (𝜑 → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ∈ V)
108		ssfii 8325	. . . . 5 ⊢ ((𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ∈ V → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))
109	107, 108	syl 17	. . . 4 ⊢ (𝜑 → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))
110	109	unssad 3790	. . 3 ⊢ (𝜑 → 𝐵 ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))
111		ssfg 21676	. . . 4 ⊢ ((fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌) → (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))) ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))))
112	103, 111	syl 17	. . 3 ⊢ (𝜑 → (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))) ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))))
113	110, 112	sstrd 3613	. 2 ⊢ (𝜑 → 𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))))
114	1, 6, 7, 8	fmfnfmlem4 21761	. . . . 5 ⊢ (𝜑 → (𝑡 ∈ 𝐿 ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡)))
115		elfm 21751	. . . . . 6 ⊢ ((𝑋 ∈ 𝐿 ∧ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝑡 ∈ ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡)))
116	15, 103, 7, 115	syl3anc 1326	. . . . 5 ⊢ (𝜑 → (𝑡 ∈ ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡)))
117	114, 116	bitr4d 271	. . . 4 ⊢ (𝜑 → (𝑡 ∈ 𝐿 ↔ 𝑡 ∈ ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))))
118	117	eqrdv 2620	. . 3 ⊢ (𝜑 → 𝐿 = ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))))
119		eqid 2622	. . . . 5 ⊢ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))
120	119	fmfg 21753	. . . 4 ⊢ ((𝑋 ∈ 𝐿 ∧ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))))
121	15, 103, 7, 120	syl3anc 1326	. . 3 ⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))))
122	118, 121	eqtrd 2656	. 2 ⊢ (𝜑 → 𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))))
123		sseq2 3627	. . . 4 ⊢ (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) → (𝐵 ⊆ 𝑓 ↔ 𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))))
124		fveq2 6191	. . . . 5 ⊢ (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) → ((𝑋 FilMap 𝐹)‘𝑓) = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))))
125	124	eqeq2d 2632	. . . 4 ⊢ (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) → (𝐿 = ((𝑋 FilMap 𝐹)‘𝑓) ↔ 𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))))))
126	123, 125	anbi12d 747	. . 3 ⊢ (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) → ((𝐵 ⊆ 𝑓 ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘𝑓)) ↔ (𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))))))
127	126	rspcev 3309	. 2 ⊢ (((𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) ∈ (Fil‘𝑌) ∧ (𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))))) → ∃𝑓 ∈ (Fil‘𝑌)(𝐵 ⊆ 𝑓 ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘𝑓)))
128	105, 113, 122, 127	syl12anc 1324	1 ⊢ (𝜑 → ∃𝑓 ∈ (Fil‘𝑌)(𝐵 ⊆ 𝑓 ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘𝑓)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∃wex 1704 ∈ wcel 1990 ≠ wne 2794 ∀wral 2912 ∃wrex 2913 Vcvv 3200 ∪ cun 3572 ∩ cin 3573 ⊆ wss 3574 ∅c0 3915 𝒫 cpw 4158 ↦ cmpt 4729 ^◡ccnv 5113 dom cdm 5114 ran crn 5115 “ cima 5117 Fun wfun 5882 Fn wfn 5883 ⟶wf 5884 –onto→wfo 5886 ‘cfv 5888 (class class class)co 6650 ficfi 8316 fBascfbas 19734 filGencfg 19735 Filcfil 21649 FilMap cfm 21737

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-en 7956 df-fin 7959 df-fi 8317 df-fbas 19743 df-fg 19744 df-fil 21650 df-fm 21742

This theorem is referenced by: fmufil 21763 cnpfcf 21845

W3C validator