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	⊢ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( ( 𝐴 ∖ 𝑥 ) = ∅ ∨ ( 𝐴 ∖ 𝑥 ) = 𝐴 ) ) } = { 𝑥 ∈ 𝒫 𝐴 ∣ ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) }

Proof

Step	Hyp	Ref	Expression
1		velpw	⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
2		sseqin2	⊢ ( 𝑥 ⊆ 𝐴 ↔ ( 𝐴 ∩ 𝑥 ) = 𝑥 )
3	1 2	bitri	⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ ( 𝐴 ∩ 𝑥 ) = 𝑥 )
4		eqeq1	⊢ ( ( 𝐴 ∩ 𝑥 ) = 𝑥 → ( ( 𝐴 ∩ 𝑥 ) = ∅ ↔ 𝑥 = ∅ ) )
5	3 4	sylbi	⊢ ( 𝑥 ∈ 𝒫 𝐴 → ( ( 𝐴 ∩ 𝑥 ) = ∅ ↔ 𝑥 = ∅ ) )
6		disj3	⊢ ( ( 𝐴 ∩ 𝑥 ) = ∅ ↔ 𝐴 = ( 𝐴 ∖ 𝑥 ) )
7		eqcom	⊢ ( 𝐴 = ( 𝐴 ∖ 𝑥 ) ↔ ( 𝐴 ∖ 𝑥 ) = 𝐴 )
8	6 7	bitri	⊢ ( ( 𝐴 ∩ 𝑥 ) = ∅ ↔ ( 𝐴 ∖ 𝑥 ) = 𝐴 )
9	5 8	bitr3di	⊢ ( 𝑥 ∈ 𝒫 𝐴 → ( 𝑥 = ∅ ↔ ( 𝐴 ∖ 𝑥 ) = 𝐴 ) )
10		eqss	⊢ ( 𝑥 = 𝐴 ↔ ( 𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑥 ) )
11		ssdif0	⊢ ( 𝐴 ⊆ 𝑥 ↔ ( 𝐴 ∖ 𝑥 ) = ∅ )
12	11	bicomi	⊢ ( ( 𝐴 ∖ 𝑥 ) = ∅ ↔ 𝐴 ⊆ 𝑥 )
13	1 12	anbi12i	⊢ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) = ∅ ) ↔ ( 𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑥 ) )
14	10 13	bitr4i	⊢ ( 𝑥 = 𝐴 ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ ( 𝐴 ∖ 𝑥 ) = ∅ ) )
15	14	baib	⊢ ( 𝑥 ∈ 𝒫 𝐴 → ( 𝑥 = 𝐴 ↔ ( 𝐴 ∖ 𝑥 ) = ∅ ) )
16	9 15	orbi12d	⊢ ( 𝑥 ∈ 𝒫 𝐴 → ( ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ↔ ( ( 𝐴 ∖ 𝑥 ) = 𝐴 ∨ ( 𝐴 ∖ 𝑥 ) = ∅ ) ) )
17		orcom	⊢ ( ( ( 𝐴 ∖ 𝑥 ) = 𝐴 ∨ ( 𝐴 ∖ 𝑥 ) = ∅ ) ↔ ( ( 𝐴 ∖ 𝑥 ) = ∅ ∨ ( 𝐴 ∖ 𝑥 ) = 𝐴 ) )
18	16 17	syl6bb	⊢ ( 𝑥 ∈ 𝒫 𝐴 → ( ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ↔ ( ( 𝐴 ∖ 𝑥 ) = ∅ ∨ ( 𝐴 ∖ 𝑥 ) = 𝐴 ) ) )
19	18	orbi2d	⊢ ( 𝑥 ∈ 𝒫 𝐴 → ( ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) ↔ ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( ( 𝐴 ∖ 𝑥 ) = ∅ ∨ ( 𝐴 ∖ 𝑥 ) = 𝐴 ) ) ) )
20	19	bicomd	⊢ ( 𝑥 ∈ 𝒫 𝐴 → ( ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( ( 𝐴 ∖ 𝑥 ) = ∅ ∨ ( 𝐴 ∖ 𝑥 ) = 𝐴 ) ) ↔ ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) ) )
21	20	rabbiia	⊢ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( ( 𝐴 ∖ 𝑥 ) = ∅ ∨ ( 𝐴 ∖ 𝑥 ) = 𝐴 ) ) } = { 𝑥 ∈ 𝒫 𝐴 ∣ ( ¬ ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) }