Theorem cdleme31sn1 39247

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

Hypotheses

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

Assertion

Ref	Expression
cdleme31sn1	⊢ ((𝑅 ∈ 𝐴 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ⦋𝑅 / 𝑠⦌𝑁 = 𝐶)

Distinct variable groups:   𝑡,𝑠,𝑦,𝐴   𝐵,𝑠   ∨ ,𝑠   ≤ ,𝑠   𝑃,𝑠   𝑄,𝑠   𝑅,𝑠,𝑡,𝑦   𝑊,𝑠

Allowed substitution hints:   𝐵(𝑦,𝑡)   𝐶(𝑦,𝑡,𝑠)   𝐷(𝑦,𝑡,𝑠)   𝑃(𝑦,𝑡)   𝑄(𝑦,𝑡)   𝐺(𝑦,𝑡,𝑠)   𝐼(𝑦,𝑡,𝑠)   ∨ (𝑦,𝑡)   ≤ (𝑦,𝑡)   𝑁(𝑦,𝑡,𝑠)   𝑊(𝑦,𝑡)

Proof of Theorem cdleme31sn1

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  Ⅎwnfc 2883  ∀wral 3061  ⦋csb 3893  ifcif 4528   class class class wbr 5148  ℩crio 7363  (class class class)co 7408

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-riota 7364

This theorem is referenced by:  cdleme31sn1c  39254