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

Metamath Proof Explorer

Theorem cdleme31fv1

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

Ref Expression
Hypotheses cdleme31.o ⊢ 𝑂 = ( ℩ 𝑧 ∈ 𝐵 ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑥 ∧ 𝑊 ) ) = 𝑥 ) → 𝑧 = ( 𝑁 ∨ ( 𝑥 ∧ 𝑊 ) ) ) )
cdleme31.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ if ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊 ) , 𝑂 , 𝑥 ) )
cdleme31.c ⊢ 𝐶 = ( ℩ 𝑧 ∈ 𝐵 ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → 𝑧 = ( 𝑁 ∨ ( 𝑋 ∧ 𝑊 ) ) ) )
Assertion cdleme31fv1 ( ( 𝑋 ∈ 𝐵 ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → ( 𝐹 ‘ 𝑋 ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 cdleme31.o ⊢ 𝑂 = ( ℩ 𝑧 ∈ 𝐵 ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑥 ∧ 𝑊 ) ) = 𝑥 ) → 𝑧 = ( 𝑁 ∨ ( 𝑥 ∧ 𝑊 ) ) ) )
2 cdleme31.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ if ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑥 ≤ 𝑊 ) , 𝑂 , 𝑥 ) )
3 cdleme31.c ⊢ 𝐶 = ( ℩ 𝑧 ∈ 𝐵 ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑋 ∧ 𝑊 ) ) = 𝑋 ) → 𝑧 = ( 𝑁 ∨ ( 𝑋 ∧ 𝑊 ) ) ) )
4 1 2 3 cdleme31fv ⊢ ( 𝑋 ∈ 𝐵 → ( 𝐹 ‘ 𝑋 ) = if ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊 ) , 𝐶 , 𝑋 ) )
5 iftrue ⊢ ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊 ) → if ( ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊 ) , 𝐶 , 𝑋 ) = 𝐶 )
6 4 5 sylan9eq ⊢ ( ( 𝑋 ∈ 𝐵 ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → ( 𝐹 ‘ 𝑋 ) = 𝐶 )