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

Metamath Proof Explorer

Theorem cdleme31sn

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 26-Feb-2013)

Ref Expression
Hypotheses cdleme31sn.n ⊢ N = if s ≤ ˙ P ∨ ˙ Q I D
cdleme31sn.c ⊢ C = if R ≤ ˙ P ∨ ˙ Q ⦋ R / s⦌ I ⦋ R / s⦌ D
Assertion cdleme31sn ⊢ R ∈ A → ⦋ R / s⦌ N = C

Proof

Step Hyp Ref Expression
1 cdleme31sn.n ⊢ N = if s ≤ ˙ P ∨ ˙ Q I D
2 cdleme31sn.c ⊢ C = if R ≤ ˙ P ∨ ˙ Q ⦋ R / s⦌ I ⦋ R / s⦌ D
3 nfv ⊢ Ⅎ s R ≤ ˙ P ∨ ˙ Q
4 nfcsb1v ⊢ Ⅎ _ s ⦋ R / s⦌ I
5 nfcsb1v ⊢ Ⅎ _ s ⦋ R / s⦌ D
6 3 4 5 nfif ⊢ Ⅎ _ s if R ≤ ˙ P ∨ ˙ Q ⦋ R / s⦌ I ⦋ R / s⦌ D
7 6 a1i ⊢ R ∈ A → Ⅎ _ s if R ≤ ˙ P ∨ ˙ Q ⦋ R / s⦌ I ⦋ R / s⦌ D
8 breq1 ⊢ s = R → s ≤ ˙ P ∨ ˙ Q ↔ R ≤ ˙ P ∨ ˙ Q
9 csbeq1a ⊢ s = R → I = ⦋ R / s⦌ I
10 csbeq1a ⊢ s = R → D = ⦋ R / s⦌ D
11 8 9 10 ifbieq12d ⊢ s = R → if s ≤ ˙ P ∨ ˙ Q I D = if R ≤ ˙ P ∨ ˙ Q ⦋ R / s⦌ I ⦋ R / s⦌ D
12 7 11 csbiegf ⊢ R ∈ A → ⦋ R / s⦌ if s ≤ ˙ P ∨ ˙ Q I D = if R ≤ ˙ P ∨ ˙ Q ⦋ R / s⦌ I ⦋ R / s⦌ D
13 1 csbeq2i ⊢ ⦋ R / s⦌ N = ⦋ R / s⦌ if s ≤ ˙ P ∨ ˙ Q I D
14 12 13 2 3eqtr4g ⊢ R ∈ A → ⦋ R / s⦌ N = C