This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isf34lem3

Description: Lemma for isfin3-4 . (Contributed by Stefan O'Rear, 7-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

Ref Expression
Hypothesis compss.a ⊢ 𝐹 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑥 ) )
Assertion isf34lem3 ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴 ) → ( 𝐹 “ ( 𝐹 “ 𝑋 ) ) = 𝑋 )

Proof

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 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ⊆ 𝒫 𝐴 ) → ( 𝐹 “ ( 𝐹 “ 𝑋 ) ) = 𝑋 )