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 → 𝑇 = { ∅ , 𝐴 } ) |