Theorem topdifinfindis

Description: Part of Exercise 3 of Munkres p. 83. The topology of all subsets x of A such that the complement of x in A is infinite, or x is the empty set, or x is all of A , is the trivial topology when A is finite. (Contributed by ML, 14-Jul-2020)

	Ref	Expression
Hypothesis	topdifinf.t	⊢ 𝑇 = { 𝑥 ∈ 𝒫 𝐴 ∣ ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) }
Assertion	topdifinfindis	⊢ ( 𝐴 ∈ Fin → 𝑇 = { ∅ , 𝐴 } )

Proof

Step	Hyp	Ref	Expression
1		topdifinf.t	⊢ 𝑇 = { 𝑥 ∈ 𝒫 𝐴 ∣ ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) }
2		nfv	⊢ Ⅎ 𝑥 𝐴 ∈ Fin
3		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝒫 𝐴 ∣ ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) }
4	1 3	nfcxfr	⊢ Ⅎ 𝑥 𝑇
5		nfcv	⊢ Ⅎ 𝑥 { ∅ , 𝐴 }
6		0elpw	⊢ ∅ ∈ 𝒫 𝐴
7		eleq1a	⊢ ( ∅ ∈ 𝒫 𝐴 → ( 𝑥 = ∅ → 𝑥 ∈ 𝒫 𝐴 ) )
8	6 7	mp1i	⊢ ( 𝐴 ∈ Fin → ( 𝑥 = ∅ → 𝑥 ∈ 𝒫 𝐴 ) )
9		pwidg	⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ 𝒫 𝐴 )
10		eleq1a	⊢ ( 𝐴 ∈ 𝒫 𝐴 → ( 𝑥 = 𝐴 → 𝑥 ∈ 𝒫 𝐴 ) )
11	9 10	syl	⊢ ( 𝐴 ∈ Fin → ( 𝑥 = 𝐴 → 𝑥 ∈ 𝒫 𝐴 ) )
12	8 11	jaod	⊢ ( 𝐴 ∈ Fin → ( ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) → 𝑥 ∈ 𝒫 𝐴 ) )
13	12	pm4.71rd	⊢ ( 𝐴 ∈ Fin → ( ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) ) )
14		vex	⊢ 𝑥 ∈ V
15	14	elpr	⊢ ( 𝑥 ∈ { ∅ , 𝐴 } ↔ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) )
16	15	a1i	⊢ ( 𝐴 ∈ Fin → ( 𝑥 ∈ { ∅ , 𝐴 } ↔ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) )
17	1	reqabi	⊢ ( 𝑥 ∈ 𝑇 ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) ) )
18		diffi	⊢ ( 𝐴 ∈ Fin → ( 𝐴 ∖ 𝑥 ) ∈ Fin )
19		biortn	⊢ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin → ( ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ↔ ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) ) )
20	18 19	syl	⊢ ( 𝐴 ∈ Fin → ( ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ↔ ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) ) )
21	20	anbi2d	⊢ ( 𝐴 ∈ Fin → ( ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) ) ) )
22	17 21	bitr4id	⊢ ( 𝐴 ∈ Fin → ( 𝑥 ∈ 𝑇 ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) ) )
23	13 16 22	3bitr4rd	⊢ ( 𝐴 ∈ Fin → ( 𝑥 ∈ 𝑇 ↔ 𝑥 ∈ { ∅ , 𝐴 } ) )
24	2 4 5 23	eqrd	⊢ ( 𝐴 ∈ Fin → 𝑇 = { ∅ , 𝐴 } )