Theorem cdleme31sn

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

	Ref	Expression
Hypotheses	cdleme31sn.n	⊢ 𝑁 = if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐼 , 𝐷 )
	cdleme31sn.c	⊢ 𝐶 = if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 )
Assertion	cdleme31sn	⊢ ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ 𝑁 = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		cdleme31sn.n	⊢ 𝑁 = if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐼 , 𝐷 )
2		cdleme31sn.c	⊢ 𝐶 = if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 )
3		nfv	⊢ Ⅎ 𝑠 𝑅 ≤ ( 𝑃 ∨ 𝑄 )
4		nfcsb1v	⊢ Ⅎ 𝑠 ⦋ 𝑅 / 𝑠 ⦌ 𝐼
5		nfcsb1v	⊢ Ⅎ 𝑠 ⦋ 𝑅 / 𝑠 ⦌ 𝐷
6	3 4 5	nfif	⊢ Ⅎ 𝑠 if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 )
7	6	a1i	⊢ ( 𝑅 ∈ 𝐴 → Ⅎ 𝑠 if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 ) )
8		breq1	⊢ ( 𝑠 = 𝑅 → ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) ↔ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) )
9		csbeq1a	⊢ ( 𝑠 = 𝑅 → 𝐼 = ⦋ 𝑅 / 𝑠 ⦌ 𝐼 )
10		csbeq1a	⊢ ( 𝑠 = 𝑅 → 𝐷 = ⦋ 𝑅 / 𝑠 ⦌ 𝐷 )
11	8 9 10	ifbieq12d	⊢ ( 𝑠 = 𝑅 → if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐼 , 𝐷 ) = if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 ) )
12	7 11	csbiegf	⊢ ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐼 , 𝐷 ) = if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 ) )
13	1	csbeq2i	⊢ ⦋ 𝑅 / 𝑠 ⦌ 𝑁 = ⦋ 𝑅 / 𝑠 ⦌ if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐼 , 𝐷 )
14	12 13 2	3eqtr4g	⊢ ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ 𝑁 = 𝐶 )