Theorem cdleme25cv 35646

Description: Change bound variables in cdleme25c 35643. (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 4656	. . . . . . . . 9 ⊢ (𝑠 = 𝑧 → (𝑠 ≤ 𝑊 ↔ 𝑧 ≤ 𝑊))
2	1	notbid 308	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → (¬ 𝑠 ≤ 𝑊 ↔ ¬ 𝑧 ≤ 𝑊))
3		breq1 4656	. . . . . . . . 9 ⊢ (𝑠 = 𝑧 → (𝑠 ≤ (𝑃 ∨ 𝑄) ↔ 𝑧 ≤ (𝑃 ∨ 𝑄)))
4	3	notbid 308	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → (¬ 𝑠 ≤ (𝑃 ∨ 𝑄) ↔ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)))
5	2, 4	anbi12d 747	. . . . . . 7 ⊢ (𝑠 = 𝑧 → ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) ↔ (¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄))))
6		oveq1 6657	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑧 → (𝑠 ∨ 𝑈) = (𝑧 ∨ 𝑈))
7		oveq2 6658	. . . . . . . . . . . . 13 ⊢ (𝑠 = 𝑧 → (𝑃 ∨ 𝑠) = (𝑃 ∨ 𝑧))
8	7	oveq1d 6665	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑧 → ((𝑃 ∨ 𝑠) ∧ 𝑊) = ((𝑃 ∨ 𝑧) ∧ 𝑊))
9	8	oveq2d 6666	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑧 → (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊)) = (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊)))
10	6, 9	oveq12d 6668	. . . . . . . . . 10 ⊢ (𝑠 = 𝑧 → ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) = ((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))))
11		oveq2 6658	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑧 → (𝑅 ∨ 𝑠) = (𝑅 ∨ 𝑧))
12	11	oveq1d 6665	. . . . . . . . . 10 ⊢ (𝑠 = 𝑧 → ((𝑅 ∨ 𝑠) ∧ 𝑊) = ((𝑅 ∨ 𝑧) ∧ 𝑊))
13	10, 12	oveq12d 6668	. . . . . . . . 9 ⊢ (𝑠 = 𝑧 → (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)) = (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))
14	13	oveq2d 6666	. . . . . . . 8 ⊢ (𝑠 = 𝑧 → ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊))) = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊))))
15	14	eqeq2d 2632	. . . . . . 7 ⊢ (𝑠 = 𝑧 → (𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊))) ↔ 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))))
16	5, 15	imbi12d 334	. . . . . 6 ⊢ (𝑠 = 𝑧 → (((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))) ↔ ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊))))))
17	16	cbvralv 3171	. . . . 5 ⊢ (∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))) ↔ ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))))
18		cdleme25cv.n	. . . . . . . . 9 ⊢ 𝑁 = ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))
19		cdleme25cv.f	. . . . . . . . . . 11 ⊢ 𝐹 = ((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊)))
20	19	oveq1i 6660	. . . . . . . . . 10 ⊢ (𝐹 ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)) = (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊))
21	20	oveq2i 6661	. . . . . . . . 9 ⊢ ((𝑃 ∨ 𝑄) ∧ (𝐹 ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊))) = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))
22	18, 21	eqtri 2644	. . . . . . . 8 ⊢ 𝑁 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))
23	22	eqeq2i 2634	. . . . . . 7 ⊢ (𝑢 = 𝑁 ↔ 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊))))
24	23	imbi2i 326	. . . . . 6 ⊢ (((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁) ↔ ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))))
25	24	ralbii 2980	. . . . 5 ⊢ (∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁) ↔ ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑠 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑠) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑠) ∧ 𝑊)))))
26		cdleme25cv.o	. . . . . . . . 9 ⊢ 𝑂 = ((𝑃 ∨ 𝑄) ∧ (𝐺 ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))
27		cdleme25cv.g	. . . . . . . . . . 11 ⊢ 𝐺 = ((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊)))
28	27	oveq1i 6660	. . . . . . . . . 10 ⊢ (𝐺 ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)) = (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊))
29	28	oveq2i 6661	. . . . . . . . 9 ⊢ ((𝑃 ∨ 𝑄) ∧ (𝐺 ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊))) = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))
30	26, 29	eqtri 2644	. . . . . . . 8 ⊢ 𝑂 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))
31	30	eqeq2i 2634	. . . . . . 7 ⊢ (𝑢 = 𝑂 ↔ 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊))))
32	31	imbi2i 326	. . . . . 6 ⊢ (((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂) ↔ ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))))
33	32	ralbii 2980	. . . . 5 ⊢ (∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂) ↔ ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = ((𝑃 ∨ 𝑄) ∧ (((𝑧 ∨ 𝑈) ∧ (𝑄 ∨ ((𝑃 ∨ 𝑧) ∧ 𝑊))) ∨ ((𝑅 ∨ 𝑧) ∧ 𝑊)))))
34	17, 25, 33	3bitr4i 292	. . . 4 ⊢ (∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁) ↔ ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂))
35	34	a1i 11	. . 3 ⊢ (𝑢 ∈ 𝐵 → (∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁) ↔ ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂)))
36	35	riotabiia 6628	. 2 ⊢ (℩𝑢 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁)) = (℩𝑢 ∈ 𝐵 ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂))
37		cdleme25cv.i	. 2 ⊢ 𝐼 = (℩𝑢 ∈ 𝐵 ∀𝑠 ∈ 𝐴 ((¬ 𝑠 ≤ 𝑊 ∧ ¬ 𝑠 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑁))
38		cdleme25cv.e	. 2 ⊢ 𝐸 = (℩𝑢 ∈ 𝐵 ∀𝑧 ∈ 𝐴 ((¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ (𝑃 ∨ 𝑄)) → 𝑢 = 𝑂))
39	36, 37, 38	3eqtr4i 2654	1 ⊢ 𝐼 = 𝐸

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1483   ∈ wcel 1990  ∀wral 2912   class class class wbr 4653  ℩crio 6610  (class class class)co 6650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-riota 6611  df-ov 6653

This theorem is referenced by:  cdleme27a  35655