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	⊢ ( ( 𝑋 ∈ 𝐵 ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑋 ≤ 𝑊 ) ) → ( 𝐹 ‘ 𝑋 ) = 𝐶 )