Metamath Proof Explorer

Theorem cdleme31sde

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

Ref Expression
Hypotheses cdleme31sde.c ⊢ 𝐷 = ( ( 𝑡 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑡 ) ∧ 𝑊 ) ) )
cdleme31sde.e ⊢ 𝐸 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑡 ) ∧ 𝑊 ) ) )
cdleme31sde.x ⊢ 𝑌 = ( ( 𝑆 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) )
cdleme31sde.z ⊢ 𝑍 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑌 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) )
Assertion cdleme31sde ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ⦋ 𝑅 / 𝑠 ⦌ ⦋ 𝑆 / 𝑡 ⦌ 𝐸 = 𝑍 )

Proof

Step Hyp Ref Expression
1 cdleme31sde.c ⊢ 𝐷 = ( ( 𝑡 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑡 ) ∧ 𝑊 ) ) )
2 cdleme31sde.e ⊢ 𝐸 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑡 ) ∧ 𝑊 ) ) )
3 cdleme31sde.x ⊢ 𝑌 = ( ( 𝑆 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) )
4 cdleme31sde.z ⊢ 𝑍 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑌 ∨ ( ( 𝑅 ∨ 𝑆 ) ∧ 𝑊 ) ) )
5 2 csbeq2i ⊢ ⦋ 𝑆 / 𝑡 ⦌ 𝐸 = ⦋ 𝑆 / 𝑡 ⦌ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑡 ) ∧ 𝑊 ) ) )
6 nfcvd ⊢ ( 𝑆 ∈ 𝐴 → Ⅎ 𝑡 ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑌 ∨ ( ( 𝑠 ∨ 𝑆 ) ∧ 𝑊 ) ) ) )
7 oveq1 ⊢ ( 𝑡 = 𝑆 → ( 𝑡 ∨ 𝑈 ) = ( 𝑆 ∨ 𝑈 ) )
8 oveq2 ⊢ ( 𝑡 = 𝑆 → ( 𝑃 ∨ 𝑡 ) = ( 𝑃 ∨ 𝑆 ) )
9 8 oveq1d ⊢ ( 𝑡 = 𝑆 → ( ( 𝑃 ∨ 𝑡 ) ∧ 𝑊 ) = ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) )
10 9 oveq2d ⊢ ( 𝑡 = 𝑆 → ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑡 ) ∧ 𝑊 ) ) = ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) )
11 7 10 oveq12d ⊢ ( 𝑡 = 𝑆 → ( ( 𝑡 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑡 ) ∧ 𝑊 ) ) ) = ( ( 𝑆 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ) ) )
12 11 1 3 3eqtr4g ⊢ ( 𝑡 = 𝑆 → 𝐷 = 𝑌 )
13 oveq2 ⊢ ( 𝑡 = 𝑆 → ( 𝑠 ∨ 𝑡 ) = ( 𝑠 ∨ 𝑆 ) )
14 13 oveq1d ⊢ ( 𝑡 = 𝑆 → ( ( 𝑠 ∨ 𝑡 ) ∧ 𝑊 ) = ( ( 𝑠 ∨ 𝑆 ) ∧ 𝑊 ) )
15 12 14 oveq12d ⊢ ( 𝑡 = 𝑆 → ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑡 ) ∧ 𝑊 ) ) = ( 𝑌 ∨ ( ( 𝑠 ∨ 𝑆 ) ∧ 𝑊 ) ) )
16 15 oveq2d ⊢ ( 𝑡 = 𝑆 → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑡 ) ∧ 𝑊 ) ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑌 ∨ ( ( 𝑠 ∨ 𝑆 ) ∧ 𝑊 ) ) ) )
17 6 16 csbiegf ⊢ ( 𝑆 ∈ 𝐴 → ⦋ 𝑆 / 𝑡 ⦌ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑡 ) ∧ 𝑊 ) ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑌 ∨ ( ( 𝑠 ∨ 𝑆 ) ∧ 𝑊 ) ) ) )
18 5 17 eqtrid ⊢ ( 𝑆 ∈ 𝐴 → ⦋ 𝑆 / 𝑡 ⦌ 𝐸 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑌 ∨ ( ( 𝑠 ∨ 𝑆 ) ∧ 𝑊 ) ) ) )
19 18 csbeq2dv ⊢ ( 𝑆 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ ⦋ 𝑆 / 𝑡 ⦌ 𝐸 = ⦋ 𝑅 / 𝑠 ⦌ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑌 ∨ ( ( 𝑠 ∨ 𝑆 ) ∧ 𝑊 ) ) ) )
20 eqid ⊢ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑌 ∨ ( ( 𝑠 ∨ 𝑆 ) ∧ 𝑊 ) ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑌 ∨ ( ( 𝑠 ∨ 𝑆 ) ∧ 𝑊 ) ) )
21 20 4 cdleme31se ⊢ ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑌 ∨ ( ( 𝑠 ∨ 𝑆 ) ∧ 𝑊 ) ) ) = 𝑍 )
22 19 21 sylan9eqr ⊢ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ) → ⦋ 𝑅 / 𝑠 ⦌ ⦋ 𝑆 / 𝑡 ⦌ 𝐸 = 𝑍 )