Theorem cdleme31sn1 40346

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 2735	. . . 4 ⊢ if(𝑅 ≤ (𝑃 ∨ 𝑄), ⦋𝑅 / 𝑠⦌𝐼, ⦋𝑅 / 𝑠⦌𝐷) = if(𝑅 ≤ (𝑃 ∨ 𝑄), ⦋𝑅 / 𝑠⦌𝐼, ⦋𝑅 / 𝑠⦌𝐷)
3	1, 2	cdleme31sn 40345	. . 3 ⊢ (𝑅 ∈ 𝐴 → ⦋𝑅 / 𝑠⦌𝑁 = if(𝑅 ≤ (𝑃 ∨ 𝑄), ⦋𝑅 / 𝑠⦌𝐼, ⦋𝑅 / 𝑠⦌𝐷))
4	3	adantr 480	. 2 ⊢ ((𝑅 ∈ 𝐴 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ⦋𝑅 / 𝑠⦌𝑁 = if(𝑅 ≤ (𝑃 ∨ 𝑄), ⦋𝑅 / 𝑠⦌𝐼, ⦋𝑅 / 𝑠⦌𝐷))
5		iftrue 4506	. . . . 5 ⊢ (𝑅 ≤ (𝑃 ∨ 𝑄) → if(𝑅 ≤ (𝑃 ∨ 𝑄), ⦋𝑅 / 𝑠⦌𝐼, ⦋𝑅 / 𝑠⦌𝐷) = ⦋𝑅 / 𝑠⦌𝐼)
6		cdleme31sn1.i	. . . . . 6 ⊢ 𝐼 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺))
7	6	csbeq2i 3882	. . . . 5 ⊢ ⦋𝑅 / 𝑠⦌𝐼 = ⦋𝑅 / 𝑠⦌(℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺))
8	5, 7	eqtrdi 2786	. . . 4 ⊢ (𝑅 ≤ (𝑃 ∨ 𝑄) → if(𝑅 ≤ (𝑃 ∨ 𝑄), ⦋𝑅 / 𝑠⦌𝐼, ⦋𝑅 / 𝑠⦌𝐷) = ⦋𝑅 / 𝑠⦌(℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺)))
9		nfcv 2898	. . . . . . . 8 ⊢ Ⅎ𝑠𝐴
10		nfv 1914	. . . . . . . . 9 ⊢ Ⅎ𝑠(¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄))
11		nfcsb1v 3898	. . . . . . . . . 10 ⊢ Ⅎ𝑠⦋𝑅 / 𝑠⦌𝐺
12	11	nfeq2 2916	. . . . . . . . 9 ⊢ Ⅎ𝑠 𝑦 = ⦋𝑅 / 𝑠⦌𝐺
13	10, 12	nfim 1896	. . . . . . . 8 ⊢ Ⅎ𝑠((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = ⦋𝑅 / 𝑠⦌𝐺)
14	9, 13	nfralw 3291	. . . . . . 7 ⊢ Ⅎ𝑠∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = ⦋𝑅 / 𝑠⦌𝐺)
15		nfcv 2898	. . . . . . 7 ⊢ Ⅎ𝑠𝐵
16	14, 15	nfriota 7372	. . . . . 6 ⊢ Ⅎ𝑠(℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = ⦋𝑅 / 𝑠⦌𝐺))
17	16	a1i 11	. . . . 5 ⊢ (𝑅 ∈ 𝐴 → Ⅎ𝑠(℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = ⦋𝑅 / 𝑠⦌𝐺)))
18		csbeq1a 3888	. . . . . . . . 9 ⊢ (𝑠 = 𝑅 → 𝐺 = ⦋𝑅 / 𝑠⦌𝐺)
19	18	eqeq2d 2746	. . . . . . . 8 ⊢ (𝑠 = 𝑅 → (𝑦 = 𝐺 ↔ 𝑦 = ⦋𝑅 / 𝑠⦌𝐺))
20	19	imbi2d 340	. . . . . . 7 ⊢ (𝑠 = 𝑅 → (((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺) ↔ ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = ⦋𝑅 / 𝑠⦌𝐺)))
21	20	ralbidv 3163	. . . . . 6 ⊢ (𝑠 = 𝑅 → (∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺) ↔ ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = ⦋𝑅 / 𝑠⦌𝐺)))
22	21	riotabidv 7362	. . . . 5 ⊢ (𝑠 = 𝑅 → (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺)) = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = ⦋𝑅 / 𝑠⦌𝐺)))
23	17, 22	csbiegf 3907	. . . 4 ⊢ (𝑅 ∈ 𝐴 → ⦋𝑅 / 𝑠⦌(℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = 𝐺)) = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = ⦋𝑅 / 𝑠⦌𝐺)))
24	8, 23	sylan9eqr 2792	. . 3 ⊢ ((𝑅 ∈ 𝐴 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → if(𝑅 ≤ (𝑃 ∨ 𝑄), ⦋𝑅 / 𝑠⦌𝐼, ⦋𝑅 / 𝑠⦌𝐷) = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = ⦋𝑅 / 𝑠⦌𝐺)))
25		cdleme31sn1.c	. . 3 ⊢ 𝐶 = (℩𝑦 ∈ 𝐵 ∀𝑡 ∈ 𝐴 ((¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ (𝑃 ∨ 𝑄)) → 𝑦 = ⦋𝑅 / 𝑠⦌𝐺))
26	24, 25	eqtr4di 2788	. 2 ⊢ ((𝑅 ∈ 𝐴 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → if(𝑅 ≤ (𝑃 ∨ 𝑄), ⦋𝑅 / 𝑠⦌𝐼, ⦋𝑅 / 𝑠⦌𝐷) = 𝐶)
27	4, 26	eqtrd 2770	1 ⊢ ((𝑅 ∈ 𝐴 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ⦋𝑅 / 𝑠⦌𝑁 = 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  Ⅎwnfc 2883  ∀wral 3051  ⦋csb 3874  ifcif 4500   class class class wbr 5119  ℩crio 7359  (class class class)co 7403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-riota 7360

This theorem is referenced by:  cdleme31sn1c  40353