Theorem cdleme31id

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 18-Apr-2013)

	Ref	Expression
Hypothesis	cdleme31fv2.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ if ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊 ) , 𝑂 , 𝑥 ) )
Assertion	cdleme31id	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑃 = 𝑄 ) → ( 𝐹 ‘ 𝑋 ) = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		cdleme31fv2.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ if ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊 ) , 𝑂 , 𝑥 ) )
2		simpl	⊢ ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊 ) → 𝑃 ≠ 𝑄 )
3	2	necon2bi	⊢ ( 𝑃 = 𝑄 → ¬ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊 ) )
4	1	cdleme31fv2	⊢ ( ( 𝑋 ∈ 𝐵 ∧ ¬ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → ( 𝐹 ‘ 𝑋 ) = 𝑋 )
5	3 4	sylan2	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑃 = 𝑄 ) → ( 𝐹 ‘ 𝑋 ) = 𝑋 )