Step |
Hyp |
Ref |
Expression |
1 |
|
compss.a |
⊢ 𝐹 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑥 ) ) |
2 |
1
|
compsscnv |
⊢ ◡ 𝐹 = 𝐹 |
3 |
2
|
imaeq1i |
⊢ ( ◡ 𝐹 “ ( 𝐹 “ 𝑋 ) ) = ( 𝐹 “ ( 𝐹 “ 𝑋 ) ) |
4 |
1
|
compssiso |
⊢ ( 𝐴 ∈ 𝑉 → 𝐹 Isom [⊊] , ◡ [⊊] ( 𝒫 𝐴 , 𝒫 𝐴 ) ) |
5 |
|
isof1o |
⊢ ( 𝐹 Isom [⊊] , ◡ [⊊] ( 𝒫 𝐴 , 𝒫 𝐴 ) → 𝐹 : 𝒫 𝐴 –1-1-onto→ 𝒫 𝐴 ) |
6 |
|
f1of1 |
⊢ ( 𝐹 : 𝒫 𝐴 –1-1-onto→ 𝒫 𝐴 → 𝐹 : 𝒫 𝐴 –1-1→ 𝒫 𝐴 ) |
7 |
4 5 6
|
3syl |
⊢ ( 𝐴 ∈ 𝑉 → 𝐹 : 𝒫 𝐴 –1-1→ 𝒫 𝐴 ) |
8 |
|
f1imacnv |
⊢ ( ( 𝐹 : 𝒫 𝐴 –1-1→ 𝒫 𝐴 ∧ 𝑋 ⊆ 𝒫 𝐴 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑋 ) ) = 𝑋 ) |
9 |
7 8
|
sylan |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴 ) → ( ◡ 𝐹 “ ( 𝐹 “ 𝑋 ) ) = 𝑋 ) |
10 |
3 9
|
eqtr3id |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴 ) → ( 𝐹 “ ( 𝐹 “ 𝑋 ) ) = 𝑋 ) |