Theorem topdifinfeq

Description: Two different ways of defining the collection from Exercise 3 of Munkres p. 83. (Contributed by ML, 18-Jul-2020)

	Ref	Expression
Assertion	topdifinfeq	|- { x e. ~P A | ( -. ( A \ x ) e. Fin \/ ( ( A \ x ) = (/) \/ ( A \ x ) = A ) ) } = { x e. ~P A | ( -. ( A \ x ) e. Fin \/ ( x = (/) \/ x = A ) ) }

Proof

Step	Hyp	Ref	Expression
1		velpw	|- ( x e. ~P A <-> x C_ A )
2		sseqin2	|- ( x C_ A <-> ( A i^i x ) = x )
3	1 2	bitri	|- ( x e. ~P A <-> ( A i^i x ) = x )
4		eqeq1	|- ( ( A i^i x ) = x -> ( ( A i^i x ) = (/) <-> x = (/) ) )
5	3 4	sylbi	|- ( x e. ~P A -> ( ( A i^i x ) = (/) <-> x = (/) ) )
6		disj3	|- ( ( A i^i x ) = (/) <-> A = ( A \ x ) )
7		eqcom	|- ( A = ( A \ x ) <-> ( A \ x ) = A )
8	6 7	bitri	|- ( ( A i^i x ) = (/) <-> ( A \ x ) = A )
9	5 8	bitr3di	|- ( x e. ~P A -> ( x = (/) <-> ( A \ x ) = A ) )
10		eqss	|- ( x = A <-> ( x C_ A /\ A C_ x ) )
11		ssdif0	|- ( A C_ x <-> ( A \ x ) = (/) )
12	11	bicomi	|- ( ( A \ x ) = (/) <-> A C_ x )
13	1 12	anbi12i	|- ( ( x e. ~P A /\ ( A \ x ) = (/) ) <-> ( x C_ A /\ A C_ x ) )
14	10 13	bitr4i	|- ( x = A <-> ( x e. ~P A /\ ( A \ x ) = (/) ) )
15	14	baib	|- ( x e. ~P A -> ( x = A <-> ( A \ x ) = (/) ) )
16	9 15	orbi12d	|- ( x e. ~P A -> ( ( x = (/) \/ x = A ) <-> ( ( A \ x ) = A \/ ( A \ x ) = (/) ) ) )
17		orcom	|- ( ( ( A \ x ) = A \/ ( A \ x ) = (/) ) <-> ( ( A \ x ) = (/) \/ ( A \ x ) = A ) )
18	16 17	bitrdi	|- ( x e. ~P A -> ( ( x = (/) \/ x = A ) <-> ( ( A \ x ) = (/) \/ ( A \ x ) = A ) ) )
19	18	orbi2d	|- ( x e. ~P A -> ( ( -. ( A \ x ) e. Fin \/ ( x = (/) \/ x = A ) ) <-> ( -. ( A \ x ) e. Fin \/ ( ( A \ x ) = (/) \/ ( A \ x ) = A ) ) ) )
20	19	bicomd	|- ( x e. ~P A -> ( ( -. ( A \ x ) e. Fin \/ ( ( A \ x ) = (/) \/ ( A \ x ) = A ) ) <-> ( -. ( A \ x ) e. Fin \/ ( x = (/) \/ x = A ) ) ) )
21	20	rabbiia	|- { x e. ~P A | ( -. ( A \ x ) e. Fin \/ ( ( A \ x ) = (/) \/ ( A \ x ) = A ) ) } = { x e. ~P A | ( -. ( A \ x ) e. Fin \/ ( x = (/) \/ x = A ) ) }