Metamath Proof Explorer

Theorem 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 ⊢ 𝐼 = 𝐸