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 ∨ ( 𝑥 = ∅ ∨ 𝑥 = 𝐴 ) ) } |