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

Metamath Proof Explorer

Theorem cdleme31fv2

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

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

Proof

Step Hyp Ref Expression
1 cdleme31fv2.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ if ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊 ) , 𝑂 , 𝑥 ) )
2 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ≤ 𝑊 ↔ 𝑋 ≤ 𝑊 ) )
3 2 notbid ⊢ ( 𝑥 = 𝑋 → ( ¬ 𝑥 ≤ 𝑊 ↔ ¬ 𝑋 ≤ 𝑊 ) )
4 3 anbi2d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊 ) ↔ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊 ) ) )
5 4 notbid ⊢ ( 𝑥 = 𝑋 → ( ¬ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊 ) ↔ ¬ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊 ) ) )
6 5 biimparc ⊢ ( ( ¬ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊 ) ∧ 𝑥 = 𝑋 ) → ¬ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊 ) )
7 6 adantll ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ ¬ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ 𝑥 = 𝑋 ) → ¬ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊 ) )
8 7 iffalsed ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ ¬ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ 𝑥 = 𝑋 ) → if ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊 ) , 𝑂 , 𝑥 ) = 𝑥 )
9 simpr ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ ¬ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
10 8 9 eqtrd ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ ¬ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊 ) ) ∧ 𝑥 = 𝑋 ) → if ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊 ) , 𝑂 , 𝑥 ) = 𝑋 )
11 simpl ⊢ ( ( 𝑋 ∈ 𝐵 ∧ ¬ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → 𝑋 ∈ 𝐵 )
12 1 10 11 11 fvmptd2 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ ¬ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → ( 𝐹 ‘ 𝑋 ) = 𝑋 )