Theorem cdleme25cv 38066

Description: Change bound variables in cdleme25c 38063. (Contributed by NM, 2-Feb-2013.)

Hypotheses

Ref	Expression
cdleme25cv.f	⊢ 𝐹 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊)))
cdleme25cv.n	⊢ 𝑁 = ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))
cdleme25cv.g	⊢ 𝐺 = ((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊)))
cdleme25cv.o	⊢ 𝑂 = ((𝑃 ∨ 𝑄) ∧ (𝐺 ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))
cdleme25cv.i	⊢ 𝐼 = (℩𝑢 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁))
cdleme25cv.e	⊢ 𝐸 = (℩𝑢 ∈ 𝐵 ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂))

Assertion

Ref	Expression
cdleme25cv	⊢ 𝐼 = 𝐸

Distinct variable groups:   𝑧,𝑠,𝐴   ∨ ,𝑠,𝑧   ≤ ,𝑠,𝑧   ∧ ,𝑠,𝑧   𝑃,𝑠,𝑧   𝑄,𝑠,𝑧   𝑅,𝑠,𝑧   𝑈,𝑠,𝑧   𝑊,𝑠,𝑧   𝑢,𝑠,𝑧

Allowed substitution hints:   𝐴(𝑢)   𝐵(𝑧,𝑢,𝑠)   𝑃(𝑢)   𝑄(𝑢)   𝑅(𝑢)   𝑈(𝑢)   𝐸(𝑧,𝑢,𝑠)   𝐹(𝑧,𝑢,𝑠)   𝐺(𝑧,𝑢,𝑠)   𝐼(𝑧,𝑢,𝑠)   ∨ (𝑢)   ≤ (𝑢)   ∧ (𝑢)   𝑁(𝑧,𝑢,𝑠)   𝑂(𝑧,𝑢,𝑠)   𝑊(𝑢)

Proof of Theorem cdleme25cv

Step	Hyp	Ref	Expression
1		breq1 5046	. . . . . . . . 9 ⊢ (𝑠 = 𝑧 → (𝑠 ≤ 𝑊 ↔ 𝑧 ≤ 𝑊))
2	1	notbid 321	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → (¬ 𝑠 ≤ 𝑊 ↔ ¬ 𝑧 ≤ 𝑊))
3		breq1 5046	. . . . . . . . 9 ⊢ (𝑠 = 𝑧 → (𝑠 ≤ (𝑃 ∨ 𝑄) ↔ 𝑧 ≤ (𝑃 ∨ 𝑄)))
4	3	notbid 321	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → (¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ↔ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)))
5	2, 4	anbi12d 634	. . . . . . 7 ⊢ (𝑠 = 𝑧 → ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) ↔ (¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄))))
6		oveq1 7209	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑧 → (𝑠 ∨ 𝑈) = (𝑧 ∨ 𝑈))
7		oveq2 7210	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑧 → (𝑃 ∨ 𝑠) = (𝑃 ∨ 𝑧))
8	7	oveq1d 7217	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑧 → ((𝑃 ∨ 𝑠) ∧ 𝑊) = ((𝑃 ∨ 𝑧) ∧ 𝑊))
9	8	oveq2d 7218	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑧 → (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊)) = (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊)))
10	6, 9	oveq12d 7220	. . . . . . . . . 10 ⊢ (𝑠 = 𝑧 → ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) = ((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))))
11		oveq2 7210	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑧 → (𝑅 ∨ 𝑠) = (𝑅 ∨ 𝑧))
12	11	oveq1d 7217	. . . . . . . . . 10 ⊢ (𝑠 = 𝑧 → ((𝑅 ∨ 𝑠) ∧ 𝑊) = ((𝑅 ∨ 𝑧) ∧ 𝑊))
13	10, 12	oveq12d 7220	. . . . . . . . 9 ⊢ (𝑠 = 𝑧 → (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)) = (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))
14	13	oveq2d 7218	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊))) = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊))))
15	14	eqeq2d 2745	. . . . . . 7 ⊢ (𝑠 = 𝑧 → (𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊))) ↔ 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))))
16	5, 15	imbi12d 348	. . . . . 6 ⊢ (𝑠 = 𝑧 → (((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))) ↔ ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊))))))
17	16	cbvralvw 3351	. . . . 5 ⊢ (∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))) ↔ ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))))
18		cdleme25cv.n	. . . . . . . . 9 ⊢ 𝑁 = ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))
19		cdleme25cv.f	. . . . . . . . . . 11 ⊢ 𝐹 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊)))
20	19	oveq1i 7212	. . . . . . . . . 10 ⊢ (𝐹 ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)) = (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊))
21	20	oveq2i 7213	. . . . . . . . 9 ⊢ ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊))) = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))
22	18, 21	eqtri 2762	. . . . . . . 8 ⊢ 𝑁 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))
23	22	eqeq2i 2747	. . . . . . 7 ⊢ (𝑢 = 𝑁 ↔ 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊))))
24	23	imbi2i 339	. . . . . 6 ⊢ (((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁) ↔ ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))))
25	24	ralbii 3081	. . . . 5 ⊢ (∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁) ↔ ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))))
26		cdleme25cv.o	. . . . . . . . 9 ⊢ 𝑂 = ((𝑃 ∨ 𝑄) ∧ (𝐺 ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))
27		cdleme25cv.g	. . . . . . . . . . 11 ⊢ 𝐺 = ((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊)))
28	27	oveq1i 7212	. . . . . . . . . 10 ⊢ (𝐺 ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)) = (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊))
29	28	oveq2i 7213	. . . . . . . . 9 ⊢ ((𝑃 ∨ 𝑄) ∧ (𝐺 ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊))) = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))
30	26, 29	eqtri 2762	. . . . . . . 8 ⊢ 𝑂 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))
31	30	eqeq2i 2747	. . . . . . 7 ⊢ (𝑢 = 𝑂 ↔ 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊))))
32	31	imbi2i 339	. . . . . 6 ⊢ (((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂) ↔ ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))))
33	32	ralbii 3081	. . . . 5 ⊢ (∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂) ↔ ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))))
34	17, 25, 33	3bitr4i 306	. . . 4 ⊢ (∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁) ↔ ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂))
35	34	a1i 11	. . 3 ⊢ (𝑢 ∈ 𝐵 → (∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁) ↔ ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂)))
36	35	riotabiia 7180	. 2 ⊢ (℩𝑢 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁)) = (℩𝑢 ∈ 𝐵 ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂))
37		cdleme25cv.i	. 2 ⊢ 𝐼 = (℩𝑢 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁))
38		cdleme25cv.e	. 2 ⊢ 𝐸 = (℩𝑢 ∈ 𝐵 ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂))
39	36, 37, 38	3eqtr4i 2772	1 ⊢ 𝐼 = 𝐸

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543   ∈ wcel 2110  ∀wral 3054   class class class wbr 5043  ℩crio 7158  (class class class)co 7202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2706

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2713  df-cleq 2726  df-clel 2812  df-ral 3059  df-rab 3063  df-v 3403  df-dif 3860  df-un 3862  df-in 3864  df-ss 3874  df-nul 4228  df-if 4430  df-sn 4532  df-pr 4534  df-op 4538  df-uni 4810  df-br 5044  df-iota 6327  df-fv 6377  df-riota 7159  df-ov 7205

This theorem is referenced by:  cdleme27a  38075