Metamath Proof Explorer


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 rabeq2i ( 𝑥𝑇 ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( ¬ ( 𝐴𝑥 ) ∈ 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 → 𝑇 = { ∅ , 𝐴 } )