Theorem cdlemk34 41573

Description: Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. Part of attempt to simplify hypotheses. (Contributed by NM, 18-Jul-2013.)

Hypotheses

Ref	Expression
cdlemk3.b	⊢ 𝐵 = (Base‘𝐾)
cdlemk3.l	⊢ ≤ = (le‘𝐾)
cdlemk3.j	⊢ ∨ = (join‘𝐾)
cdlemk3.m	⊢ ∧ = (meet‘𝐾)
cdlemk3.a	⊢ 𝐴 = (Atoms‘𝐾)
cdlemk3.h	⊢ 𝐻 = (LHyp‘𝐾)
cdlemk3.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemk3.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
cdlemk3.s	⊢ 𝑆 = (𝑓 ∈ 𝑇 ↦ (℩𝑖 ∈ 𝑇 (𝑖‘𝑃) = ((𝑃 ∨ (𝑅‘𝑓)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑓 ∘ ◡𝐹))))))
cdlemk3.u1	⊢ 𝑌 = (𝑑 ∈ 𝑇, 𝑒 ∈ 𝑇 ↦ (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑))))))
cdlemk3.x	⊢ 𝑋 = (℩𝑧 ∈ 𝑇 ∀𝑏 ∈ 𝑇 ((𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)) → 𝑧 = (𝑏𝑌𝐺)))

Assertion

Ref	Expression
cdlemk34	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) → 𝑋 = (℩𝑧 ∈ 𝑇 ∀𝑏 ∈ 𝑇 ((𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)) → (𝑧‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹)))) ∨ (𝑅‘(𝐺 ∘ ◡𝑏)))))))

Distinct variable groups:   𝑒,𝑑,𝑓,𝑖, ∧   ≤ ,𝑖   ∨ ,𝑑,𝑒,𝑓,𝑖   𝐴,𝑖   𝑗,𝑑,𝑒,𝑓,𝑖,𝐹   𝐺,𝑑,𝑒,𝑗   𝑖,𝐻   𝑖,𝐾   𝑓,𝑁,𝑖   𝑃,𝑑,𝑒,𝑓,𝑖   𝑅,𝑑,𝑒,𝑓,𝑖   𝑇,𝑑,𝑒,𝑓,𝑖   𝑊,𝑑,𝑒,𝑓,𝑖,𝑏   ∧ ,𝑗   ≤ ,𝑗   ∨ ,𝑗   𝐴,𝑗   𝑗,𝐹   𝑗,𝐻   𝑗,𝐾   𝑗,𝑁   𝑃,𝑗   𝑅,𝑗   𝑏,𝑑,𝑆,𝑒,𝑗   𝑇,𝑗   𝑗,𝑊   𝐹,𝑑,𝑒   ≤ ,𝑒   𝑓,𝐺,𝑖   ≤ ,𝑏   𝐴,𝑏,𝑧   𝐵,𝑏,𝑧   𝐹,𝑏,𝑧   𝐺,𝑏,𝑧   𝐻,𝑏   𝐾,𝑏   𝑁,𝑏   𝑃,𝑏   𝑅,𝑏,𝑧   𝑇,𝑏,𝑧   𝑊,𝑏,𝑧   𝑌,𝑏,𝑧   𝑧,𝑑,𝑒,𝑓,𝑖,𝑗   𝑧, ≤   𝑧,𝐴   𝑧,𝐻   𝑧,𝐾   𝑧,𝑁   𝑧,𝑃

Allowed substitution hints:   𝐴(𝑒,𝑓,𝑑)   𝐵(𝑒,𝑓,𝑖,𝑗,𝑑)   𝑆(𝑧,𝑓,𝑖)   𝐻(𝑒,𝑓,𝑑)   ∨ (𝑧,𝑏)   𝐾(𝑒,𝑓,𝑑)   ≤ (𝑓,𝑑)   ∧ (𝑧,𝑏)   𝑁(𝑒,𝑑)   𝑋(𝑧,𝑒,𝑓,𝑖,𝑗,𝑏,𝑑)   𝑌(𝑒,𝑓,𝑖,𝑗,𝑑)

Proof of Theorem cdlemk34

Step	Hyp	Ref	Expression
1		cdlemk3.x	. 2 ⊢ 𝑋 = (℩𝑧 ∈ 𝑇 ∀𝑏 ∈ 𝑇 ((𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)) → 𝑧 = (𝑏𝑌𝐺)))
2		fveq1 6881	. . . . . . . . 9 ⊢ (𝑧 = (𝑏𝑌𝐺) → (𝑧‘𝑃) = ((𝑏𝑌𝐺)‘𝑃))
3		simpll1 1229	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) ∧ (𝑧‘𝑃) = ((𝑏𝑌𝐺)‘𝑃)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
4		simplr1 1232	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) ∧ (𝑧‘𝑃) = ((𝑏𝑌𝐺)‘𝑃)) → 𝑧 ∈ 𝑇)
5		simpl1 1208	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
6		simpl3r 1246	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) → (𝑅‘𝐹) = (𝑅‘𝑁))
7		simp22l 1309	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) → 𝐺 ∈ 𝑇)
8	7	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) → 𝐺 ∈ 𝑇)
9	5, 6, 8	3jca 1144	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐺 ∈ 𝑇))
10	9	adantr 485	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) ∧ (𝑧‘𝑃) = ((𝑏𝑌𝐺)‘𝑃)) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐺 ∈ 𝑇))
11		simp21l 1307	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) → 𝐹 ∈ 𝑇)
12	11	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) → 𝐹 ∈ 𝑇)
13		simpr2 1212	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) → 𝑏 ∈ 𝑇)
14		simpl23 1270	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) → 𝑁 ∈ 𝑇)
15	12, 13, 14	3jca 1144	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) → (𝐹 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇))
16	15	adantr 485	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) ∧ (𝑧‘𝑃) = ((𝑏𝑌𝐺)‘𝑃)) → (𝐹 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇))
17		simpr32 1281	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) → (𝑅‘𝑏) ≠ (𝑅‘𝐹))
18		simpr33 1282	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) → (𝑅‘𝑏) ≠ (𝑅‘𝐺))
19	17, 18	jca 520	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) → ((𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))
20	19	adantr 485	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) ∧ (𝑧‘𝑃) = ((𝑏𝑌𝐺)‘𝑃)) → ((𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))
21		simp21r 1308	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) → 𝐹 ≠ ( I ↾ 𝐵))
22	21	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) → 𝐹 ≠ ( I ↾ 𝐵))
23		simp22r 1310	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) → 𝐺 ≠ ( I ↾ 𝐵))
24	23	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) → 𝐺 ≠ ( I ↾ 𝐵))
25		simpr31 1280	. . . . . . . . . . . . . 14 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) → 𝑏 ≠ ( I ↾ 𝐵))
26	22, 24, 25	3jca 1144	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) → (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑏 ≠ ( I ↾ 𝐵)))
27	26	adantr 485	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) ∧ (𝑧‘𝑃) = ((𝑏𝑌𝐺)‘𝑃)) → (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑏 ≠ ( I ↾ 𝐵)))
28		simpl3l 1245	. . . . . . . . . . . . 13 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
29	28	adantr 485	. . . . . . . . . . . 12 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) ∧ (𝑧‘𝑃) = ((𝑏𝑌𝐺)‘𝑃)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
30		cdlemk3.b	. . . . . . . . . . . . 13 ⊢ 𝐵 = (Base‘𝐾)
31		cdlemk3.l	. . . . . . . . . . . . 13 ⊢ ≤ = (le‘𝐾)
32		cdlemk3.j	. . . . . . . . . . . . 13 ⊢ ∨ = (join‘𝐾)
33		cdlemk3.m	. . . . . . . . . . . . 13 ⊢ ∧ = (meet‘𝐾)
34		cdlemk3.a	. . . . . . . . . . . . 13 ⊢ 𝐴 = (Atoms‘𝐾)
35		cdlemk3.h	. . . . . . . . . . . . 13 ⊢ 𝐻 = (LHyp‘𝐾)
36		cdlemk3.t	. . . . . . . . . . . . 13 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
37		cdlemk3.r	. . . . . . . . . . . . 13 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
38		cdlemk3.s	. . . . . . . . . . . . 13 ⊢ 𝑆 = (𝑓 ∈ 𝑇 ↦ (℩𝑖 ∈ 𝑇 (𝑖‘𝑃) = ((𝑃 ∨ (𝑅‘𝑓)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑓 ∘ ◡𝐹))))))
39		cdlemk3.u1	. . . . . . . . . . . . 13 ⊢ 𝑌 = (𝑑 ∈ 𝑇, 𝑒 ∈ 𝑇 ↦ (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑))))))
40	30, 31, 32, 33, 34, 35, 36, 37, 38, 39	cdlemkuel-3 41561	. . . . . . . . . . . 12 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁) ∧ 𝐺 ∈ 𝑇) ∧ (𝐹 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ (((𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵) ∧ 𝑏 ≠ ( I ↾ 𝐵)) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))) → (𝑏𝑌𝐺) ∈ 𝑇)
41	10, 16, 20, 27, 29, 40	syl113anc 1407	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) ∧ (𝑧‘𝑃) = ((𝑏𝑌𝐺)‘𝑃)) → (𝑏𝑌𝐺) ∈ 𝑇)
42		simpr 489	. . . . . . . . . . 11 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) ∧ (𝑧‘𝑃) = ((𝑏𝑌𝐺)‘𝑃)) → (𝑧‘𝑃) = ((𝑏𝑌𝐺)‘𝑃))
43	31, 34, 35, 36	cdlemd 40870	. . . . . . . . . . 11 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑧 ∈ 𝑇 ∧ (𝑏𝑌𝐺) ∈ 𝑇) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑧‘𝑃) = ((𝑏𝑌𝐺)‘𝑃)) → 𝑧 = (𝑏𝑌𝐺))
44	3, 4, 41, 29, 42, 43	syl311anc 1409	. . . . . . . . . 10 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) ∧ (𝑧‘𝑃) = ((𝑏𝑌𝐺)‘𝑃)) → 𝑧 = (𝑏𝑌𝐺))
45	44	ex 417	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) → ((𝑧‘𝑃) = ((𝑏𝑌𝐺)‘𝑃) → 𝑧 = (𝑏𝑌𝐺)))
46	2, 45	impbid2 229	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) → (𝑧 = (𝑏𝑌𝐺) ↔ (𝑧‘𝑃) = ((𝑏𝑌𝐺)‘𝑃)))
47		simp1 1152	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
48		simp3r 1219	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) → (𝑅‘𝐹) = (𝑅‘𝑁))
49	47, 48	jca 520	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)))
50	49	adantr 485	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) → ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)))
51	22, 25, 24	3jca 1144	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) → (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝑏 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)))
52	30, 31, 32, 33, 34, 35, 36, 37, 38, 39	cdlemk32 41560	. . . . . . . . . 10 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝐹 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇) ∧ 𝐺 ∈ 𝑇) ∧ (((𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ 𝑏 ≠ ( I ↾ 𝐵) ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))) → ((𝑏𝑌𝐺)‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹)))) ∨ (𝑅‘(𝐺 ∘ ◡𝑏)))))
53	50, 15, 8, 19, 51, 28, 52	syl123anc 1412	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) → ((𝑏𝑌𝐺)‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹)))) ∨ (𝑅‘(𝐺 ∘ ◡𝑏)))))
54	53	eqeq2d 2780	. . . . . . . 8 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) → ((𝑧‘𝑃) = ((𝑏𝑌𝐺)‘𝑃) ↔ (𝑧‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹)))) ∨ (𝑅‘(𝐺 ∘ ◡𝑏))))))
55	46, 54	bitrd 282	. . . . . . 7 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ (𝑧 ∈ 𝑇 ∧ 𝑏 ∈ 𝑇 ∧ (𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)))) → (𝑧 = (𝑏𝑌𝐺) ↔ (𝑧‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹)))) ∨ (𝑅‘(𝐺 ∘ ◡𝑏))))))
56	55	3exp2 1371	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) → (𝑧 ∈ 𝑇 → (𝑏 ∈ 𝑇 → ((𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)) → (𝑧 = (𝑏𝑌𝐺) ↔ (𝑧‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹)))) ∨ (𝑅‘(𝐺 ∘ ◡𝑏)))))))))
57	56	imp31 422	. . . . 5 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ 𝑧 ∈ 𝑇) ∧ 𝑏 ∈ 𝑇) → ((𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)) → (𝑧 = (𝑏𝑌𝐺) ↔ (𝑧‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹)))) ∨ (𝑅‘(𝐺 ∘ ◡𝑏)))))))
58	57	pm5.74d 276	. . . 4 ⊢ (((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ 𝑧 ∈ 𝑇) ∧ 𝑏 ∈ 𝑇) → (((𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)) → 𝑧 = (𝑏𝑌𝐺)) ↔ ((𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)) → (𝑧‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹)))) ∨ (𝑅‘(𝐺 ∘ ◡𝑏)))))))
59	58	ralbidva 3192	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) ∧ 𝑧 ∈ 𝑇) → (∀𝑏 ∈ 𝑇 ((𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)) → 𝑧 = (𝑏𝑌𝐺)) ↔ ∀𝑏 ∈ 𝑇 ((𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)) → (𝑧‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹)))) ∨ (𝑅‘(𝐺 ∘ ◡𝑏)))))))
60	59	riotabidva 7387	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) → (℩𝑧 ∈ 𝑇 ∀𝑏 ∈ 𝑇 ((𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)) → 𝑧 = (𝑏𝑌𝐺))) = (℩𝑧 ∈ 𝑇 ∀𝑏 ∈ 𝑇 ((𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)) → (𝑧‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹)))) ∨ (𝑅‘(𝐺 ∘ ◡𝑏)))))))
61	1, 60	eqtrid 2816	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 ∈ 𝑇 ∧ 𝐹 ≠ ( I ↾ 𝐵)) ∧ (𝐺 ∈ 𝑇 ∧ 𝐺 ≠ ( I ↾ 𝐵)) ∧ 𝑁 ∈ 𝑇) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅‘𝐹) = (𝑅‘𝑁))) → 𝑋 = (℩𝑧 ∈ 𝑇 ∀𝑏 ∈ 𝑇 ((𝑏 ≠ ( I ↾ 𝐵) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐹) ∧ (𝑅‘𝑏) ≠ (𝑅‘𝐺)) → (𝑧‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ (((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ◡𝐹)))) ∨ (𝑅‘(𝐺 ∘ ◡𝑏)))))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149   ≠ wne 2964  ∀wral 3085   class class class wbr 5113   ↦ cmpt 5196   I cid 5556  ^◡ccnv 5661   ↾ cres 5664   ∘ ccom 5666  ‘cfv 6537  ℩crio 7367  (class class class)co 7411   ∈ cmpo 7413  Basecbs 17268  lecple 17316  joincjn 18366  meetcmee 18367  Atomscatm 39926  HLchlt 40013  LHypclh 40647  LTrncltrn 40764  trLctrl 40821

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-riotaBAD 39616

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-iin 4963  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7985  df-2nd 7986  df-undef 8268  df-map 8825  df-proset 18349  df-poset 18368  df-plt 18383  df-lub 18399  df-glb 18400  df-join 18401  df-meet 18402  df-p0 18478  df-p1 18479  df-lat 18487  df-clat 18554  df-oposet 39839  df-ol 39841  df-oml 39842  df-covers 39929  df-ats 39930  df-atl 39961  df-cvlat 39985  df-hlat 40014  df-llines 40161  df-lplanes 40162  df-lvols 40163  df-lines 40164  df-psubsp 40166  df-pmap 40167  df-padd 40459  df-lhyp 40651  df-laut 40652  df-ldil 40767  df-ltrn 40768  df-trl 40822

This theorem is referenced by:  cdlemk35  41575