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	⊢ ( 𝑆 ∈ 𝐴 → ⦋ 𝑆 / 𝑡 ⦌ 𝐸 = 𝑌 )