Theorem cdleme25cv 38372

Description: Change bound variables in cdleme25c 38369. (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 5077	. . . . . . . . 9 ⊢ (𝑠 = 𝑧 → (𝑠 ≤ 𝑊 ↔ 𝑧 ≤ 𝑊))
2	1	notbid 318	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → (¬ 𝑠 ≤ 𝑊 ↔ ¬ 𝑧 ≤ 𝑊))
3		breq1 5077	. . . . . . . . 9 ⊢ (𝑠 = 𝑧 → (𝑠 ≤ (𝑃 ∨ 𝑄) ↔ 𝑧 ≤ (𝑃 ∨ 𝑄)))
4	3	notbid 318	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → (¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ↔ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)))
5	2, 4	anbi12d 631	. . . . . . 7 ⊢ (𝑠 = 𝑧 → ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) ↔ (¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄))))
6		oveq1 7282	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑧 → (𝑠 ∨ 𝑈) = (𝑧 ∨ 𝑈))
7		oveq2 7283	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑧 → (𝑃 ∨ 𝑠) = (𝑃 ∨ 𝑧))
8	7	oveq1d 7290	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑧 → ((𝑃 ∨ 𝑠) ∧ 𝑊) = ((𝑃 ∨ 𝑧) ∧ 𝑊))
9	8	oveq2d 7291	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑧 → (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊)) = (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊)))
10	6, 9	oveq12d 7293	. . . . . . . . . 10 ⊢ (𝑠 = 𝑧 → ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) = ((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))))
11		oveq2 7283	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑧 → (𝑅 ∨ 𝑠) = (𝑅 ∨ 𝑧))
12	11	oveq1d 7290	. . . . . . . . . 10 ⊢ (𝑠 = 𝑧 → ((𝑅 ∨ 𝑠) ∧ 𝑊) = ((𝑅 ∨ 𝑧) ∧ 𝑊))
13	10, 12	oveq12d 7293	. . . . . . . . 9 ⊢ (𝑠 = 𝑧 → (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)) = (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))
14	13	oveq2d 7291	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊))) = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊))))
15	14	eqeq2d 2749	. . . . . . 7 ⊢ (𝑠 = 𝑧 → (𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊))) ↔ 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))))
16	5, 15	imbi12d 345	. . . . . 6 ⊢ (𝑠 = 𝑧 → (((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))) ↔ ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊))))))
17	16	cbvralvw 3383	. . . . 5 ⊢ (∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))) ↔ ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))))
18		cdleme25cv.n	. . . . . . . . 9 ⊢ 𝑁 = ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))
19		cdleme25cv.f	. . . . . . . . . . 11 ⊢ 𝐹 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊)))
20	19	oveq1i 7285	. . . . . . . . . 10 ⊢ (𝐹 ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)) = (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊))
21	20	oveq2i 7286	. . . . . . . . 9 ⊢ ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊))) = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))
22	18, 21	eqtri 2766	. . . . . . . 8 ⊢ 𝑁 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))
23	22	eqeq2i 2751	. . . . . . 7 ⊢ (𝑢 = 𝑁 ↔ 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊))))
24	23	imbi2i 336	. . . . . 6 ⊢ (((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁) ↔ ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))))
25	24	ralbii 3092	. . . . 5 ⊢ (∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁) ↔ ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))))
26		cdleme25cv.o	. . . . . . . . 9 ⊢ 𝑂 = ((𝑃 ∨ 𝑄) ∧ (𝐺 ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))
27		cdleme25cv.g	. . . . . . . . . . 11 ⊢ 𝐺 = ((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊)))
28	27	oveq1i 7285	. . . . . . . . . 10 ⊢ (𝐺 ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)) = (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊))
29	28	oveq2i 7286	. . . . . . . . 9 ⊢ ((𝑃 ∨ 𝑄) ∧ (𝐺 ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊))) = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))
30	26, 29	eqtri 2766	. . . . . . . 8 ⊢ 𝑂 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))
31	30	eqeq2i 2751	. . . . . . 7 ⊢ (𝑢 = 𝑂 ↔ 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊))))
32	31	imbi2i 336	. . . . . 6 ⊢ (((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂) ↔ ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))))
33	32	ralbii 3092	. . . . 5 ⊢ (∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂) ↔ ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))))
34	17, 25, 33	3bitr4i 303	. . . 4 ⊢ (∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁) ↔ ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂))
35	34	a1i 11	. . 3 ⊢ (𝑢 ∈ 𝐵 → (∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁) ↔ ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂)))
36	35	riotabiia 7253	. 2 ⊢ (℩𝑢 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁)) = (℩𝑢 ∈ 𝐵 ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂))
37		cdleme25cv.i	. 2 ⊢ 𝐼 = (℩𝑢 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁))
38		cdleme25cv.e	. 2 ⊢ 𝐸 = (℩𝑢 ∈ 𝐵 ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂))
39	36, 37, 38	3eqtr4i 2776	1 ⊢ 𝐼 = 𝐸

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  ∀wral 3064   class class class wbr 5074  ℩crio 7231  (class class class)co 7275

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-iota 6391  df-fv 6441  df-riota 7232  df-ov 7278

This theorem is referenced by:  cdleme27a  38381