Theorem cdlemf2

Description: Part of Lemma F in Crawley p. 116. (Contributed by NM, 12-Apr-2013)

	Ref	Expression
Hypotheses	cdlemf1.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdlemf1.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdlemf1.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdlemf1.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdlemf2.m	⊢ ∧ = ( meet ‘ 𝐾 )
Assertion	cdlemf2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ∨ 𝑞 ) ∧ 𝑊 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cdlemf1.l	⊢ ≤ = ( le ‘ 𝐾 )
2		cdlemf1.j	⊢ ∨ = ( join ‘ 𝐾 )
3		cdlemf1.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		cdlemf1.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
5		cdlemf2.m	⊢ ∧ = ( meet ‘ 𝐾 )
6	1 3 4	lhpexnle	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∃ 𝑝 ∈ 𝐴 ¬ 𝑝 ≤ 𝑊 )
7	6	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ¬ 𝑝 ≤ 𝑊 )
8	1 2 3 4	cdlemf1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) ) )
9		simpr1r	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) ) ) ) → ¬ 𝑝 ≤ 𝑊 )
10		simpr32	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) ) ) ) → ¬ 𝑞 ≤ 𝑊 )
11		simpr33	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) ) ) ) → 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) )
12		simplrr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) ) ) ) → 𝑈 ≤ 𝑊 )
13		hllat	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
14	13	ad3antrrr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) ) ) ) → 𝐾 ∈ Lat )
15		simplrl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) ) ) ) → 𝑈 ∈ 𝐴 )
16		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
17	16 3	atbase	⊢ ( 𝑈 ∈ 𝐴 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
18	15 17	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) ) ) ) → 𝑈 ∈ ( Base ‘ 𝐾 ) )
19		simplll	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) ) ) ) → 𝐾 ∈ HL )
20		simpr1l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) ) ) ) → 𝑝 ∈ 𝐴 )
21		simpr2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) ) ) ) → 𝑞 ∈ 𝐴 )
22	16 2 3	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑝 ∨ 𝑞 ) ∈ ( Base ‘ 𝐾 ) )
23	19 20 21 22	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) ) ) ) → ( 𝑝 ∨ 𝑞 ) ∈ ( Base ‘ 𝐾 ) )
24	16 4	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
25	24	ad3antlr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) ) ) ) → 𝑊 ∈ ( Base ‘ 𝐾 ) )
26	16 1 5	latlem12	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑝 ∨ 𝑞 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑈 ≤ 𝑊 ) ↔ 𝑈 ≤ ( ( 𝑝 ∨ 𝑞 ) ∧ 𝑊 ) ) )
27	14 18 23 25 26	syl13anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) ) ) ) → ( ( 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) ∧ 𝑈 ≤ 𝑊 ) ↔ 𝑈 ≤ ( ( 𝑝 ∨ 𝑞 ) ∧ 𝑊 ) ) )
28	11 12 27	mpbi2and	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) ) ) ) → 𝑈 ≤ ( ( 𝑝 ∨ 𝑞 ) ∧ 𝑊 ) )
29		hlatl	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
30	29	ad3antrrr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) ) ) ) → 𝐾 ∈ AtLat )
31		simpll	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
32		simpr31	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) ) ) ) → 𝑝 ≠ 𝑞 )
33	1 2 5 3 4	lhpat	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ ( 𝑞 ∈ 𝐴 ∧ 𝑝 ≠ 𝑞 ) ) → ( ( 𝑝 ∨ 𝑞 ) ∧ 𝑊 ) ∈ 𝐴 )
34	31 20 9 21 32 33	syl122anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) ) ) ) → ( ( 𝑝 ∨ 𝑞 ) ∧ 𝑊 ) ∈ 𝐴 )
35	1 3	atcmp	⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑈 ∈ 𝐴 ∧ ( ( 𝑝 ∨ 𝑞 ) ∧ 𝑊 ) ∈ 𝐴 ) → ( 𝑈 ≤ ( ( 𝑝 ∨ 𝑞 ) ∧ 𝑊 ) ↔ 𝑈 = ( ( 𝑝 ∨ 𝑞 ) ∧ 𝑊 ) ) )
36	30 15 34 35	syl3anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) ) ) ) → ( 𝑈 ≤ ( ( 𝑝 ∨ 𝑞 ) ∧ 𝑊 ) ↔ 𝑈 = ( ( 𝑝 ∨ 𝑞 ) ∧ 𝑊 ) ) )
37	28 36	mpbid	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) ) ) ) → 𝑈 = ( ( 𝑝 ∨ 𝑞 ) ∧ 𝑊 ) )
38	9 10 37	jca31	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) ∧ ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ∧ 𝑞 ∈ 𝐴 ∧ ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) ) ) ) → ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ∨ 𝑞 ) ∧ 𝑊 ) ) )
39	38	3exp2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) → ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) → ( 𝑞 ∈ 𝐴 → ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) ) → ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ∨ 𝑞 ) ∧ 𝑊 ) ) ) ) ) )
40	39	3impia	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) → ( 𝑞 ∈ 𝐴 → ( ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) ) → ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ∨ 𝑞 ) ∧ 𝑊 ) ) ) ) )
41	40	reximdvai	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) → ( ∃ 𝑞 ∈ 𝐴 ( 𝑝 ≠ 𝑞 ∧ ¬ 𝑞 ≤ 𝑊 ∧ 𝑈 ≤ ( 𝑝 ∨ 𝑞 ) ) → ∃ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ∨ 𝑞 ) ∧ 𝑊 ) ) ) )
42	8 41	mpd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) ) → ∃ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ∨ 𝑞 ) ∧ 𝑊 ) ) )
43	42	3expia	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) → ( ( 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ≤ 𝑊 ) → ∃ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ∨ 𝑞 ) ∧ 𝑊 ) ) ) )
44	43	expd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) → ( 𝑝 ∈ 𝐴 → ( ¬ 𝑝 ≤ 𝑊 → ∃ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ∨ 𝑞 ) ∧ 𝑊 ) ) ) ) )
45	44	reximdvai	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) → ( ∃ 𝑝 ∈ 𝐴 ¬ 𝑝 ≤ 𝑊 → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ∨ 𝑞 ) ∧ 𝑊 ) ) ) )
46	7 45	mpd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐴 ( ( ¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑞 ≤ 𝑊 ) ∧ 𝑈 = ( ( 𝑝 ∨ 𝑞 ) ∧ 𝑊 ) ) )