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

Metamath Proof Explorer

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 ⊢ ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ 𝑁 = 𝐶 )