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

Metamath Proof Explorer

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