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 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.

Step	Hyp	Ref	Expression
1		fmfnfm.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ (fBas‘𝑌))
2		fbsspw 21915	. . . . . 6 ⊢ (𝐵 ∈ (fBas‘𝑌) → 𝐵 ⊆ 𝒫 𝑌)
3	1, 2	syl 17	. . . . 5 ⊢ (𝜑 → 𝐵 ⊆ 𝒫 𝑌)
4		elfvdm 6407	. . . . . . . 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 6223	. . . . . . . . . . 11 ⊢ (𝐹:𝑌⟶𝑋 → 𝐹 Fn 𝑌)
10		dffn4 6304	. . . . . . . . . . 11 ⊢ (𝐹 Fn 𝑌 ↔ 𝐹:𝑌–onto→ran 𝐹)
11	9, 10	sylib 209	. . . . . . . . . 10 ⊢ (𝐹:𝑌⟶𝑋 → 𝐹:𝑌–onto→ran 𝐹)
12		foima 6303	. . . . . . . . . 10 ⊢ (𝐹:𝑌–onto→ran 𝐹 → (𝐹 “ 𝑌) = ran 𝐹)
13	7, 11, 12	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 “ 𝑌) = ran 𝐹)
14		filtop 21938	. . . . . . . . . . 11 ⊢ (𝐿 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐿)
15	6, 14	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ 𝐿)
16		fgcl 21961	. . . . . . . . . . 11 ⊢ (𝐵 ∈ (fBas‘𝑌) → (𝑌filGen𝐵) ∈ (Fil‘𝑌))
17		filtop 21938	. . . . . . . . . . 11 ⊢ ((𝑌filGen𝐵) ∈ (Fil‘𝑌) → 𝑌 ∈ (𝑌filGen𝐵))
18	1, 16, 17	3syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ∈ (𝑌filGen𝐵))
19		eqid 2765	. . . . . . . . . . 11 ⊢ (𝑌filGen𝐵) = (𝑌filGen𝐵)
20	19	imaelfm 22034	. . . . . . . . . 10 ⊢ (((𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑌 ∈ (𝑌filGen𝐵)) → (𝐹 “ 𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
21	15, 1, 7, 18, 20	syl31anc 1492	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 “ 𝑌) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
22	13, 21	eqeltrrd 2845	. . . . . . . 8 ⊢ (𝜑 → ran 𝐹 ∈ ((𝑋 FilMap 𝐹)‘𝐵))
23	8, 22	sseldd 3762	. . . . . . 7 ⊢ (𝜑 → ran 𝐹 ∈ 𝐿)
24		rnelfmlem 22035	. . . . . . 7 ⊢ (((𝑌 ∈ dom fBas ∧ 𝐿 ∈ (Fil‘𝑋) ∧ 𝐹:𝑌⟶𝑋) ∧ ran 𝐹 ∈ 𝐿) → ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌))
25	5, 6, 7, 23, 24	syl31anc 1492	. . . . . 6 ⊢ (𝜑 → ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌))
26		fbsspw 21915	. . . . . 6 ⊢ (ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌) → ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ⊆ 𝒫 𝑌)
27	25, 26	syl 17	. . . . 5 ⊢ (𝜑 → ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ⊆ 𝒫 𝑌)
28	3, 27	unssd 3951	. . . 4 ⊢ (𝜑 → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ⊆ 𝒫 𝑌)
29		ssun1 3938	. . . . 5 ⊢ 𝐵 ⊆ (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))
30		fbasne0 21913	. . . . . 6 ⊢ (𝐵 ∈ (fBas‘𝑌) → 𝐵 ≠ ∅)
31	1, 30	syl 17	. . . . 5 ⊢ (𝜑 → 𝐵 ≠ ∅)
32		ssn0 4138	. . . . 5 ⊢ ((𝐵 ⊆ (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ∧ 𝐵 ≠ ∅) → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ≠ ∅)
33	29, 31, 32	sylancr 581	. . . 4 ⊢ (𝜑 → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ≠ ∅)
34		vex 3353	. . . . . . . . 9 ⊢ 𝑡 ∈ V
35		eqid 2765	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) = (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))
36	35	elrnmpt 5541	. . . . . . . . 9 ⊢ (𝑡 ∈ V → (𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑡 = (^◡𝐹 “ 𝑥)))
37	34, 36	ax-mp 5	. . . . . . . 8 ⊢ (𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝐿 𝑡 = (^◡𝐹 “ 𝑥))
38		0nelfil 21932	. . . . . . . . . . . . . 14 ⊢ (𝐿 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝐿)
39	6, 38	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ¬ ∅ ∈ 𝐿)
40	39	ad2antrr 717	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → ¬ ∅ ∈ 𝐿)
41	6	adantr 472	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝐿 ∈ (Fil‘𝑋))
42	8	adantr 472	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → ((𝑋 FilMap 𝐹)‘𝐵) ⊆ 𝐿)
43	15, 1, 7	3jca 1158	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋))
44	43	adantr 472	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋))
45		ssfg 21955	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ (fBas‘𝑌) → 𝐵 ⊆ (𝑌filGen𝐵))
46	1, 45	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ⊆ (𝑌filGen𝐵))
47	46	sselda 3761	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ∈ (𝑌filGen𝐵))
48	19	imaelfm 22034	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑋 ∈ 𝐿 ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑠 ∈ (𝑌filGen𝐵)) → (𝐹 “ 𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
49	44, 47, 48	syl2anc 579	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝐹 “ 𝑠) ∈ ((𝑋 FilMap 𝐹)‘𝐵))
50	42, 49	sseldd 3762	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝐹 “ 𝑠) ∈ 𝐿)
51	41, 50	jca 507	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝐿 ∈ (Fil‘𝑋) ∧ (𝐹 “ 𝑠) ∈ 𝐿))
52		filin 21937	. . . . . . . . . . . . . . 15 ⊢ ((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹 “ 𝑠) ∈ 𝐿 ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿)
53	52	3expa 1147	. . . . . . . . . . . . . 14 ⊢ (((𝐿 ∈ (Fil‘𝑋) ∧ (𝐹 “ 𝑠) ∈ 𝐿) ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿)
54	51, 53	sylan 575	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → ((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿)
55		eleq1 2832	. . . . . . . . . . . . 13 ⊢ (((𝐹 “ 𝑠) ∩ 𝑥) = ∅ → (((𝐹 “ 𝑠) ∩ 𝑥) ∈ 𝐿 ↔ ∅ ∈ 𝐿))
56	54, 55	syl5ibcom 236	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (((𝐹 “ 𝑠) ∩ 𝑥) = ∅ → ∅ ∈ 𝐿))
57	40, 56	mtod 189	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → ¬ ((𝐹 “ 𝑠) ∩ 𝑥) = ∅)
58		neq0 4094	. . . . . . . . . . . 12 ⊢ (¬ ((𝐹 “ 𝑠) ∩ 𝑥) = ∅ ↔ ∃𝑡 𝑡 ∈ ((𝐹 “ 𝑠) ∩ 𝑥))
59		elin 3958	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ ((𝐹 “ 𝑠) ∩ 𝑥) ↔ (𝑡 ∈ (𝐹 “ 𝑠) ∧ 𝑡 ∈ 𝑥))
60		ffun 6226	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹:𝑌⟶𝑋 → Fun 𝐹)
61		fvelima 6437	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Fun 𝐹 ∧ 𝑡 ∈ (𝐹 “ 𝑠)) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑡)
62	61	ex 401	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun 𝐹 → (𝑡 ∈ (𝐹 “ 𝑠) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑡))
63	7, 60, 62	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑡 ∈ (𝐹 “ 𝑠) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑡))
64	63	ad2antrr 717	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (𝑡 ∈ (𝐹 “ 𝑠) → ∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑡))
65	7, 60	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → Fun 𝐹)
66	65	ad3antrrr 721	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) ∧ 𝑦 ∈ 𝑠) → Fun 𝐹)
67		fbelss 21916	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ 𝑠 ∈ 𝐵) → 𝑠 ⊆ 𝑌)
68	1, 67	sylan 575	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ⊆ 𝑌)
69	7	fdmd 6232	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → dom 𝐹 = 𝑌)
70	69	adantr 472	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → dom 𝐹 = 𝑌)
71	68, 70	sseqtr4d 3802	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ⊆ dom 𝐹)
72	71	adantr 472	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → 𝑠 ⊆ dom 𝐹)
73	72	sselda 3761	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) ∧ 𝑦 ∈ 𝑠) → 𝑦 ∈ dom 𝐹)
74		fvimacnv 6522	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹) → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑦 ∈ (^◡𝐹 “ 𝑥)))
75	66, 73, 74	syl2anc 579	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑦 ∈ (^◡𝐹 “ 𝑥)))
76		inelcm 4193	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ 𝑠 ∧ 𝑦 ∈ (^◡𝐹 “ 𝑥)) → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅)
77	76	ex 401	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ 𝑠 → (𝑦 ∈ (^◡𝐹 “ 𝑥) → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅))
78	77	adantl 473	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) ∧ 𝑦 ∈ 𝑠) → (𝑦 ∈ (^◡𝐹 “ 𝑥) → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅))
79	75, 78	sylbid 231	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) ∈ 𝑥 → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅))
80		eleq1 2832	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐹‘𝑦) = 𝑡 → ((𝐹‘𝑦) ∈ 𝑥 ↔ 𝑡 ∈ 𝑥))
81	80	imbi1d 332	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑦) = 𝑡 → (((𝐹‘𝑦) ∈ 𝑥 → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅) ↔ (𝑡 ∈ 𝑥 → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅)))
82	79, 81	syl5ibcom 236	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) ∧ 𝑦 ∈ 𝑠) → ((𝐹‘𝑦) = 𝑡 → (𝑡 ∈ 𝑥 → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅)))
83	82	rexlimdva 3178	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (∃𝑦 ∈ 𝑠 (𝐹‘𝑦) = 𝑡 → (𝑡 ∈ 𝑥 → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅)))
84	64, 83	syld 47	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (𝑡 ∈ (𝐹 “ 𝑠) → (𝑡 ∈ 𝑥 → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅)))
85	84	impd 398	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → ((𝑡 ∈ (𝐹 “ 𝑠) ∧ 𝑡 ∈ 𝑥) → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅))
86	59, 85	syl5bi 233	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (𝑡 ∈ ((𝐹 “ 𝑠) ∩ 𝑥) → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅))
87	86	exlimdv 2028	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (∃𝑡 𝑡 ∈ ((𝐹 “ 𝑠) ∩ 𝑥) → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅))
88	58, 87	syl5bi 233	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (¬ ((𝐹 “ 𝑠) ∩ 𝑥) = ∅ → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅))
89	57, 88	mpd 15	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅)
90		ineq2 3970	. . . . . . . . . . 11 ⊢ (𝑡 = (^◡𝐹 “ 𝑥) → (𝑠 ∩ 𝑡) = (𝑠 ∩ (^◡𝐹 “ 𝑥)))
91	90	neeq1d 2996	. . . . . . . . . 10 ⊢ (𝑡 = (^◡𝐹 “ 𝑥) → ((𝑠 ∩ 𝑡) ≠ ∅ ↔ (𝑠 ∩ (^◡𝐹 “ 𝑥)) ≠ ∅))
92	89, 91	syl5ibrcom 238	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝐵) ∧ 𝑥 ∈ 𝐿) → (𝑡 = (^◡𝐹 “ 𝑥) → (𝑠 ∩ 𝑡) ≠ ∅))
93	92	rexlimdva 3178	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (∃𝑥 ∈ 𝐿 𝑡 = (^◡𝐹 “ 𝑥) → (𝑠 ∩ 𝑡) ≠ ∅))
94	37, 93	syl5bi 233	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → (𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅))
95	94	expimpd 445	. . . . . 6 ⊢ (𝜑 → ((𝑠 ∈ 𝐵 ∧ 𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) → (𝑠 ∩ 𝑡) ≠ ∅))
96	95	ralrimivv 3117	. . . . 5 ⊢ (𝜑 → ∀𝑠 ∈ 𝐵 ∀𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))(𝑠 ∩ 𝑡) ≠ ∅)
97		fbunfip 21952	. . . . . 6 ⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌)) → (¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))) ↔ ∀𝑠 ∈ 𝐵 ∀𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))(𝑠 ∩ 𝑡) ≠ ∅))
98	1, 25, 97	syl2anc 579	. . . . 5 ⊢ (𝜑 → (¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))) ↔ ∀𝑠 ∈ 𝐵 ∀𝑡 ∈ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))(𝑠 ∩ 𝑡) ≠ ∅))
99	96, 98	mpbird 248	. . . 4 ⊢ (𝜑 → ¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))
100		fsubbas 21950	. . . . 5 ⊢ (𝑌 ∈ dom fBas → ((fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌) ↔ ((𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ⊆ 𝒫 𝑌 ∧ (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))))
101	1, 4, 100	3syl 18	. . . 4 ⊢ (𝜑 → ((fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌) ↔ ((𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ⊆ 𝒫 𝑌 ∧ (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ≠ ∅ ∧ ¬ ∅ ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))))
102	28, 33, 99, 101	mpbir3and 1442	. . 3 ⊢ (𝜑 → (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌))
103		fgcl 21961	. . 3 ⊢ ((fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌) → (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) ∈ (Fil‘𝑌))
104	102, 103	syl 17	. 2 ⊢ (𝜑 → (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) ∈ (Fil‘𝑌))
105		unexg 7157	. . . . . 6 ⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)) ∈ (fBas‘𝑌)) → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ∈ V)
106	1, 25, 105	syl2anc 579	. . . . 5 ⊢ (𝜑 → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ∈ V)
107		ssfii 8532	. . . . 5 ⊢ ((𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ∈ V → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))
108	106, 107	syl 17	. . . 4 ⊢ (𝜑 → (𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))) ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))
109	108	unssad 3952	. . 3 ⊢ (𝜑 → 𝐵 ⊆ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))
110		ssfg 21955	. . . 4 ⊢ ((fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌) → (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))) ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))))
111	102, 110	syl 17	. . 3 ⊢ (𝜑 → (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))) ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))))
112	109, 111	sstrd 3771	. 2 ⊢ (𝜑 → 𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))))
113	1, 6, 7, 8	fmfnfmlem4 22040	. . . . 5 ⊢ (𝜑 → (𝑡 ∈ 𝐿 ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡)))
114		elfm 22030	. . . . . 6 ⊢ ((𝑋 ∈ 𝐿 ∧ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝑡 ∈ ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡)))
115	15, 102, 7, 114	syl3anc 1490	. . . . 5 ⊢ (𝜑 → (𝑡 ∈ ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) ↔ (𝑡 ⊆ 𝑋 ∧ ∃𝑠 ∈ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))(𝐹 “ 𝑠) ⊆ 𝑡)))
116	113, 115	bitr4d 273	. . . 4 ⊢ (𝜑 → (𝑡 ∈ 𝐿 ↔ 𝑡 ∈ ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))))
117	116	eqrdv 2763	. . 3 ⊢ (𝜑 → 𝐿 = ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))))
118		eqid 2765	. . . . 5 ⊢ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))
119	118	fmfg 22032	. . . 4 ⊢ ((𝑋 ∈ 𝐿 ∧ (fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))) ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))))
120	15, 102, 7, 119	syl3anc 1490	. . 3 ⊢ (𝜑 → ((𝑋 FilMap 𝐹)‘(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))))
121	117, 120	eqtrd 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 (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))))
124	123	eqeq2d 2775	. . . 4 ⊢ (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) → (𝐿 = ((𝑋 FilMap 𝐹)‘𝑓) ↔ 𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))))))
125	122, 124	anbi12d 624	. . 3 ⊢ (𝑓 = (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) → ((𝐵 ⊆ 𝑓 ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘𝑓)) ↔ (𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))))))
126	125	rspcev 3461	. 2 ⊢ (((𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) ∈ (Fil‘𝑌) ∧ (𝐵 ⊆ (𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥))))) ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘(𝑌filGen(fi‘(𝐵 ∪ ran (𝑥 ∈ 𝐿 ↦ (^◡𝐹 “ 𝑥)))))))) → ∃𝑓 ∈ (Fil‘𝑌)(𝐵 ⊆ 𝑓 ∧ 𝐿 = ((𝑋 FilMap 𝐹)‘𝑓)))
127	104, 112, 121, 126	syl12anc 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 –onto→wfo 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

W3C validator