Theorem cdleme31snd

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

	Ref	Expression
Hypotheses	cdleme31snd.d	⊢ 𝐷 = ( ( 𝑡 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑡 ) ∧ 𝑊 ) ) )
	cdleme31snd.n	⊢ 𝑁 = ( ( 𝑣 ∨ 𝑉 ) ∧ ( 𝑃 ∨ ( ( 𝑄 ∨ 𝑣 ) ∧ 𝑊 ) ) )
	cdleme31snd.e	⊢ 𝐸 = ( ( 𝑂 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑂 ) ∧ 𝑊 ) ) )
	cdleme31snd.o	⊢ 𝑂 = ( ( 𝑆 ∨ 𝑉 ) ∧ ( 𝑃 ∨ ( ( 𝑄 ∨ 𝑆 ) ∧ 𝑊 ) ) )
Assertion	cdleme31snd	⊢ ( 𝑆 ∈ 𝐴 → ⦋ 𝑆 / 𝑣 ⦌ ⦋ 𝑁 / 𝑡 ⦌ 𝐷 = 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		cdleme31snd.d	⊢ 𝐷 = ( ( 𝑡 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑡 ) ∧ 𝑊 ) ) )
2		cdleme31snd.n	⊢ 𝑁 = ( ( 𝑣 ∨ 𝑉 ) ∧ ( 𝑃 ∨ ( ( 𝑄 ∨ 𝑣 ) ∧ 𝑊 ) ) )
3		cdleme31snd.e	⊢ 𝐸 = ( ( 𝑂 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑂 ) ∧ 𝑊 ) ) )
4		cdleme31snd.o	⊢ 𝑂 = ( ( 𝑆 ∨ 𝑉 ) ∧ ( 𝑃 ∨ ( ( 𝑄 ∨ 𝑆 ) ∧ 𝑊 ) ) )
5		csbnestgw	⊢ ( 𝑆 ∈ 𝐴 → ⦋ 𝑆 / 𝑣 ⦌ ⦋ 𝑁 / 𝑡 ⦌ 𝐷 = ⦋ ⦋ 𝑆 / 𝑣 ⦌ 𝑁 / 𝑡 ⦌ 𝐷 )
6	2 4	cdleme31sc	⊢ ( 𝑆 ∈ 𝐴 → ⦋ 𝑆 / 𝑣 ⦌ 𝑁 = 𝑂 )
7	6	csbeq1d	⊢ ( 𝑆 ∈ 𝐴 → ⦋ ⦋ 𝑆 / 𝑣 ⦌ 𝑁 / 𝑡 ⦌ 𝐷 = ⦋ 𝑂 / 𝑡 ⦌ 𝐷 )
8	4	ovexi	⊢ 𝑂 ∈ V
9	1 3	cdleme31sc	⊢ ( 𝑂 ∈ V → ⦋ 𝑂 / 𝑡 ⦌ 𝐷 = 𝐸 )
10	8 9	ax-mp	⊢ ⦋ 𝑂 / 𝑡 ⦌ 𝐷 = 𝐸
11	7 10	eqtrdi	⊢ ( 𝑆 ∈ 𝐴 → ⦋ ⦋ 𝑆 / 𝑣 ⦌ 𝑁 / 𝑡 ⦌ 𝐷 = 𝐸 )
12	5 11	eqtrd	⊢ ( 𝑆 ∈ 𝐴 → ⦋ 𝑆 / 𝑣 ⦌ ⦋ 𝑁 / 𝑡 ⦌ 𝐷 = 𝐸 )