cdleme25cv

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

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

Proof

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

Metamath Proof Explorer

Theorem cdleme25cv

Proof