Theorem cdleme25cv 41395

Description: Change bound variables in cdleme25c 41392. (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 5106	. . . . . . . . 9 ⊢ (𝑠 = 𝑧 → (𝑠 ≤ 𝑊 ↔ 𝑧 ≤ 𝑊))
2	1	notbid 321	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → (¬ 𝑠 ≤ 𝑊 ↔ ¬ 𝑧 ≤ 𝑊))
3		breq1 5106	. . . . . . . . 9 ⊢ (𝑠 = 𝑧 → (𝑠 ≤ (𝑃 ∨ 𝑄) ↔ 𝑧 ≤ (𝑃 ∨ 𝑄)))
4	3	notbid 321	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → (¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ↔ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)))
5	2, 4	anbi12d 644	. . . . . . 7 ⊢ (𝑠 = 𝑧 → ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) ↔ (¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄))))
6		oveq1 7425	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑧 → (𝑠 ∨ 𝑈) = (𝑧 ∨ 𝑈))
7		oveq2 7426	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑧 → (𝑃 ∨ 𝑠) = (𝑃 ∨ 𝑧))
8	7	oveq1d 7433	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑧 → ((𝑃 ∨ 𝑠) ∧ 𝑊) = ((𝑃 ∨ 𝑧) ∧ 𝑊))
9	8	oveq2d 7434	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑧 → (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊)) = (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊)))
10	6, 9	oveq12d 7436	. . . . . . . . . 10 ⊢ (𝑠 = 𝑧 → ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) = ((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))))
11		oveq2 7426	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑧 → (𝑅 ∨ 𝑠) = (𝑅 ∨ 𝑧))
12	11	oveq1d 7433	. . . . . . . . . 10 ⊢ (𝑠 = 𝑧 → ((𝑅 ∨ 𝑠) ∧ 𝑊) = ((𝑅 ∨ 𝑧) ∧ 𝑊))
13	10, 12	oveq12d 7436	. . . . . . . . 9 ⊢ (𝑠 = 𝑧 → (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)) = (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))
14	13	oveq2d 7434	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊))) = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊))))
15	14	eqeq2d 2772	. . . . . . 7 ⊢ (𝑠 = 𝑧 → (𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊))) ↔ 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))))
16	5, 15	imbi12d 347	. . . . . 6 ⊢ (𝑠 = 𝑧 → (((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))) ↔ ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊))))))
17	16	cbvralvw 3241	. . . . 5 ⊢ (∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))) ↔ ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))))
18		cdleme25cv.n	. . . . . . . . 9 ⊢ 𝑁 = ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))
19		cdleme25cv.f	. . . . . . . . . . 11 ⊢ 𝐹 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊)))
20	19	oveq1i 7428	. . . . . . . . . 10 ⊢ (𝐹 ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)) = (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊))
21	20	oveq2i 7429	. . . . . . . . 9 ⊢ ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊))) = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))
22	18, 21	eqtri 2784	. . . . . . . 8 ⊢ 𝑁 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))
23	22	eqeq2i 2774	. . . . . . 7 ⊢ (𝑢 = 𝑁 ↔ 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊))))
24	23	imbi2i 339	. . . . . 6 ⊢ (((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁) ↔ ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))))
25	24	ralbii 3109	. . . . 5 ⊢ (∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁) ↔ ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))))
26		cdleme25cv.o	. . . . . . . . 9 ⊢ 𝑂 = ((𝑃 ∨ 𝑄) ∧ (𝐺 ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))
27		cdleme25cv.g	. . . . . . . . . . 11 ⊢ 𝐺 = ((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊)))
28	27	oveq1i 7428	. . . . . . . . . 10 ⊢ (𝐺 ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)) = (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊))
29	28	oveq2i 7429	. . . . . . . . 9 ⊢ ((𝑃 ∨ 𝑄) ∧ (𝐺 ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊))) = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))
30	26, 29	eqtri 2784	. . . . . . . 8 ⊢ 𝑂 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))
31	30	eqeq2i 2774	. . . . . . 7 ⊢ (𝑢 = 𝑂 ↔ 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊))))
32	31	imbi2i 339	. . . . . 6 ⊢ (((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂) ↔ ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))))
33	32	ralbii 3109	. . . . 5 ⊢ (∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂) ↔ ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))))
34	17, 25, 33	3bitr4i 306	. . . 4 ⊢ (∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁) ↔ ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂))
35	34	a1i 11	. . 3 ⊢ (𝑢 ∈ 𝐵 → (∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁) ↔ ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂)))
36	35	riotabiia 7395	. 2 ⊢ (℩𝑢 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁)) = (℩𝑢 ∈ 𝐵 ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂))
37		cdleme25cv.i	. 2 ⊢ 𝐼 = (℩𝑢 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁))
38		cdleme25cv.e	. 2 ⊢ 𝐸 = (℩𝑢 ∈ 𝐵 ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂))
39	36, 37, 38	3eqtr4i 2794	1 ⊢ 𝐼 = 𝐸

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3077   class class class wbr 5103  ℩crio 7374  (class class class)co 7418

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6493  df-fv 6545  df-riota 7375  df-ov 7421

This theorem is used by:  cdleme27a  41404