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

Metamath Proof Explorer

Theorem cdleme31sc

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

Ref Expression
Hypotheses cdleme31sc.c ⊢ 𝐶 = ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) )
cdleme31sc.x ⊢ 𝑋 = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) )
Assertion cdleme31sc ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ 𝐶 = 𝑋 )

Proof

Step Hyp Ref Expression
1 cdleme31sc.c ⊢ 𝐶 = ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) )
2 cdleme31sc.x ⊢ 𝑋 = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) )
3 nfcvd ⊢ ( 𝑅 ∈ 𝐴 → Ⅎ 𝑠 ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) )
4 oveq1 ⊢ ( 𝑠 = 𝑅 → ( 𝑠 ∨ 𝑈 ) = ( 𝑅 ∨ 𝑈 ) )
5 oveq2 ⊢ ( 𝑠 = 𝑅 → ( 𝑃 ∨ 𝑠 ) = ( 𝑃 ∨ 𝑅 ) )
6 5 oveq1d ⊢ ( 𝑠 = 𝑅 → ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) = ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) )
7 6 oveq2d ⊢ ( 𝑠 = 𝑅 → ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) = ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) )
8 4 7 oveq12d ⊢ ( 𝑠 = 𝑅 → ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) ) = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) )
9 3 8 csbiegf ⊢ ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) ) = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) )
10 1 csbeq2i ⊢ ⦋ 𝑅 / 𝑠 ⦌ 𝐶 = ⦋ 𝑅 / 𝑠 ⦌ ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) )
11 9 10 2 3eqtr4g ⊢ ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ 𝐶 = 𝑋 )