Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 31-Mar-2013) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | cdleme31sdn.c | ⊢ 𝐶 = ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) ) | |
| cdleme31sdn.d | ⊢ 𝐷 = ( ( 𝑡 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑡 ) ∧ 𝑊 ) ) ) | ||
| cdleme31sdn.n | ⊢ 𝑁 = if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐼 , 𝐶 ) | ||
| Assertion | cdleme31sdnN | ⊢ 𝑁 = if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐼 , ⦋ 𝑠 / 𝑡 ⦌ 𝐷 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cdleme31sdn.c | ⊢ 𝐶 = ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) ) | |
| 2 | cdleme31sdn.d | ⊢ 𝐷 = ( ( 𝑡 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑡 ) ∧ 𝑊 ) ) ) | |
| 3 | cdleme31sdn.n | ⊢ 𝑁 = if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐼 , 𝐶 ) | |
| 4 | biid | ⊢ ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) ↔ 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) ) | |
| 5 | 2 1 | cdleme31sc | ⊢ ( 𝑠 ∈ V → ⦋ 𝑠 / 𝑡 ⦌ 𝐷 = 𝐶 ) |
| 6 | 5 | elv | ⊢ ⦋ 𝑠 / 𝑡 ⦌ 𝐷 = 𝐶 |
| 7 | 4 6 | ifbieq2i | ⊢ if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐼 , ⦋ 𝑠 / 𝑡 ⦌ 𝐷 ) = if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐼 , 𝐶 ) |
| 8 | 3 7 | eqtr4i | ⊢ 𝑁 = if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐼 , ⦋ 𝑠 / 𝑡 ⦌ 𝐷 ) |