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

Metamath Proof Explorer

Theorem cdleme31se2

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

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

Proof

Step Hyp Ref Expression
1 cdleme31se2.e ⊢ 𝐸 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑅 ∨ 𝑡 ) ∧ 𝑊 ) ) )
2 cdleme31se2.y ⊢ 𝑌 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( ⦋ 𝑆 / 𝑡 ⦌ 𝐷 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) )
3 nfcv ⊢ Ⅎ 𝑡 ( 𝑃 ∨ 𝑄 )
4 nfcv ⊢ Ⅎ 𝑡 ∧
5 nfcsb1v ⊢ Ⅎ 𝑡 ⦋ 𝑆 / 𝑡 ⦌ 𝐷
6 nfcv ⊢ Ⅎ 𝑡 ∨
7 nfcv ⊢ Ⅎ 𝑡 ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 )
8 5 6 7 nfov ⊢ Ⅎ 𝑡 ( ⦋ 𝑆 / 𝑡 ⦌ 𝐷 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) )
9 3 4 8 nfov ⊢ Ⅎ 𝑡 ( ( 𝑃 ∨ 𝑄 ) ∧ ( ⦋ 𝑆 / 𝑡 ⦌ 𝐷 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) )
10 9 a1i ⊢ ( 𝑆 ∈ 𝐴 → Ⅎ 𝑡 ( ( 𝑃 ∨ 𝑄 ) ∧ ( ⦋ 𝑆 / 𝑡 ⦌ 𝐷 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) ) )
11 csbeq1a ⊢ ( 𝑡 = 𝑆 → 𝐷 = ⦋ 𝑆 / 𝑡 ⦌ 𝐷 )
12 oveq2 ⊢ ( 𝑡 = 𝑆 → ( 𝑅 ∨ 𝑡 ) = ( 𝑅 ∨ 𝑆 ) )
13 12 oveq1d ⊢ ( 𝑡 = 𝑆 → ( ( 𝑅 ∨ 𝑡 ) ∧ 𝑊 ) = ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) )
14 11 13 oveq12d ⊢ ( 𝑡 = 𝑆 → ( 𝐷 ∨ ( ( 𝑅 ∨ 𝑡 ) ∧ 𝑊 ) ) = ( ⦋ 𝑆 / 𝑡 ⦌ 𝐷 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) )
15 14 oveq2d ⊢ ( 𝑡 = 𝑆 → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑅 ∨ 𝑡 ) ∧ 𝑊 ) ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( ⦋ 𝑆 / 𝑡 ⦌ 𝐷 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) ) )
16 10 15 csbiegf ⊢ ( 𝑆 ∈ 𝐴 → ⦋ 𝑆 / 𝑡 ⦌ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑅 ∨ 𝑡 ) ∧ 𝑊 ) ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( ⦋ 𝑆 / 𝑡 ⦌ 𝐷 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) ) )
17 1 csbeq2i ⊢ ⦋ 𝑆 / 𝑡 ⦌ 𝐸 = ⦋ 𝑆 / 𝑡 ⦌ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑅 ∨ 𝑡 ) ∧ 𝑊 ) ) )
18 16 17 2 3eqtr4g ⊢ ( 𝑆 ∈ 𝐴 → ⦋ 𝑆 / 𝑡 ⦌ 𝐸 = 𝑌 )