Theorem cdlemg2ce

Description: Utility theorem to eliminate p,q when converting theorems with explicit f. TODO: fix comment. (Contributed by NM, 22-Apr-2013)

	Ref	Expression
Hypotheses	cdlemg2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	cdlemg2.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdlemg2.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdlemg2.m	⊢ ∧ = ( meet ‘ 𝐾 )
	cdlemg2.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdlemg2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdlemg2.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	cdlemg2ex.u	⊢ 𝑈 = ( ( 𝑝 ∨ 𝑞 ) ∧ 𝑊 )
	cdlemg2ex.d	⊢ 𝐷 = ( ( 𝑡 ∨ 𝑈 ) ∧ ( 𝑞 ∨ ( ( 𝑝 ∨ 𝑡 ) ∧ 𝑊 ) ) )
	cdlemg2ex.e	⊢ 𝐸 = ( ( 𝑝 ∨ 𝑞 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑡 ) ∧ 𝑊 ) ) )
	cdlemg2ex.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐵 ↦ if ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑥 ≤ 𝑊 ) , ( ℩ 𝑧 ∈ 𝐵 ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑥 ∧ 𝑊 ) ) = 𝑥 ) → 𝑧 = ( if ( 𝑠 ≤ ( 𝑝 ∨ 𝑞 ) , ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑝 ∨ 𝑞 ) ) → 𝑦 = 𝐸 ) ) , ⦋ 𝑠 / 𝑡 ⦌ 𝐷 ) ∨ ( 𝑥 ∧ 𝑊 ) ) ) ) , 𝑥 ) )
	cdlemg2ce.p	⊢ ( 𝐹 = 𝐺 → ( 𝜓 ↔ 𝜒 ) )
	cdlemg2ce.c	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ) ∧ 𝜑 ) → 𝜒 )
Assertion	cdlemg2ce	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝜑 ) → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		cdlemg2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		cdlemg2.l	⊢ ≤ = ( le ‘ 𝐾 )
3		cdlemg2.j	⊢ ∨ = ( join ‘ 𝐾 )
4		cdlemg2.m	⊢ ∧ = ( meet ‘ 𝐾 )
5		cdlemg2.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6		cdlemg2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7		cdlemg2.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
8		cdlemg2ex.u	⊢ 𝑈 = ( ( 𝑝 ∨ 𝑞 ) ∧ 𝑊 )
9		cdlemg2ex.d	⊢ 𝐷 = ( ( 𝑡 ∨ 𝑈 ) ∧ ( 𝑞 ∨ ( ( 𝑝 ∨ 𝑡 ) ∧ 𝑊 ) ) )
10		cdlemg2ex.e	⊢ 𝐸 = ( ( 𝑝 ∨ 𝑞 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑡 ) ∧ 𝑊 ) ) )
11		cdlemg2ex.g	⊢ 𝐺 = ( 𝑥 ∈ 𝐵 ↦ if ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑥 ≤ 𝑊 ) , ( ℩ 𝑧 ∈ 𝐵 ∀ 𝑠 ∈ 𝐴 ( ( ¬ 𝑠 ≤ 𝑊 ∧ ( 𝑠 ∨ ( 𝑥 ∧ 𝑊 ) ) = 𝑥 ) → 𝑧 = ( if ( 𝑠 ≤ ( 𝑝 ∨ 𝑞 ) , ( ℩ 𝑦 ∈ 𝐵 ∀ 𝑡 ∈ 𝐴 ( ( ¬ 𝑡 ≤ 𝑊 ∧ ¬ 𝑡 ≤ ( 𝑝 ∨ 𝑞 ) ) → 𝑦 = 𝐸 ) ) , ⦋ 𝑠 / 𝑡 ⦌ 𝐷 ) ∨ ( 𝑥 ∧ 𝑊 ) ) ) ) , 𝑥 ) )
12		cdlemg2ce.p	⊢ ( 𝐹 = 𝐺 → ( 𝜓 ↔ 𝜒 ) )
13		cdlemg2ce.c	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) ) ∧ 𝜑 ) → 𝜒 )
14		simp2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝜑 ) → 𝐹 ∈ 𝑇 )
15	1 2 3 4 5 6 7 8 9 10 11	cdlemg2cex	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐹 ∈ 𝑇 ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝐹 = 𝐺 ) ) )
16	15	3ad2ant1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝜑 ) → ( 𝐹 ∈ 𝑇 ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝐹 = 𝐺 ) ) )
17	14 16	mpbid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝜑 ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝐹 = 𝐺 ) )
18		simp11	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝜑 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝐹 = 𝐺 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
19		simp2l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝜑 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝐹 = 𝐺 ) ) → 𝑝 ∈ 𝐴 )
20		simp31	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝜑 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝐹 = 𝐺 ) ) → ¬ 𝑝 ≤ 𝑊 )
21	19 20	jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝜑 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝐹 = 𝐺 ) ) → ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) )
22		simp2r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝜑 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝐹 = 𝐺 ) ) → 𝑞 ∈ 𝐴 )
23		simp32	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝜑 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝐹 = 𝐺 ) ) → ¬ 𝑞 ≤ 𝑊 )
24	22 23	jca	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝜑 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝐹 = 𝐺 ) ) → ( 𝑞 ∈ 𝐴 ∧ ¬ 𝑞 ≤ 𝑊 ) )
25		simp13	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝜑 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝐹 = 𝐺 ) ) → 𝜑 )
26	18 21 24 25 13	syl31anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝜑 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝐹 = 𝐺 ) ) → 𝜒 )
27		simp33	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝜑 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝐹 = 𝐺 ) ) → 𝐹 = 𝐺 )
28	27 12	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝜑 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝐹 = 𝐺 ) ) → ( 𝜓 ↔ 𝜒 ) )
29	26 28	mpbird	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝜑 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) ∧ ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝐹 = 𝐺 ) ) → 𝜓 )
30	29	3exp	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝜑 ) → ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) → ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝐹 = 𝐺 ) → 𝜓 ) ) )
31	30	rexlimdvv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝜑 ) → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝐹 = 𝐺 ) → 𝜓 ) )
32	17 31	mpd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝜑 ) → 𝜓 )