Metamath Proof Explorer

Theorem cdleme31sn1

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

Ref Expression
Hypotheses cdleme31sn1.i ⊢ 𝐼 = ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = 𝐺 ) )
cdleme31sn1.n ⊢ 𝑁 = if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐼 , 𝐷 )
cdleme31sn1.c ⊢ 𝐶 = ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = ⦋ 𝑅 / 𝑠 ⦌ 𝐺 ) )
Assertion cdleme31sn1 ( ( 𝑅 ∈ 𝐴 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ⦋ 𝑅 / 𝑠 ⦌ 𝑁 = 𝐶 )

Proof

Step Hyp Ref Expression
1 cdleme31sn1.i ⊢ 𝐼 = ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = 𝐺 ) )
2 cdleme31sn1.n ⊢ 𝑁 = if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐼 , 𝐷 )
3 cdleme31sn1.c ⊢ 𝐶 = ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = ⦋ 𝑅 / 𝑠 ⦌ 𝐺 ) )
4 eqid ⊢ if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 ) = if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 )
5 2 4 cdleme31sn ⊢ ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ 𝑁 = if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 ) )
6 5 adantr ⊢ ( ( 𝑅 ∈ 𝐴 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ⦋ 𝑅 / 𝑠 ⦌ 𝑁 = if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 ) )
7 iftrue ⊢ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) → if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 ) = ⦋ 𝑅 / 𝑠 ⦌ 𝐼 )
8 1 csbeq2i ⊢ ⦋ 𝑅 / 𝑠 ⦌ 𝐼 = ⦋ 𝑅 / 𝑠 ⦌ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = 𝐺 ) )
9 7 8 eqtrdi ⊢ ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) → if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 ) = ⦋ 𝑅 / 𝑠 ⦌ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = 𝐺 ) ) )
10 nfcv ⊢ Ⅎ 𝑠 𝐴
11 nfv ⊢ Ⅎ 𝑠 ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) )
12 nfcsb1v ⊢ Ⅎ 𝑠 ⦋ 𝑅 / 𝑠 ⦌ 𝐺
13 12 nfeq2 ⊢ Ⅎ 𝑠 𝑦 = ⦋ 𝑅 / 𝑠 ⦌ 𝐺
14 11 13 nfim ⊢ Ⅎ 𝑠 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = ⦋ 𝑅 / 𝑠 ⦌ 𝐺 )
15 10 14 nfralw ⊢ Ⅎ 𝑠 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = ⦋ 𝑅 / 𝑠 ⦌ 𝐺 )
16 nfcv ⊢ Ⅎ 𝑠 𝐵
17 15 16 nfriota ⊢ Ⅎ 𝑠 ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = ⦋ 𝑅 / 𝑠 ⦌ 𝐺 ) )
18 17 a1i ⊢ ( 𝑅 ∈ 𝐴 → Ⅎ 𝑠 ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = ⦋ 𝑅 / 𝑠 ⦌ 𝐺 ) ) )
19 csbeq1a ⊢ ( 𝑠 = 𝑅 → 𝐺 = ⦋ 𝑅 / 𝑠 ⦌ 𝐺 )
20 19 eqeq2d ⊢ ( 𝑠 = 𝑅 → ( 𝑦 = 𝐺 ↔ 𝑦 = ⦋ 𝑅 / 𝑠 ⦌ 𝐺 ) )
21 20 imbi2d ⊢ ( 𝑠 = 𝑅 → ( ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = 𝐺 ) ↔ ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = ⦋ 𝑅 / 𝑠 ⦌ 𝐺 ) ) )
22 21 ralbidv ⊢ ( 𝑠 = 𝑅 → ( ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = 𝐺 ) ↔ ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = ⦋ 𝑅 / 𝑠 ⦌ 𝐺 ) ) )
23 22 riotabidv ⊢ ( 𝑠 = 𝑅 → ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = 𝐺 ) ) = ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = ⦋ 𝑅 / 𝑠 ⦌ 𝐺 ) ) )
24 18 23 csbiegf ⊢ ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = 𝐺 ) ) = ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = ⦋ 𝑅 / 𝑠 ⦌ 𝐺 ) ) )
25 9 24 sylan9eqr ⊢ ( ( 𝑅 ∈ 𝐴 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 ) = ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑦 = ⦋ 𝑅 / 𝑠 ⦌ 𝐺 ) ) )
26 25 3 eqtr4di ⊢ ( ( 𝑅 ∈ 𝐴 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → if ( 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) , ⦋ 𝑅 / 𝑠 ⦌ 𝐼 , ⦋ 𝑅 / 𝑠 ⦌ 𝐷 ) = 𝐶 )
27 6 26 eqtrd ⊢ ( ( 𝑅 ∈ 𝐴 ∧ 𝑅 ≤ ( 𝑃 ∨ 𝑄 ) ) → ⦋ 𝑅 / 𝑠 ⦌ 𝑁 = 𝐶 )