Theorem cdleme27b

Description: Lemma for cdleme27N . (Contributed by NM, 3-Feb-2013)

	Ref	Expression
Hypotheses	cdleme26.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	cdleme26.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdleme26.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdleme26.m	⊢ ∧ = ( meet ‘ 𝐾 )
	cdleme26.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdleme26.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdleme27.u	⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
	cdleme27.f	⊢ 𝐹 = ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) )
	cdleme27.z	⊢ 𝑍 = ( ( 𝑧 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) )
	cdleme27.n	⊢ 𝑁 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑍 ∨ ( ( 𝑠 ∨ 𝑧 ) ∧ 𝑊 ) ) )
	cdleme27.d	⊢ 𝐷 = ( ℩ 𝑢 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( ( ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑢 = 𝑁 ) )
	cdleme27.c	⊢ 𝐶 = if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐷 , 𝐹 )
	cdleme27.g	⊢ 𝐺 = ( ( 𝑡 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑡 ) ∧ 𝑊 ) ) )
	cdleme27.o	⊢ 𝑂 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑍 ∨ ( ( 𝑡 ∨ 𝑧 ) ∧ 𝑊 ) ) )
	cdleme27.e	⊢ 𝐸 = ( ℩ 𝑢 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( ( ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑢 = 𝑂 ) )
	cdleme27.y	⊢ 𝑌 = if ( 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐸 , 𝐺 )
Assertion	cdleme27b	⊢ ( 𝑠 = 𝑡 → 𝐶 = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		cdleme26.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		cdleme26.l	⊢ ≤ = ( le ‘ 𝐾 )
3		cdleme26.j	⊢ ∨ = ( join ‘ 𝐾 )
4		cdleme26.m	⊢ ∧ = ( meet ‘ 𝐾 )
5		cdleme26.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6		cdleme26.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7		cdleme27.u	⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
8		cdleme27.f	⊢ 𝐹 = ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) )
9		cdleme27.z	⊢ 𝑍 = ( ( 𝑧 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑧 ) ∧ 𝑊 ) ) )
10		cdleme27.n	⊢ 𝑁 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑍 ∨ ( ( 𝑠 ∨ 𝑧 ) ∧ 𝑊 ) ) )
11		cdleme27.d	⊢ 𝐷 = ( ℩ 𝑢 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( ( ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑢 = 𝑁 ) )
12		cdleme27.c	⊢ 𝐶 = if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐷 , 𝐹 )
13		cdleme27.g	⊢ 𝐺 = ( ( 𝑡 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑡 ) ∧ 𝑊 ) ) )
14		cdleme27.o	⊢ 𝑂 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑍 ∨ ( ( 𝑡 ∨ 𝑧 ) ∧ 𝑊 ) ) )
15		cdleme27.e	⊢ 𝐸 = ( ℩ 𝑢 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( ( ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑢 = 𝑂 ) )
16		cdleme27.y	⊢ 𝑌 = if ( 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐸 , 𝐺 )
17		breq1	⊢ ( 𝑠 = 𝑡 → ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) ↔ 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) ) )
18		oveq1	⊢ ( 𝑠 = 𝑡 → ( 𝑠 ∨ 𝑧 ) = ( 𝑡 ∨ 𝑧 ) )
19	18	oveq1d	⊢ ( 𝑠 = 𝑡 → ( ( 𝑠 ∨ 𝑧 ) ∧ 𝑊 ) = ( ( 𝑡 ∨ 𝑧 ) ∧ 𝑊 ) )
20	19	oveq2d	⊢ ( 𝑠 = 𝑡 → ( 𝑍 ∨ ( ( 𝑠 ∨ 𝑧 ) ∧ 𝑊 ) ) = ( 𝑍 ∨ ( ( 𝑡 ∨ 𝑧 ) ∧ 𝑊 ) ) )
21	20	oveq2d	⊢ ( 𝑠 = 𝑡 → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑍 ∨ ( ( 𝑠 ∨ 𝑧 ) ∧ 𝑊 ) ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝑍 ∨ ( ( 𝑡 ∨ 𝑧 ) ∧ 𝑊 ) ) ) )
22	21 10 14	3eqtr4g	⊢ ( 𝑠 = 𝑡 → 𝑁 = 𝑂 )
23	22	eqeq2d	⊢ ( 𝑠 = 𝑡 → ( 𝑢 = 𝑁 ↔ 𝑢 = 𝑂 ) )
24	23	imbi2d	⊢ ( 𝑠 = 𝑡 → ( ( ( ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑢 = 𝑁 ) ↔ ( ( ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑢 = 𝑂 ) ) )
25	24	ralbidv	⊢ ( 𝑠 = 𝑡 → ( ∀ 𝑧 ∈ 𝐴 ( ( ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑢 = 𝑁 ) ↔ ∀ 𝑧 ∈ 𝐴 ( ( ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑢 = 𝑂 ) ) )
26	25	riotabidv	⊢ ( 𝑠 = 𝑡 → ( ℩ 𝑢 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( ( ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑢 = 𝑁 ) ) = ( ℩ 𝑢 ∈ 𝐵 ∀ 𝑧 ∈ 𝐴 ( ( ¬ 𝑧 ≤ 𝑊 ∧ ¬ 𝑧 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑢 = 𝑂 ) ) )
27	26 11 15	3eqtr4g	⊢ ( 𝑠 = 𝑡 → 𝐷 = 𝐸 )
28		oveq1	⊢ ( 𝑠 = 𝑡 → ( 𝑠 ∨ 𝑈 ) = ( 𝑡 ∨ 𝑈 ) )
29		oveq2	⊢ ( 𝑠 = 𝑡 → ( 𝑃 ∨ 𝑠 ) = ( 𝑃 ∨ 𝑡 ) )
30	29	oveq1d	⊢ ( 𝑠 = 𝑡 → ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) = ( ( 𝑃 ∨ 𝑡 ) ∧ 𝑊 ) )
31	30	oveq2d	⊢ ( 𝑠 = 𝑡 → ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) = ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑡 ) ∧ 𝑊 ) ) )
32	28 31	oveq12d	⊢ ( 𝑠 = 𝑡 → ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) ) = ( ( 𝑡 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑡 ) ∧ 𝑊 ) ) ) )
33	32 8 13	3eqtr4g	⊢ ( 𝑠 = 𝑡 → 𝐹 = 𝐺 )
34	17 27 33	ifbieq12d	⊢ ( 𝑠 = 𝑡 → if ( 𝑠 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐷 , 𝐹 ) = if ( 𝑡 ≤ ( 𝑃 ∨ 𝑄 ) , 𝐸 , 𝐺 ) )
35	34 12 16	3eqtr4g	⊢ ( 𝑠 = 𝑡 → 𝐶 = 𝑌 )