Theorem kelac2

Description: Kelley's choice, most common form: compactness of a product of knob topologies recovers choice. (Contributed by Stefan O'Rear, 22-Feb-2015)

	Ref	Expression
Hypotheses	kelac2.s	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑆 ∈ 𝑉 )
	kelac2.z	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑆 ≠ ∅ )
	kelac2.k	⊢ ( 𝜑 → ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ) ) ∈ Comp )
Assertion	kelac2	⊢ ( 𝜑 → X 𝑥 ∈ 𝐼 𝑆 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		kelac2.s	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑆 ∈ 𝑉 )
2		kelac2.z	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑆 ≠ ∅ )
3		kelac2.k	⊢ ( 𝜑 → ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ) ) ∈ Comp )
4		kelac2lem	⊢ ( 𝑆 ∈ 𝑉 → ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ∈ Comp )
5		cmptop	⊢ ( ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ∈ Comp → ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ∈ Top )
6	1 4 5	3syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ∈ Top )
7		uncom	⊢ ( 𝑆 ∪ { 𝒫 ∪ 𝑆 } ) = ( { 𝒫 ∪ 𝑆 } ∪ 𝑆 )
8	7	difeq1i	⊢ ( ( 𝑆 ∪ { 𝒫 ∪ 𝑆 } ) ∖ 𝑆 ) = ( ( { 𝒫 ∪ 𝑆 } ∪ 𝑆 ) ∖ 𝑆 )
9		difun2	⊢ ( ( { 𝒫 ∪ 𝑆 } ∪ 𝑆 ) ∖ 𝑆 ) = ( { 𝒫 ∪ 𝑆 } ∖ 𝑆 )
10	8 9	eqtri	⊢ ( ( 𝑆 ∪ { 𝒫 ∪ 𝑆 } ) ∖ 𝑆 ) = ( { 𝒫 ∪ 𝑆 } ∖ 𝑆 )
11		snex	⊢ { 𝒫 ∪ 𝑆 } ∈ V
12		uniprg	⊢ ( ( 𝑆 ∈ 𝑉 ∧ { 𝒫 ∪ 𝑆 } ∈ V ) → ∪ { 𝑆 , { 𝒫 ∪ 𝑆 } } = ( 𝑆 ∪ { 𝒫 ∪ 𝑆 } ) )
13	1 11 12	sylancl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ∪ { 𝑆 , { 𝒫 ∪ 𝑆 } } = ( 𝑆 ∪ { 𝒫 ∪ 𝑆 } ) )
14	13	difeq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ∪ { 𝑆 , { 𝒫 ∪ 𝑆 } } ∖ 𝑆 ) = ( ( 𝑆 ∪ { 𝒫 ∪ 𝑆 } ) ∖ 𝑆 ) )
15		incom	⊢ ( { 𝒫 ∪ 𝑆 } ∩ 𝑆 ) = ( 𝑆 ∩ { 𝒫 ∪ 𝑆 } )
16		pwuninel	⊢ ¬ 𝒫 ∪ 𝑆 ∈ 𝑆
17	16	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ¬ 𝒫 ∪ 𝑆 ∈ 𝑆 )
18		disjsn	⊢ ( ( 𝑆 ∩ { 𝒫 ∪ 𝑆 } ) = ∅ ↔ ¬ 𝒫 ∪ 𝑆 ∈ 𝑆 )
19	17 18	sylibr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑆 ∩ { 𝒫 ∪ 𝑆 } ) = ∅ )
20	15 19	eqtrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( { 𝒫 ∪ 𝑆 } ∩ 𝑆 ) = ∅ )
21		disj3	⊢ ( ( { 𝒫 ∪ 𝑆 } ∩ 𝑆 ) = ∅ ↔ { 𝒫 ∪ 𝑆 } = ( { 𝒫 ∪ 𝑆 } ∖ 𝑆 ) )
22	20 21	sylib	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → { 𝒫 ∪ 𝑆 } = ( { 𝒫 ∪ 𝑆 } ∖ 𝑆 ) )
23	10 14 22	3eqtr4a	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ∪ { 𝑆 , { 𝒫 ∪ 𝑆 } } ∖ 𝑆 ) = { 𝒫 ∪ 𝑆 } )
24		prex	⊢ { 𝑆 , { 𝒫 ∪ 𝑆 } } ∈ V
25		bastg	⊢ ( { 𝑆 , { 𝒫 ∪ 𝑆 } } ∈ V → { 𝑆 , { 𝒫 ∪ 𝑆 } } ⊆ ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) )
26	24 25	mp1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → { 𝑆 , { 𝒫 ∪ 𝑆 } } ⊆ ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) )
27	11	prid2	⊢ { 𝒫 ∪ 𝑆 } ∈ { 𝑆 , { 𝒫 ∪ 𝑆 } }
28	27	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → { 𝒫 ∪ 𝑆 } ∈ { 𝑆 , { 𝒫 ∪ 𝑆 } } )
29	26 28	sseldd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → { 𝒫 ∪ 𝑆 } ∈ ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) )
30	23 29	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ∪ { 𝑆 , { 𝒫 ∪ 𝑆 } } ∖ 𝑆 ) ∈ ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) )
31		prid1g	⊢ ( 𝑆 ∈ 𝑉 → 𝑆 ∈ { 𝑆 , { 𝒫 ∪ 𝑆 } } )
32		elssuni	⊢ ( 𝑆 ∈ { 𝑆 , { 𝒫 ∪ 𝑆 } } → 𝑆 ⊆ ∪ { 𝑆 , { 𝒫 ∪ 𝑆 } } )
33	1 31 32	3syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑆 ⊆ ∪ { 𝑆 , { 𝒫 ∪ 𝑆 } } )
34		unitg	⊢ ( { 𝑆 , { 𝒫 ∪ 𝑆 } } ∈ V → ∪ ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) = ∪ { 𝑆 , { 𝒫 ∪ 𝑆 } } )
35	24 34	ax-mp	⊢ ∪ ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) = ∪ { 𝑆 , { 𝒫 ∪ 𝑆 } }
36	35	eqcomi	⊢ ∪ { 𝑆 , { 𝒫 ∪ 𝑆 } } = ∪ ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } )
37	36	iscld2	⊢ ( ( ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ∈ Top ∧ 𝑆 ⊆ ∪ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) → ( 𝑆 ∈ ( Clsd ‘ ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ) ↔ ( ∪ { 𝑆 , { 𝒫 ∪ 𝑆 } } ∖ 𝑆 ) ∈ ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ) )
38	6 33 37	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑆 ∈ ( Clsd ‘ ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ) ↔ ( ∪ { 𝑆 , { 𝒫 ∪ 𝑆 } } ∖ 𝑆 ) ∈ ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ) )
39	30 38	mpbird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑆 ∈ ( Clsd ‘ ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) ) )
40		f1oi	⊢ ( I ↾ 𝑆 ) : 𝑆 –1-1-onto→ 𝑆
41	40	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( I ↾ 𝑆 ) : 𝑆 –1-1-onto→ 𝑆 )
42		elssuni	⊢ ( { 𝒫 ∪ 𝑆 } ∈ { 𝑆 , { 𝒫 ∪ 𝑆 } } → { 𝒫 ∪ 𝑆 } ⊆ ∪ { 𝑆 , { 𝒫 ∪ 𝑆 } } )
43	27 42	mp1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → { 𝒫 ∪ 𝑆 } ⊆ ∪ { 𝑆 , { 𝒫 ∪ 𝑆 } } )
44		uniexg	⊢ ( 𝑆 ∈ 𝑉 → ∪ 𝑆 ∈ V )
45		pwexg	⊢ ( ∪ 𝑆 ∈ V → 𝒫 ∪ 𝑆 ∈ V )
46		snidg	⊢ ( 𝒫 ∪ 𝑆 ∈ V → 𝒫 ∪ 𝑆 ∈ { 𝒫 ∪ 𝑆 } )
47	1 44 45 46	4syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝒫 ∪ 𝑆 ∈ { 𝒫 ∪ 𝑆 } )
48	43 47	sseldd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝒫 ∪ 𝑆 ∈ ∪ { 𝑆 , { 𝒫 ∪ 𝑆 } } )
49	48 35	eleqtrrdi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝒫 ∪ 𝑆 ∈ ∪ ( topGen ‘ { 𝑆 , { 𝒫 ∪ 𝑆 } } ) )
50	2 6 39 41 49 3	kelac1	⊢ ( 𝜑 → X 𝑥 ∈ 𝐼 𝑆 ≠ ∅ )