Theorem cdlemefrs29bpre0

Description: TODO fix comment. (Contributed by NM, 29-Mar-2013)

	Ref	Expression
Hypotheses	cdlemefrs27.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	cdlemefrs27.l	⊢ ≤ = ( le ‘ 𝐾 )
	cdlemefrs27.j	⊢ ∨ = ( join ‘ 𝐾 )
	cdlemefrs27.m	⊢ ∧ = ( meet ‘ 𝐾 )
	cdlemefrs27.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	cdlemefrs27.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	cdlemefrs27.eq	⊢ ( 𝑠 = 𝑅 → ( 𝜑 ↔ 𝜓 ) )
	cdlemefrs27.nb	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ∧ ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ) → 𝑁 ∈ 𝐵 )
Assertion	cdlemefrs29bpre0	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) → ( ∀ 𝑠 ∈ 𝐴 ( ( ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ∧ ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ) → 𝑧 = ( 𝑁 ∨ ( 𝑅 ∧ 𝑊 ) ) ) ↔ 𝑧 = ⦋ 𝑅 / 𝑠 ⦌ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		cdlemefrs27.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		cdlemefrs27.l	⊢ ≤ = ( le ‘ 𝐾 )
3		cdlemefrs27.j	⊢ ∨ = ( join ‘ 𝐾 )
4		cdlemefrs27.m	⊢ ∧ = ( meet ‘ 𝐾 )
5		cdlemefrs27.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6		cdlemefrs27.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7		cdlemefrs27.eq	⊢ ( 𝑠 = 𝑅 → ( 𝜑 ↔ 𝜓 ) )
8		cdlemefrs27.nb	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ 𝑃 ≠ 𝑄 ∧ ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ) → 𝑁 ∈ 𝐵 )
9		df-ral	⊢ ( ∀ 𝑠 ∈ 𝐴 ( ( ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ∧ ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ) → 𝑧 = ( 𝑁 ∨ ( 𝑅 ∧ 𝑊 ) ) ) ↔ ∀ 𝑠 ( 𝑠 ∈ 𝐴 → ( ( ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ∧ ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ) → 𝑧 = ( 𝑁 ∨ ( 𝑅 ∧ 𝑊 ) ) ) ) )
10		anass	⊢ ( ( ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ∧ ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ) ↔ ( 𝑠 ∈ 𝐴 ∧ ( ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ∧ ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ) ) )
11	10	imbi1i	⊢ ( ( ( ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ∧ ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ) → 𝑧 = ( 𝑁 ∨ ( 𝑅 ∧ 𝑊 ) ) ) ↔ ( ( 𝑠 ∈ 𝐴 ∧ ( ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ∧ ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ) ) → 𝑧 = ( 𝑁 ∨ ( 𝑅 ∧ 𝑊 ) ) ) )
12		impexp	⊢ ( ( ( ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ∧ ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ) → 𝑧 = ( 𝑁 ∨ ( 𝑅 ∧ 𝑊 ) ) ) ↔ ( ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) → ( ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 → 𝑧 = ( 𝑁 ∨ ( 𝑅 ∧ 𝑊 ) ) ) ) )
13		impexp	⊢ ( ( ( 𝑠 ∈ 𝐴 ∧ ( ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ∧ ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ) ) → 𝑧 = ( 𝑁 ∨ ( 𝑅 ∧ 𝑊 ) ) ) ↔ ( 𝑠 ∈ 𝐴 → ( ( ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ∧ ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ) → 𝑧 = ( 𝑁 ∨ ( 𝑅 ∧ 𝑊 ) ) ) ) )
14	11 12 13	3bitr3ri	⊢ ( ( 𝑠 ∈ 𝐴 → ( ( ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ∧ ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ) → 𝑧 = ( 𝑁 ∨ ( 𝑅 ∧ 𝑊 ) ) ) ) ↔ ( ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) → ( ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 → 𝑧 = ( 𝑁 ∨ ( 𝑅 ∧ 𝑊 ) ) ) ) )
15		simpl11	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
16		simpl2r	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ) → ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) )
17		eqid	⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
18	2 4 17 5 6	lhpmat	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) → ( 𝑅 ∧ 𝑊 ) = ( 0. ‘ 𝐾 ) )
19	15 16 18	syl2anc	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ) → ( 𝑅 ∧ 𝑊 ) = ( 0. ‘ 𝐾 ) )
20	19	oveq2d	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ) → ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = ( 𝑠 ∨ ( 0. ‘ 𝐾 ) ) )
21		simp11l	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) → 𝐾 ∈ HL )
22		hlol	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
23	21 22	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) → 𝐾 ∈ OL )
24	23	adantr	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ) → 𝐾 ∈ OL )
25		simprl	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ) → 𝑠 ∈ 𝐴 )
26	1 5	atbase	⊢ ( 𝑠 ∈ 𝐴 → 𝑠 ∈ 𝐵 )
27	25 26	syl	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ) → 𝑠 ∈ 𝐵 )
28	1 3 17	olj01	⊢ ( ( 𝐾 ∈ OL ∧ 𝑠 ∈ 𝐵 ) → ( 𝑠 ∨ ( 0. ‘ 𝐾 ) ) = 𝑠 )
29	24 27 28	syl2anc	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ) → ( 𝑠 ∨ ( 0. ‘ 𝐾 ) ) = 𝑠 )
30	20 29	eqtrd	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ) → ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑠 )
31	30	eqeq1d	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ) → ( ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ↔ 𝑠 = 𝑅 ) )
32	19	oveq2d	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ) → ( 𝑁 ∨ ( 𝑅 ∧ 𝑊 ) ) = ( 𝑁 ∨ ( 0. ‘ 𝐾 ) ) )
33		simpl1	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ) → ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) )
34		simpl2l	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ) → 𝑃 ≠ 𝑄 )
35		simprr	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ) → ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) )
36	33 34 25 35 8	syl112anc	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ) → 𝑁 ∈ 𝐵 )
37	1 3 17	olj01	⊢ ( ( 𝐾 ∈ OL ∧ 𝑁 ∈ 𝐵 ) → ( 𝑁 ∨ ( 0. ‘ 𝐾 ) ) = 𝑁 )
38	24 36 37	syl2anc	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ) → ( 𝑁 ∨ ( 0. ‘ 𝐾 ) ) = 𝑁 )
39	32 38	eqtrd	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ) → ( 𝑁 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑁 )
40	39	eqeq2d	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ) → ( 𝑧 = ( 𝑁 ∨ ( 𝑅 ∧ 𝑊 ) ) ↔ 𝑧 = 𝑁 ) )
41	31 40	imbi12d	⊢ ( ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) ∧ ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ) → ( ( ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 → 𝑧 = ( 𝑁 ∨ ( 𝑅 ∧ 𝑊 ) ) ) ↔ ( 𝑠 = 𝑅 → 𝑧 = 𝑁 ) ) )
42	41	pm5.74da	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) → ( ( ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) → ( ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 → 𝑧 = ( 𝑁 ∨ ( 𝑅 ∧ 𝑊 ) ) ) ) ↔ ( ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) → ( 𝑠 = 𝑅 → 𝑧 = 𝑁 ) ) ) )
43		impexp	⊢ ( ( ( ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ∧ 𝑠 = 𝑅 ) → 𝑧 = 𝑁 ) ↔ ( ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) → ( 𝑠 = 𝑅 → 𝑧 = 𝑁 ) ) )
44		simp2rl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) → 𝑅 ∈ 𝐴 )
45		simp2rr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) → ¬ 𝑅 ≤ 𝑊 )
46		simp3	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) → 𝜓 )
47		eleq1	⊢ ( 𝑠 = 𝑅 → ( 𝑠 ∈ 𝐴 ↔ 𝑅 ∈ 𝐴 ) )
48		breq1	⊢ ( 𝑠 = 𝑅 → ( 𝑠 ≤ 𝑊 ↔ 𝑅 ≤ 𝑊 ) )
49	48	notbid	⊢ ( 𝑠 = 𝑅 → ( ¬ 𝑠 ≤ 𝑊 ↔ ¬ 𝑅 ≤ 𝑊 ) )
50	49 7	anbi12d	⊢ ( 𝑠 = 𝑅 → ( ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ↔ ( ¬ 𝑅 ≤ 𝑊 ∧ 𝜓 ) ) )
51	47 50	anbi12d	⊢ ( 𝑠 = 𝑅 → ( ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ↔ ( 𝑅 ∈ 𝐴 ∧ ( ¬ 𝑅 ≤ 𝑊 ∧ 𝜓 ) ) ) )
52	51	biimprcd	⊢ ( ( 𝑅 ∈ 𝐴 ∧ ( ¬ 𝑅 ≤ 𝑊 ∧ 𝜓 ) ) → ( 𝑠 = 𝑅 → ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ) )
53	44 45 46 52	syl12anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) → ( 𝑠 = 𝑅 → ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ) )
54	53	pm4.71rd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) → ( 𝑠 = 𝑅 ↔ ( ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ∧ 𝑠 = 𝑅 ) ) )
55	54	imbi1d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) → ( ( 𝑠 = 𝑅 → 𝑧 = 𝑁 ) ↔ ( ( ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ∧ 𝑠 = 𝑅 ) → 𝑧 = 𝑁 ) ) )
56		eqcom	⊢ ( 𝑧 = 𝑁 ↔ 𝑁 = 𝑧 )
57	56	imbi2i	⊢ ( ( 𝑠 = 𝑅 → 𝑧 = 𝑁 ) ↔ ( 𝑠 = 𝑅 → 𝑁 = 𝑧 ) )
58	55 57	bitr3di	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) → ( ( ( ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) ∧ 𝑠 = 𝑅 ) → 𝑧 = 𝑁 ) ↔ ( 𝑠 = 𝑅 → 𝑁 = 𝑧 ) ) )
59	43 58	bitr3id	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) → ( ( ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) → ( 𝑠 = 𝑅 → 𝑧 = 𝑁 ) ) ↔ ( 𝑠 = 𝑅 → 𝑁 = 𝑧 ) ) )
60	42 59	bitrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) → ( ( ( 𝑠 ∈ 𝐴 ∧ ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ) → ( ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 → 𝑧 = ( 𝑁 ∨ ( 𝑅 ∧ 𝑊 ) ) ) ) ↔ ( 𝑠 = 𝑅 → 𝑁 = 𝑧 ) ) )
61	14 60	bitrid	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) → ( ( 𝑠 ∈ 𝐴 → ( ( ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ∧ ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ) → 𝑧 = ( 𝑁 ∨ ( 𝑅 ∧ 𝑊 ) ) ) ) ↔ ( 𝑠 = 𝑅 → 𝑁 = 𝑧 ) ) )
62	61	albidv	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) → ( ∀ 𝑠 ( 𝑠 ∈ 𝐴 → ( ( ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ∧ ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ) → 𝑧 = ( 𝑁 ∨ ( 𝑅 ∧ 𝑊 ) ) ) ) ↔ ∀ 𝑠 ( 𝑠 = 𝑅 → 𝑁 = 𝑧 ) ) )
63	9 62	bitrid	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) → ( ∀ 𝑠 ∈ 𝐴 ( ( ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ∧ ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ) → 𝑧 = ( 𝑁 ∨ ( 𝑅 ∧ 𝑊 ) ) ) ↔ ∀ 𝑠 ( 𝑠 = 𝑅 → 𝑁 = 𝑧 ) ) )
64		nfcv	⊢ Ⅎ 𝑠 𝑧
65	64	csbiebg	⊢ ( 𝑅 ∈ 𝐴 → ( ∀ 𝑠 ( 𝑠 = 𝑅 → 𝑁 = 𝑧 ) ↔ ⦋ 𝑅 / 𝑠 ⦌ 𝑁 = 𝑧 ) )
66	44 65	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) → ( ∀ 𝑠 ( 𝑠 = 𝑅 → 𝑁 = 𝑧 ) ↔ ⦋ 𝑅 / 𝑠 ⦌ 𝑁 = 𝑧 ) )
67		eqcom	⊢ ( ⦋ 𝑅 / 𝑠 ⦌ 𝑁 = 𝑧 ↔ 𝑧 = ⦋ 𝑅 / 𝑠 ⦌ 𝑁 )
68	66 67	bitrdi	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) → ( ∀ 𝑠 ( 𝑠 = 𝑅 → 𝑁 = 𝑧 ) ↔ 𝑧 = ⦋ 𝑅 / 𝑠 ⦌ 𝑁 ) )
69	63 68	bitrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ) ) ∧ 𝜓 ) → ( ∀ 𝑠 ∈ 𝐴 ( ( ( ¬ 𝑠 ≤ 𝑊 ∧ 𝜑 ) ∧ ( 𝑠 ∨ ( 𝑅 ∧ 𝑊 ) ) = 𝑅 ) → 𝑧 = ( 𝑁 ∨ ( 𝑅 ∧ 𝑊 ) ) ) ↔ 𝑧 = ⦋ 𝑅 / 𝑠 ⦌ 𝑁 ) )