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