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

Metamath Proof Explorer

Theorem cdleme31sn2

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

Ref Expression
Hypotheses cdleme32sn2.d ⊢ 𝐷 = ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) )
cdleme31sn2.n ⊢ 𝑁 = if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐼 , 𝐷 )
cdleme31sn2.c ⊢ 𝐶 = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) )
Assertion cdleme31sn2 ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ⦋ 𝑅 / 𝑠 ⦌ 𝑁 = 𝐶 )

Proof

Step Hyp Ref Expression
1 cdleme32sn2.d ⊢ 𝐷 = ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) )
2 cdleme31sn2.n ⊢ 𝑁 = if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐼 , 𝐷 )
3 cdleme31sn2.c ⊢ 𝐶 = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) )
4 eqid ⊢ if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 ) = if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 )
5 2 4 cdleme31sn ⊢ ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ 𝑁 = if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 ) )
6 5 adantr ⊢ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ⦋ 𝑅 / 𝑠 ⦌ 𝑁 = if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 ) )
7 iffalse ⊢ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) → if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 ) = ⦋ 𝑅 / 𝑠 ⦌ 𝐷 )
8 1 csbeq2i ⊢ ⦋ 𝑅 / 𝑠 ⦌ 𝐷 = ⦋ 𝑅 / 𝑠 ⦌ ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) )
9 7 8 eqtrdi ⊢ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) → if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 ) = ⦋ 𝑅 / 𝑠 ⦌ ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) ) )
10 nfcvd ⊢ ( 𝑅 ∈ 𝐴 → Ⅎ 𝑠 ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) )
11 oveq1 ⊢ ( 𝑠 = 𝑅 → ( 𝑠 ∨ 𝑈 ) = ( 𝑅 ∨ 𝑈 ) )
12 oveq2 ⊢ ( 𝑠 = 𝑅 → ( 𝑃 ∨ 𝑠 ) = ( 𝑃 ∨ 𝑅 ) )
13 12 oveq1d ⊢ ( 𝑠 = 𝑅 → ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) = ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) )
14 13 oveq2d ⊢ ( 𝑠 = 𝑅 → ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) = ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) )
15 11 14 oveq12d ⊢ ( 𝑠 = 𝑅 → ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) ) = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) )
16 10 15 csbiegf ⊢ ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) ) = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) )
17 9 16 sylan9eqr ⊢ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 ) = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) )
18 6 17 eqtrd ⊢ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ⦋ 𝑅 / 𝑠 ⦌ 𝑁 = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) )
19 18 3 eqtr4di ⊢ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ⦋ 𝑅 / 𝑠 ⦌ 𝑁 = 𝐶 )