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 
|- T = { x e. ~P A | ( -. ( A \ x ) e. Fin \/ ( x = (/) \/ x = A ) ) }
Assertion topdifinfindis 
|- ( A e. Fin -> T = { (/) , A } )

Proof

Step Hyp Ref Expression
1 topdifinf.t 
 |-  T = { x e. ~P A | ( -. ( A \ x ) e. Fin \/ ( x = (/) \/ x = A ) ) }
2 nfv 
 |-  F/ x A e. Fin
3 nfrab1 
 |-  F/_ x { x e. ~P A | ( -. ( A \ x ) e. Fin \/ ( x = (/) \/ x = A ) ) }
4 1 3 nfcxfr 
 |-  F/_ x T
5 nfcv 
 |-  F/_ x { (/) , A }
6 0elpw 
 |-  (/) e. ~P A
7 eleq1a 
 |-  ( (/) e. ~P A -> ( x = (/) -> x e. ~P A ) )
8 6 7 mp1i 
 |-  ( A e. Fin -> ( x = (/) -> x e. ~P A ) )
9 pwidg 
 |-  ( A e. Fin -> A e. ~P A )
10 eleq1a 
 |-  ( A e. ~P A -> ( x = A -> x e. ~P A ) )
11 9 10 syl 
 |-  ( A e. Fin -> ( x = A -> x e. ~P A ) )
12 8 11 jaod 
 |-  ( A e. Fin -> ( ( x = (/) \/ x = A ) -> x e. ~P A ) )
13 12 pm4.71rd 
 |-  ( A e. Fin -> ( ( x = (/) \/ x = A ) <-> ( x e. ~P A /\ ( x = (/) \/ x = A ) ) ) )
14 vex 
 |-  x e. _V
15 14 elpr 
 |-  ( x e. { (/) , A } <-> ( x = (/) \/ x = A ) )
16 15 a1i 
 |-  ( A e. Fin -> ( x e. { (/) , A } <-> ( x = (/) \/ x = A ) ) )
17 1 rabeq2i 
 |-  ( x e. T <-> ( x e. ~P A /\ ( -. ( A \ x ) e. Fin \/ ( x = (/) \/ x = A ) ) ) )
18 diffi 
 |-  ( A e. Fin -> ( A \ x ) e. Fin )
19 biortn 
 |-  ( ( A \ x ) e. Fin -> ( ( x = (/) \/ x = A ) <-> ( -. ( A \ x ) e. Fin \/ ( x = (/) \/ x = A ) ) ) )
20 18 19 syl 
 |-  ( A e. Fin -> ( ( x = (/) \/ x = A ) <-> ( -. ( A \ x ) e. Fin \/ ( x = (/) \/ x = A ) ) ) )
21 20 anbi2d 
 |-  ( A e. Fin -> ( ( x e. ~P A /\ ( x = (/) \/ x = A ) ) <-> ( x e. ~P A /\ ( -. ( A \ x ) e. Fin \/ ( x = (/) \/ x = A ) ) ) ) )
22 17 21 bitr4id 
 |-  ( A e. Fin -> ( x e. T <-> ( x e. ~P A /\ ( x = (/) \/ x = A ) ) ) )
23 13 16 22 3bitr4rd 
 |-  ( A e. Fin -> ( x e. T <-> x e. { (/) , A } ) )
24 2 4 5 23 eqrd 
 |-  ( A e. Fin -> T = { (/) , A } )