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 ⊢ E = P ∨ ˙ Q ∧ ˙ D ∨ ˙ R ∨ ˙ t ∧ ˙ W
cdleme31se2.y ⊢ Y = P ∨ ˙ Q ∧ ˙ ⦋ S / t⦌ D ∨ ˙ R ∨ ˙ S ∧ ˙ W
Assertion cdleme31se2 ⊢ S ∈ A → ⦋ S / t⦌ E = Y

Proof

Step Hyp Ref Expression
1 cdleme31se2.e ⊢ E = P ∨ ˙ Q ∧ ˙ D ∨ ˙ R ∨ ˙ t ∧ ˙ W
2 cdleme31se2.y ⊢ Y = P ∨ ˙ Q ∧ ˙ ⦋ S / t⦌ D ∨ ˙ R ∨ ˙ S ∧ ˙ W
3 nfcv ⊢ Ⅎ _ t P ∨ ˙ Q
4 nfcv ⊢ Ⅎ _ t ∧ ˙
5 nfcsb1v ⊢ Ⅎ _ t ⦋ S / t⦌ D
6 nfcv ⊢ Ⅎ _ t ∨ ˙
7 nfcv ⊢ Ⅎ _ t R ∨ ˙ S ∧ ˙ W
8 5 6 7 nfov ⊢ Ⅎ _ t ⦋ S / t⦌ D ∨ ˙ R ∨ ˙ S ∧ ˙ W
9 3 4 8 nfov ⊢ Ⅎ _ t P ∨ ˙ Q ∧ ˙ ⦋ S / t⦌ D ∨ ˙ R ∨ ˙ S ∧ ˙ W
10 9 a1i ⊢ S ∈ A → Ⅎ _ t P ∨ ˙ Q ∧ ˙ ⦋ S / t⦌ D ∨ ˙ R ∨ ˙ S ∧ ˙ W
11 csbeq1a ⊢ t = S → D = ⦋ S / t⦌ D
12 oveq2 ⊢ t = S → R ∨ ˙ t = R ∨ ˙ S
13 12 oveq1d ⊢ t = S → R ∨ ˙ t ∧ ˙ W = R ∨ ˙ S ∧ ˙ W
14 11 13 oveq12d ⊢ t = S → D ∨ ˙ R ∨ ˙ t ∧ ˙ W = ⦋ S / t⦌ D ∨ ˙ R ∨ ˙ S ∧ ˙ W
15 14 oveq2d ⊢ t = S → P ∨ ˙ Q ∧ ˙ D ∨ ˙ R ∨ ˙ t ∧ ˙ W = P ∨ ˙ Q ∧ ˙ ⦋ S / t⦌ D ∨ ˙ R ∨ ˙ S ∧ ˙ W
16 10 15 csbiegf ⊢ S ∈ A → ⦋ S / t⦌ P ∨ ˙ Q ∧ ˙ D ∨ ˙ R ∨ ˙ t ∧ ˙ W = P ∨ ˙ Q ∧ ˙ ⦋ S / t⦌ D ∨ ˙ R ∨ ˙ S ∧ ˙ W
17 1 csbeq2i ⊢ ⦋ S / t⦌ E = ⦋ S / t⦌ P ∨ ˙ Q ∧ ˙ D ∨ ˙ R ∨ ˙ t ∧ ˙ W
18 16 17 2 3eqtr4g ⊢ S ∈ A → ⦋ S / t⦌ E = Y