Theorem kelac2lem

Description: Lemma for kelac2 and dfac21 : knob topologies are compact. (Contributed by Stefan O'Rear, 22-Feb-2015)

	Ref	Expression
Assertion	kelac2lem	⊢ ( 𝑆 ∈ 𝑉 → ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ∈ Comp )

Proof

Step	Hyp	Ref	Expression
1		prex	⊢ { 𝑆 , { 𝒫 ∪ 𝑆 } } ∈ V
2		vex	⊢ 𝑥 ∈ V
3	2	elpr	⊢ ( 𝑥 ∈ { 𝑆 , { 𝒫 ∪ 𝑆 } } ↔ ( 𝑥 = 𝑆 ∨ 𝑥 = { 𝒫 ∪ 𝑆 } ) )
4		vex	⊢ 𝑦 ∈ V
5	4	elpr	⊢ ( 𝑦 ∈ { 𝑆 , { 𝒫 ∪ 𝑆 } } ↔ ( 𝑦 = 𝑆 ∨ 𝑦 = { 𝒫 ∪ 𝑆 } ) )
6		eqtr3	⊢ ( ( 𝑥 = 𝑆 ∧ 𝑦 = 𝑆 ) → 𝑥 = 𝑦 )
7	6	orcd	⊢ ( ( 𝑥 = 𝑆 ∧ 𝑦 = 𝑆 ) → ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
8		ineq12	⊢ ( ( 𝑥 = { 𝒫 ∪ 𝑆 } ∧ 𝑦 = 𝑆 ) → ( 𝑥 ∩ 𝑦 ) = ( { 𝒫 ∪ 𝑆 } ∩ 𝑆 ) )
9		incom	⊢ ( { 𝒫 ∪ 𝑆 } ∩ 𝑆 ) = ( 𝑆 ∩ { 𝒫 ∪ 𝑆 } )
10		pwuninel	⊢ ¬ 𝒫 ∪ 𝑆 ∈ 𝑆
11		disjsn	⊢ ( ( 𝑆 ∩ { 𝒫 ∪ 𝑆 } ) = ∅ ↔ ¬ 𝒫 ∪ 𝑆 ∈ 𝑆 )
12	10 11	mpbir	⊢ ( 𝑆 ∩ { 𝒫 ∪ 𝑆 } ) = ∅
13	9 12	eqtri	⊢ ( { 𝒫 ∪ 𝑆 } ∩ 𝑆 ) = ∅
14	8 13	eqtrdi	⊢ ( ( 𝑥 = { 𝒫 ∪ 𝑆 } ∧ 𝑦 = 𝑆 ) → ( 𝑥 ∩ 𝑦 ) = ∅ )
15	14	olcd	⊢ ( ( 𝑥 = { 𝒫 ∪ 𝑆 } ∧ 𝑦 = 𝑆 ) → ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
16		ineq12	⊢ ( ( 𝑥 = 𝑆 ∧ 𝑦 = { 𝒫 ∪ 𝑆 } ) → ( 𝑥 ∩ 𝑦 ) = ( 𝑆 ∩ { 𝒫 ∪ 𝑆 } ) )
17	16 12	eqtrdi	⊢ ( ( 𝑥 = 𝑆 ∧ 𝑦 = { 𝒫 ∪ 𝑆 } ) → ( 𝑥 ∩ 𝑦 ) = ∅ )
18	17	olcd	⊢ ( ( 𝑥 = 𝑆 ∧ 𝑦 = { 𝒫 ∪ 𝑆 } ) → ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
19		eqtr3	⊢ ( ( 𝑥 = { 𝒫 ∪ 𝑆 } ∧ 𝑦 = { 𝒫 ∪ 𝑆 } ) → 𝑥 = 𝑦 )
20	19	orcd	⊢ ( ( 𝑥 = { 𝒫 ∪ 𝑆 } ∧ 𝑦 = { 𝒫 ∪ 𝑆 } ) → ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
21	7 15 18 20	ccase	⊢ ( ( ( 𝑥 = 𝑆 ∨ 𝑥 = { 𝒫 ∪ 𝑆 } ) ∧ ( 𝑦 = 𝑆 ∨ 𝑦 = { 𝒫 ∪ 𝑆 } ) ) → ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
22	3 5 21	syl2anb	⊢ ( ( 𝑥 ∈ { 𝑆 , { 𝒫 ∪ 𝑆 } } ∧ 𝑦 ∈ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) → ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
23	22	rgen2	⊢ ∀ 𝑥 ∈ { 𝑆 , { 𝒫 ∪ 𝑆 } } ∀ 𝑦 ∈ { 𝑆 , { 𝒫 ∪ 𝑆 } } ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ )
24		baspartn	⊢ ( ( { 𝑆 , { 𝒫 ∪ 𝑆 } } ∈ V ∧ ∀ 𝑥 ∈ { 𝑆 , { 𝒫 ∪ 𝑆 } } ∀ 𝑦 ∈ { 𝑆 , { 𝒫 ∪ 𝑆 } } ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → { 𝑆 , { 𝒫 ∪ 𝑆 } } ∈ TopBases )
25	1 23 24	mp2an	⊢ { 𝑆 , { 𝒫 ∪ 𝑆 } } ∈ TopBases
26		tgcl	⊢ ( { 𝑆 , { 𝒫 ∪ 𝑆 } } ∈ TopBases → ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ∈ Top )
27	25 26	mp1i	⊢ ( 𝑆 ∈ 𝑉 → ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ∈ Top )
28		prfi	⊢ { 𝑆 , { 𝒫 ∪ 𝑆 } } ∈ Fin
29		pwfi	⊢ ( { 𝑆 , { 𝒫 ∪ 𝑆 } } ∈ Fin ↔ 𝒫 { 𝑆 , { 𝒫 ∪ 𝑆 } } ∈ Fin )
30	28 29	mpbi	⊢ 𝒫 { 𝑆 , { 𝒫 ∪ 𝑆 } } ∈ Fin
31		tgdom	⊢ ( { 𝑆 , { 𝒫 ∪ 𝑆 } } ∈ V → ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ≼ 𝒫 { 𝑆 , { 𝒫 ∪ 𝑆 } } )
32	1 31	ax-mp	⊢ ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ≼ 𝒫 { 𝑆 , { 𝒫 ∪ 𝑆 } }
33		domfi	⊢ ( ( 𝒫 { 𝑆 , { 𝒫 ∪ 𝑆 } } ∈ Fin ∧ ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ≼ 𝒫 { 𝑆 , { 𝒫 ∪ 𝑆 } } ) → ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ∈ Fin )
34	30 32 33	mp2an	⊢ ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ∈ Fin
35	34	a1i	⊢ ( 𝑆 ∈ 𝑉 → ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ∈ Fin )
36	27 35	elind	⊢ ( 𝑆 ∈ 𝑉 → ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ∈ ( Top ∩ Fin ) )
37		fincmp	⊢ ( ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ∈ ( Top ∩ Fin ) → ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ∈ Comp )
38	36 37	syl	⊢ ( 𝑆 ∈ 𝑉 → ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ∈ Comp )