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

Metamath Proof Explorer

Theorem cdleme31se

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

Ref Expression
Hypotheses cdleme31se.e ⊢ 𝐸 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑇 ) ∧ 𝑊 ) ) )
cdleme31se.y ⊢ 𝑌 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 ) ) )
Assertion cdleme31se ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ 𝐸 = 𝑌 )

Proof

Step Hyp Ref Expression
1 cdleme31se.e ⊢ 𝐸 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑇 ) ∧ 𝑊 ) ) )
2 cdleme31se.y ⊢ 𝑌 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 ) ) )
3 nfcvd ⊢ ( 𝑅 ∈ 𝐴 → Ⅎ 𝑠 ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 ) ) ) )
4 oveq1 ⊢ ( 𝑠 = 𝑅 → ( 𝑠 ∨ 𝑇 ) = ( 𝑅 ∨ 𝑇 ) )
5 4 oveq1d ⊢ ( 𝑠 = 𝑅 → ( ( 𝑠 ∨ 𝑇 ) ∧ 𝑊 ) = ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 ) )
6 5 oveq2d ⊢ ( 𝑠 = 𝑅 → ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑇 ) ∧ 𝑊 ) ) = ( 𝐷 ∨ ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 ) ) )
7 6 oveq2d ⊢ ( 𝑠 = 𝑅 → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑇 ) ∧ 𝑊 ) ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 ) ) ) )
8 3 7 csbiegf ⊢ ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑇 ) ∧ 𝑊 ) ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 ) ) ) )
9 1 csbeq2i ⊢ ⦋ 𝑅 / 𝑠 ⦌ 𝐸 = ⦋ 𝑅 / 𝑠 ⦌ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑇 ) ∧ 𝑊 ) ) )
10 8 9 2 3eqtr4g ⊢ ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ 𝐸 = 𝑌 )