Theorem cdleme25cv 38299

Description: Change bound variables in cdleme25c 38296. (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 5073	. . . . . . . . 9 ⊢ (𝑠 = 𝑧 → (𝑠 ≤ 𝑊 ↔ 𝑧 ≤ 𝑊))
2	1	notbid 317	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → (¬ 𝑠 ≤ 𝑊 ↔ ¬ 𝑧 ≤ 𝑊))
3		breq1 5073	. . . . . . . . 9 ⊢ (𝑠 = 𝑧 → (𝑠 ≤ (𝑃 ∨ 𝑄) ↔ 𝑧 ≤ (𝑃 ∨ 𝑄)))
4	3	notbid 317	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → (¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ↔ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)))
5	2, 4	anbi12d 630	. . . . . . 7 ⊢ (𝑠 = 𝑧 → ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) ↔ (¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄))))
6		oveq1 7262	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑧 → (𝑠 ∨ 𝑈) = (𝑧 ∨ 𝑈))
7		oveq2 7263	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑧 → (𝑃 ∨ 𝑠) = (𝑃 ∨ 𝑧))
8	7	oveq1d 7270	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑧 → ((𝑃 ∨ 𝑠) ∧ 𝑊) = ((𝑃 ∨ 𝑧) ∧ 𝑊))
9	8	oveq2d 7271	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑧 → (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊)) = (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊)))
10	6, 9	oveq12d 7273	. . . . . . . . . 10 ⊢ (𝑠 = 𝑧 → ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) = ((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))))
11		oveq2 7263	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑧 → (𝑅 ∨ 𝑠) = (𝑅 ∨ 𝑧))
12	11	oveq1d 7270	. . . . . . . . . 10 ⊢ (𝑠 = 𝑧 → ((𝑅 ∨ 𝑠) ∧ 𝑊) = ((𝑅 ∨ 𝑧) ∧ 𝑊))
13	10, 12	oveq12d 7273	. . . . . . . . 9 ⊢ (𝑠 = 𝑧 → (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)) = (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))
14	13	oveq2d 7271	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊))) = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊))))
15	14	eqeq2d 2749	. . . . . . 7 ⊢ (𝑠 = 𝑧 → (𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊))) ↔ 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))))
16	5, 15	imbi12d 344	. . . . . 6 ⊢ (𝑠 = 𝑧 → (((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))) ↔ ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊))))))
17	16	cbvralvw 3372	. . . . 5 ⊢ (∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))) ↔ ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))))
18		cdleme25cv.n	. . . . . . . . 9 ⊢ 𝑁 = ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))
19		cdleme25cv.f	. . . . . . . . . . 11 ⊢ 𝐹 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊)))
20	19	oveq1i 7265	. . . . . . . . . 10 ⊢ (𝐹 ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)) = (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊))
21	20	oveq2i 7266	. . . . . . . . 9 ⊢ ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊))) = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))
22	18, 21	eqtri 2766	. . . . . . . 8 ⊢ 𝑁 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))
23	22	eqeq2i 2751	. . . . . . 7 ⊢ (𝑢 = 𝑁 ↔ 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊))))
24	23	imbi2i 335	. . . . . 6 ⊢ (((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁) ↔ ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))))
25	24	ralbii 3090	. . . . 5 ⊢ (∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁) ↔ ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))))
26		cdleme25cv.o	. . . . . . . . 9 ⊢ 𝑂 = ((𝑃 ∨ 𝑄) ∧ (𝐺 ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))
27		cdleme25cv.g	. . . . . . . . . . 11 ⊢ 𝐺 = ((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊)))
28	27	oveq1i 7265	. . . . . . . . . 10 ⊢ (𝐺 ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)) = (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊))
29	28	oveq2i 7266	. . . . . . . . 9 ⊢ ((𝑃 ∨ 𝑄) ∧ (𝐺 ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊))) = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))
30	26, 29	eqtri 2766	. . . . . . . 8 ⊢ 𝑂 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))
31	30	eqeq2i 2751	. . . . . . 7 ⊢ (𝑢 = 𝑂 ↔ 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊))))
32	31	imbi2i 335	. . . . . 6 ⊢ (((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂) ↔ ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))))
33	32	ralbii 3090	. . . . 5 ⊢ (∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂) ↔ ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))))
34	17, 25, 33	3bitr4i 302	. . . 4 ⊢ (∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁) ↔ ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂))
35	34	a1i 11	. . 3 ⊢ (𝑢 ∈ 𝐵 → (∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁) ↔ ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂)))
36	35	riotabiia 7233	. 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 395   = wceq 1539   ∈ wcel 2108  ∀wral 3063   class class class wbr 5070  ℩crio 7211  (class class class)co 7255

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-riota 7212  df-ov 7258

This theorem is referenced by:  cdleme27a  38308