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 ⊢ D = t ∨ ˙ U ∧ ˙ Q ∨ ˙ P ∨ ˙ t ∧ ˙ W
cdleme31snd.n ⊢ N = v ∨ ˙ V ∧ ˙ P ∨ ˙ Q ∨ ˙ v ∧ ˙ W
cdleme31snd.e ⊢ E = O ∨ ˙ U ∧ ˙ Q ∨ ˙ P ∨ ˙ O ∧ ˙ W
cdleme31snd.o ⊢ O = S ∨ ˙ V ∧ ˙ P ∨ ˙ Q ∨ ˙ S ∧ ˙ W
Assertion cdleme31snd ⊢ S ∈ A → ⦋ S / v⦌ ⦋ N / t⦌ D = E

Proof

Step Hyp Ref Expression
1 cdleme31snd.d ⊢ D = t ∨ ˙ U ∧ ˙ Q ∨ ˙ P ∨ ˙ t ∧ ˙ W
2 cdleme31snd.n ⊢ N = v ∨ ˙ V ∧ ˙ P ∨ ˙ Q ∨ ˙ v ∧ ˙ W
3 cdleme31snd.e ⊢ E = O ∨ ˙ U ∧ ˙ Q ∨ ˙ P ∨ ˙ O ∧ ˙ W
4 cdleme31snd.o ⊢ O = S ∨ ˙ V ∧ ˙ P ∨ ˙ Q ∨ ˙ S ∧ ˙ W
5 csbnestgw ⊢ S ∈ A → ⦋ S / v⦌ ⦋ N / t⦌ D = ⦋ ⦋ S / v⦌ N / t⦌ D
6 2 4 cdleme31sc ⊢ S ∈ A → ⦋ S / v⦌ N = O
7 6 csbeq1d ⊢ S ∈ A → ⦋ ⦋ S / v⦌ N / t⦌ D = ⦋ O / t⦌ D
8 4 ovexi ⊢ O ∈ V
9 1 3 cdleme31sc ⊢ O ∈ V → ⦋ O / t⦌ D = E
10 8 9 ax-mp ⊢ ⦋ O / t⦌ D = E
11 7 10 eqtrdi ⊢ S ∈ A → ⦋ ⦋ S / v⦌ N / t⦌ D = E
12 5 11 eqtrd ⊢ S ∈ A → ⦋ S / v⦌ ⦋ N / t⦌ D = E