fgabs - Metamath Proof Explorer

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

Theorem fgabs 23727

Description: Absorption law for filter generation. (Contributed by Mario Carneiro, 15-Oct-2015.)

**Assertion**
Ref	Expression
fgabs	⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹))

Proof of Theorem fgabs Dummy variables 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpll 764	. . . . . . . . 9 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝐹 ∈ (fBas‘𝑌))
2		fgcl 23726	. . . . . . . . 9 ⊢ (𝐹 ∈ (fBas‘𝑌) → (𝑌filGen𝐹) ∈ (Fil‘𝑌))
3		filfbas 23696	. . . . . . . . 9 ⊢ ((𝑌filGen𝐹) ∈ (Fil‘𝑌) → (𝑌filGen𝐹) ∈ (fBas‘𝑌))
4	1, 2, 3	3syl 18	. . . . . . . 8 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑌filGen𝐹) ∈ (fBas‘𝑌))
5		fbsspw 23680	. . . . . . . . . 10 ⊢ ((𝑌filGen𝐹) ∈ (fBas‘𝑌) → (𝑌filGen𝐹) ⊆ 𝒫 𝑌)
6	4, 5	syl 17	. . . . . . . . 9 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑌filGen𝐹) ⊆ 𝒫 𝑌)
7		simplr 766	. . . . . . . . . 10 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝑌 ⊆ 𝑋)
8	7	sspwd 4608	. . . . . . . . 9 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝒫 𝑌 ⊆ 𝒫 𝑋)
9	6, 8	sstrd 3985	. . . . . . . 8 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑌filGen𝐹) ⊆ 𝒫 𝑋)
10		simpr 484	. . . . . . . 8 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝑋 ∈ V)
11		fbasweak 23713	. . . . . . . 8 ⊢ (((𝑌filGen𝐹) ∈ (fBas‘𝑌) ∧ (𝑌filGen𝐹) ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → (𝑌filGen𝐹) ∈ (fBas‘𝑋))
12	4, 9, 10, 11	syl3anc 1368	. . . . . . 7 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑌filGen𝐹) ∈ (fBas‘𝑋))
13		elfg 23719	. . . . . . 7 ⊢ ((𝑌filGen𝐹) ∈ (fBas‘𝑋) → (𝑥 ∈ (𝑋filGen(𝑌filGen𝐹)) ↔ (𝑥 ⊆ 𝑋 ∧ ∃𝑦 ∈ (𝑌filGen𝐹)𝑦 ⊆ 𝑥)))
14	12, 13	syl 17	. . . . . 6 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑥 ∈ (𝑋filGen(𝑌filGen𝐹)) ↔ (𝑥 ⊆ 𝑋 ∧ ∃𝑦 ∈ (𝑌filGen𝐹)𝑦 ⊆ 𝑥)))
15	1	adantr 480	. . . . . . . . . 10 ⊢ ((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ 𝑥 ⊆ 𝑋) → 𝐹 ∈ (fBas‘𝑌))
16		elfg 23719	. . . . . . . . . 10 ⊢ (𝐹 ∈ (fBas‘𝑌) → (𝑦 ∈ (𝑌filGen𝐹) ↔ (𝑦 ⊆ 𝑌 ∧ ∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑦)))
17	15, 16	syl 17	. . . . . . . . 9 ⊢ ((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ 𝑥 ⊆ 𝑋) → (𝑦 ∈ (𝑌filGen𝐹) ↔ (𝑦 ⊆ 𝑌 ∧ ∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑦)))
18		fbsspw 23680	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (fBas‘𝑌) → 𝐹 ⊆ 𝒫 𝑌)
19	1, 18	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝐹 ⊆ 𝒫 𝑌)
20	19, 8	sstrd 3985	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝐹 ⊆ 𝒫 𝑋)
21		fbasweak 23713	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝐹 ⊆ 𝒫 𝑋 ∧ 𝑋 ∈ V) → 𝐹 ∈ (fBas‘𝑋))
22	1, 20, 10, 21	syl3anc 1368	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝐹 ∈ (fBas‘𝑋))
23		fgcl 23726	. . . . . . . . . . . . . . . 16 ⊢ (𝐹 ∈ (fBas‘𝑋) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
24	22, 23	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
25	24	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ ((𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦) ∧ 𝑦 ⊆ 𝑥)) → (𝑋filGen𝐹) ∈ (Fil‘𝑋))
26		ssfg 23720	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ∈ (fBas‘𝑋) → 𝐹 ⊆ (𝑋filGen𝐹))
27	22, 26	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝐹 ⊆ (𝑋filGen𝐹))
28	27	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) → 𝐹 ⊆ (𝑋filGen𝐹))
29	28	sselda 3975	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ 𝑧 ∈ 𝐹) → 𝑧 ∈ (𝑋filGen𝐹))
30	29	adantrr 714	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ (𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦)) → 𝑧 ∈ (𝑋filGen𝐹))
31	30	adantrr 714	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ ((𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦) ∧ 𝑦 ⊆ 𝑥)) → 𝑧 ∈ (𝑋filGen𝐹))
32		simplrl 774	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ ((𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦) ∧ 𝑦 ⊆ 𝑥)) → 𝑥 ⊆ 𝑋)
33		simprlr 777	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ ((𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦) ∧ 𝑦 ⊆ 𝑥)) → 𝑧 ⊆ 𝑦)
34		simprr 770	. . . . . . . . . . . . . . 15 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ ((𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦) ∧ 𝑦 ⊆ 𝑥)) → 𝑦 ⊆ 𝑥)
35	33, 34	sstrd 3985	. . . . . . . . . . . . . 14 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ ((𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦) ∧ 𝑦 ⊆ 𝑥)) → 𝑧 ⊆ 𝑥)
36		filss 23701	. . . . . . . . . . . . . 14 ⊢ (((𝑋filGen𝐹) ∈ (Fil‘𝑋) ∧ (𝑧 ∈ (𝑋filGen𝐹) ∧ 𝑥 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑥)) → 𝑥 ∈ (𝑋filGen𝐹))
37	25, 31, 32, 35, 36	syl13anc 1369	. . . . . . . . . . . . 13 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ ((𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦) ∧ 𝑦 ⊆ 𝑥)) → 𝑥 ∈ (𝑋filGen𝐹))
38	37	expr 456	. . . . . . . . . . . 12 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) ∧ (𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ 𝑦)) → (𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝑋filGen𝐹)))
39	38	rexlimdvaa 3148	. . . . . . . . . . 11 ⊢ ((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ (𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌)) → (∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑦 → (𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝑋filGen𝐹))))
40	39	anassrs 467	. . . . . . . . . 10 ⊢ (((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ 𝑥 ⊆ 𝑋) ∧ 𝑦 ⊆ 𝑌) → (∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑦 → (𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝑋filGen𝐹))))
41	40	expimpd 453	. . . . . . . . 9 ⊢ ((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ 𝑥 ⊆ 𝑋) → ((𝑦 ⊆ 𝑌 ∧ ∃𝑧 ∈ 𝐹 𝑧 ⊆ 𝑦) → (𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝑋filGen𝐹))))
42	17, 41	sylbid 239	. . . . . . . 8 ⊢ ((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ 𝑥 ⊆ 𝑋) → (𝑦 ∈ (𝑌filGen𝐹) → (𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝑋filGen𝐹))))
43	42	rexlimdv 3145	. . . . . . 7 ⊢ ((((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) ∧ 𝑥 ⊆ 𝑋) → (∃𝑦 ∈ (𝑌filGen𝐹)𝑦 ⊆ 𝑥 → 𝑥 ∈ (𝑋filGen𝐹)))
44	43	expimpd 453	. . . . . 6 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → ((𝑥 ⊆ 𝑋 ∧ ∃𝑦 ∈ (𝑌filGen𝐹)𝑦 ⊆ 𝑥) → 𝑥 ∈ (𝑋filGen𝐹)))
45	14, 44	sylbid 239	. . . . 5 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑥 ∈ (𝑋filGen(𝑌filGen𝐹)) → 𝑥 ∈ (𝑋filGen𝐹)))
46	45	ssrdv 3981	. . . 4 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑋filGen(𝑌filGen𝐹)) ⊆ (𝑋filGen𝐹))
47		ssfg 23720	. . . . . 6 ⊢ (𝐹 ∈ (fBas‘𝑌) → 𝐹 ⊆ (𝑌filGen𝐹))
48	47	ad2antrr 723	. . . . 5 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → 𝐹 ⊆ (𝑌filGen𝐹))
49		fgss 23721	. . . . 5 ⊢ ((𝐹 ∈ (fBas‘𝑋) ∧ (𝑌filGen𝐹) ∈ (fBas‘𝑋) ∧ 𝐹 ⊆ (𝑌filGen𝐹)) → (𝑋filGen𝐹) ⊆ (𝑋filGen(𝑌filGen𝐹)))
50	22, 12, 48, 49	syl3anc 1368	. . . 4 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑋filGen𝐹) ⊆ (𝑋filGen(𝑌filGen𝐹)))
51	46, 50	eqssd 3992	. . 3 ⊢ (((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) ∧ 𝑋 ∈ V) → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹))
52	51	ex 412	. 2 ⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) → (𝑋 ∈ V → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹)))
53		df-fg 21232	. . . . 5 ⊢ filGen = (𝑤 ∈ V, 𝑥 ∈ (fBas‘𝑤) ↦ {𝑦 ∈ 𝒫 𝑤 ∣ (𝑥 ∩ 𝒫 𝑦) ≠ ∅})
54	53	reldmmpo 7536	. . . 4 ⊢ Rel dom filGen
55	54	ovprc1 7441	. . 3 ⊢ (¬ 𝑋 ∈ V → (𝑋filGen(𝑌filGen𝐹)) = ∅)
56	54	ovprc1 7441	. . 3 ⊢ (¬ 𝑋 ∈ V → (𝑋filGen𝐹) = ∅)
57	55, 56	eqtr4d 2767	. 2 ⊢ (¬ 𝑋 ∈ V → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹))
58	52, 57	pm2.61d1 180	1 ⊢ ((𝐹 ∈ (fBas‘𝑌) ∧ 𝑌 ⊆ 𝑋) → (𝑋filGen(𝑌filGen𝐹)) = (𝑋filGen𝐹))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1533 ∈ wcel 2098 ≠ wne 2932 ∃wrex 3062 {crab 3424 Vcvv 3466 ∩ cin 3940 ⊆ wss 3941 ∅c0 4315 𝒫 cpw 4595 ‘cfv 6534 (class class class)co 7402 fBascfbas 21222 filGencfg 21223 Filcfil 23693

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-sep 5290 ax-nul 5297 ax-pow 5354 ax-pr 5418

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-nel 3039 df-ral 3054 df-rex 3063 df-rab 3425 df-v 3468 df-sbc 3771 df-csb 3887 df-dif 3944 df-un 3946 df-in 3948 df-ss 3958 df-nul 4316 df-if 4522 df-pw 4597 df-sn 4622 df-pr 4624 df-op 4628 df-uni 4901 df-br 5140 df-opab 5202 df-mpt 5223 df-id 5565 df-xp 5673 df-rel 5674 df-cnv 5675 df-co 5676 df-dm 5677 df-rn 5678 df-res 5679 df-ima 5680 df-iota 6486 df-fun 6536 df-fv 6542 df-ov 7405 df-oprab 7406 df-mpo 7407 df-fbas 21231 df-fg 21232 df-fil 23694

This theorem is referenced by: minveclem4a 25302

W3C validator