Step |
Hyp |
Ref |
Expression |
1 |
|
cdleme32sn2.d |
⊢ 𝐷 = ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) ) |
2 |
|
cdleme31sn2.n |
⊢ 𝑁 = if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐼 , 𝐷 ) |
3 |
|
cdleme31sn2.c |
⊢ 𝐶 = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) |
4 |
|
eqid |
⊢ if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 ) = if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 ) |
5 |
2 4
|
cdleme31sn |
⊢ ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ 𝑁 = if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 ) ) |
6 |
5
|
adantr |
⊢ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ⦋ 𝑅 / 𝑠 ⦌ 𝑁 = if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 ) ) |
7 |
|
iffalse |
⊢ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) → if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 ) = ⦋ 𝑅 / 𝑠 ⦌ 𝐷 ) |
8 |
1
|
csbeq2i |
⊢ ⦋ 𝑅 / 𝑠 ⦌ 𝐷 = ⦋ 𝑅 / 𝑠 ⦌ ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) ) |
9 |
7 8
|
eqtrdi |
⊢ ( ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) → if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 ) = ⦋ 𝑅 / 𝑠 ⦌ ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) ) ) |
10 |
|
nfcvd |
⊢ ( 𝑅 ∈ 𝐴 → Ⅎ 𝑠 ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) ) |
11 |
|
oveq1 |
⊢ ( 𝑠 = 𝑅 → ( 𝑠 ∨ 𝑈 ) = ( 𝑅 ∨ 𝑈 ) ) |
12 |
|
oveq2 |
⊢ ( 𝑠 = 𝑅 → ( 𝑃 ∨ 𝑠 ) = ( 𝑃 ∨ 𝑅 ) ) |
13 |
12
|
oveq1d |
⊢ ( 𝑠 = 𝑅 → ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) = ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) |
14 |
13
|
oveq2d |
⊢ ( 𝑠 = 𝑅 → ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) = ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) |
15 |
11 14
|
oveq12d |
⊢ ( 𝑠 = 𝑅 → ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) ) = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) ) |
16 |
10 15
|
csbiegf |
⊢ ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) ) = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) ) |
17 |
9 16
|
sylan9eqr |
⊢ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 ) = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) ) |
18 |
6 17
|
eqtrd |
⊢ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ⦋ 𝑅 / 𝑠 ⦌ 𝑁 = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) ) |
19 |
18 3
|
eqtr4di |
⊢ ( ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ⦋ 𝑅 / 𝑠 ⦌ 𝑁 = 𝐶 ) |