Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cdlemefrs29bpre0 Structured version   Visualization version   GIF version

Theorem cdlemefrs29bpre0 37689
Description: TODO fix comment. (Contributed by NM, 29-Mar-2013.)
Hypotheses
Ref Expression
cdlemefrs27.b 𝐵 = (Base‘𝐾)
cdlemefrs27.l = (le‘𝐾)
cdlemefrs27.j = (join‘𝐾)
cdlemefrs27.m = (meet‘𝐾)
cdlemefrs27.a 𝐴 = (Atoms‘𝐾)
cdlemefrs27.h 𝐻 = (LHyp‘𝐾)
cdlemefrs27.eq (𝑠 = 𝑅 → (𝜑𝜓))
cdlemefrs27.nb ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑))) → 𝑁𝐵)
Assertion
Ref Expression
cdlemefrs29bpre0 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) → (∀𝑠𝐴 (((¬ 𝑠 𝑊𝜑) ∧ (𝑠 (𝑅 𝑊)) = 𝑅) → 𝑧 = (𝑁 (𝑅 𝑊))) ↔ 𝑧 = 𝑅 / 𝑠𝑁))
Distinct variable groups:   𝑧,𝑠   𝐴,𝑠   𝐻,𝑠   ,𝑠   𝐾,𝑠   ,𝑠   𝑃,𝑠   𝑄,𝑠   𝑅,𝑠   𝑊,𝑠   𝜓,𝑠
Allowed substitution hints:   𝜑(𝑧,𝑠)   𝜓(𝑧)   𝐴(𝑧)   𝐵(𝑧,𝑠)   𝑃(𝑧)   𝑄(𝑧)   𝑅(𝑧)   𝐻(𝑧)   (𝑧)   𝐾(𝑧)   (𝑧)   (𝑧,𝑠)   𝑁(𝑧,𝑠)   𝑊(𝑧)

Proof of Theorem cdlemefrs29bpre0
StepHypRef Expression
1 df-ral 3111 . . 3 (∀𝑠𝐴 (((¬ 𝑠 𝑊𝜑) ∧ (𝑠 (𝑅 𝑊)) = 𝑅) → 𝑧 = (𝑁 (𝑅 𝑊))) ↔ ∀𝑠(𝑠𝐴 → (((¬ 𝑠 𝑊𝜑) ∧ (𝑠 (𝑅 𝑊)) = 𝑅) → 𝑧 = (𝑁 (𝑅 𝑊)))))
2 anass 472 . . . . . . 7 (((𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑)) ∧ (𝑠 (𝑅 𝑊)) = 𝑅) ↔ (𝑠𝐴 ∧ ((¬ 𝑠 𝑊𝜑) ∧ (𝑠 (𝑅 𝑊)) = 𝑅)))
32imbi1i 353 . . . . . 6 ((((𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑)) ∧ (𝑠 (𝑅 𝑊)) = 𝑅) → 𝑧 = (𝑁 (𝑅 𝑊))) ↔ ((𝑠𝐴 ∧ ((¬ 𝑠 𝑊𝜑) ∧ (𝑠 (𝑅 𝑊)) = 𝑅)) → 𝑧 = (𝑁 (𝑅 𝑊))))
4 impexp 454 . . . . . 6 ((((𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑)) ∧ (𝑠 (𝑅 𝑊)) = 𝑅) → 𝑧 = (𝑁 (𝑅 𝑊))) ↔ ((𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑)) → ((𝑠 (𝑅 𝑊)) = 𝑅𝑧 = (𝑁 (𝑅 𝑊)))))
5 impexp 454 . . . . . 6 (((𝑠𝐴 ∧ ((¬ 𝑠 𝑊𝜑) ∧ (𝑠 (𝑅 𝑊)) = 𝑅)) → 𝑧 = (𝑁 (𝑅 𝑊))) ↔ (𝑠𝐴 → (((¬ 𝑠 𝑊𝜑) ∧ (𝑠 (𝑅 𝑊)) = 𝑅) → 𝑧 = (𝑁 (𝑅 𝑊)))))
63, 4, 53bitr3ri 305 . . . . 5 ((𝑠𝐴 → (((¬ 𝑠 𝑊𝜑) ∧ (𝑠 (𝑅 𝑊)) = 𝑅) → 𝑧 = (𝑁 (𝑅 𝑊)))) ↔ ((𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑)) → ((𝑠 (𝑅 𝑊)) = 𝑅𝑧 = (𝑁 (𝑅 𝑊)))))
7 simpl11 1245 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) ∧ (𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
8 simpl2r 1224 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) ∧ (𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑))) → (𝑅𝐴 ∧ ¬ 𝑅 𝑊))
9 cdlemefrs27.l . . . . . . . . . . . . 13 = (le‘𝐾)
10 cdlemefrs27.m . . . . . . . . . . . . 13 = (meet‘𝐾)
11 eqid 2798 . . . . . . . . . . . . 13 (0.‘𝐾) = (0.‘𝐾)
12 cdlemefrs27.a . . . . . . . . . . . . 13 𝐴 = (Atoms‘𝐾)
13 cdlemefrs27.h . . . . . . . . . . . . 13 𝐻 = (LHyp‘𝐾)
149, 10, 11, 12, 13lhpmat 37323 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) → (𝑅 𝑊) = (0.‘𝐾))
157, 8, 14syl2anc 587 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) ∧ (𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑))) → (𝑅 𝑊) = (0.‘𝐾))
1615oveq2d 7151 . . . . . . . . . 10 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) ∧ (𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑))) → (𝑠 (𝑅 𝑊)) = (𝑠 (0.‘𝐾)))
17 simp11l 1281 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) → 𝐾 ∈ HL)
18 hlol 36654 . . . . . . . . . . . . 13 (𝐾 ∈ HL → 𝐾 ∈ OL)
1917, 18syl 17 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) → 𝐾 ∈ OL)
2019adantr 484 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) ∧ (𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑))) → 𝐾 ∈ OL)
21 simprl 770 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) ∧ (𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑))) → 𝑠𝐴)
22 cdlemefrs27.b . . . . . . . . . . . . 13 𝐵 = (Base‘𝐾)
2322, 12atbase 36582 . . . . . . . . . . . 12 (𝑠𝐴𝑠𝐵)
2421, 23syl 17 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) ∧ (𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑))) → 𝑠𝐵)
25 cdlemefrs27.j . . . . . . . . . . . 12 = (join‘𝐾)
2622, 25, 11olj01 36518 . . . . . . . . . . 11 ((𝐾 ∈ OL ∧ 𝑠𝐵) → (𝑠 (0.‘𝐾)) = 𝑠)
2720, 24, 26syl2anc 587 . . . . . . . . . 10 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) ∧ (𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑))) → (𝑠 (0.‘𝐾)) = 𝑠)
2816, 27eqtrd 2833 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) ∧ (𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑))) → (𝑠 (𝑅 𝑊)) = 𝑠)
2928eqeq1d 2800 . . . . . . . 8 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) ∧ (𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑))) → ((𝑠 (𝑅 𝑊)) = 𝑅𝑠 = 𝑅))
3015oveq2d 7151 . . . . . . . . . 10 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) ∧ (𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑))) → (𝑁 (𝑅 𝑊)) = (𝑁 (0.‘𝐾)))
31 simpl1 1188 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) ∧ (𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑))) → ((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)))
32 simpl2l 1223 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) ∧ (𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑))) → 𝑃𝑄)
33 simprr 772 . . . . . . . . . . . 12 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) ∧ (𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑))) → (¬ 𝑠 𝑊𝜑))
34 cdlemefrs27.nb . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ 𝑃𝑄 ∧ (𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑))) → 𝑁𝐵)
3531, 32, 21, 33, 34syl112anc 1371 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) ∧ (𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑))) → 𝑁𝐵)
3622, 25, 11olj01 36518 . . . . . . . . . . 11 ((𝐾 ∈ OL ∧ 𝑁𝐵) → (𝑁 (0.‘𝐾)) = 𝑁)
3720, 35, 36syl2anc 587 . . . . . . . . . 10 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) ∧ (𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑))) → (𝑁 (0.‘𝐾)) = 𝑁)
3830, 37eqtrd 2833 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) ∧ (𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑))) → (𝑁 (𝑅 𝑊)) = 𝑁)
3938eqeq2d 2809 . . . . . . . 8 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) ∧ (𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑))) → (𝑧 = (𝑁 (𝑅 𝑊)) ↔ 𝑧 = 𝑁))
4029, 39imbi12d 348 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) ∧ (𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑))) → (((𝑠 (𝑅 𝑊)) = 𝑅𝑧 = (𝑁 (𝑅 𝑊))) ↔ (𝑠 = 𝑅𝑧 = 𝑁)))
4140pm5.74da 803 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) → (((𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑)) → ((𝑠 (𝑅 𝑊)) = 𝑅𝑧 = (𝑁 (𝑅 𝑊)))) ↔ ((𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑)) → (𝑠 = 𝑅𝑧 = 𝑁))))
42 impexp 454 . . . . . . 7 ((((𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑)) ∧ 𝑠 = 𝑅) → 𝑧 = 𝑁) ↔ ((𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑)) → (𝑠 = 𝑅𝑧 = 𝑁)))
43 simp2rl 1239 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) → 𝑅𝐴)
44 simp2rr 1240 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) → ¬ 𝑅 𝑊)
45 simp3 1135 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) → 𝜓)
46 eleq1 2877 . . . . . . . . . . . . 13 (𝑠 = 𝑅 → (𝑠𝐴𝑅𝐴))
47 breq1 5033 . . . . . . . . . . . . . . 15 (𝑠 = 𝑅 → (𝑠 𝑊𝑅 𝑊))
4847notbid 321 . . . . . . . . . . . . . 14 (𝑠 = 𝑅 → (¬ 𝑠 𝑊 ↔ ¬ 𝑅 𝑊))
49 cdlemefrs27.eq . . . . . . . . . . . . . 14 (𝑠 = 𝑅 → (𝜑𝜓))
5048, 49anbi12d 633 . . . . . . . . . . . . 13 (𝑠 = 𝑅 → ((¬ 𝑠 𝑊𝜑) ↔ (¬ 𝑅 𝑊𝜓)))
5146, 50anbi12d 633 . . . . . . . . . . . 12 (𝑠 = 𝑅 → ((𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑)) ↔ (𝑅𝐴 ∧ (¬ 𝑅 𝑊𝜓))))
5251biimprcd 253 . . . . . . . . . . 11 ((𝑅𝐴 ∧ (¬ 𝑅 𝑊𝜓)) → (𝑠 = 𝑅 → (𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑))))
5343, 44, 45, 52syl12anc 835 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) → (𝑠 = 𝑅 → (𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑))))
5453pm4.71rd 566 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) → (𝑠 = 𝑅 ↔ ((𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑)) ∧ 𝑠 = 𝑅)))
5554imbi1d 345 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) → ((𝑠 = 𝑅𝑧 = 𝑁) ↔ (((𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑)) ∧ 𝑠 = 𝑅) → 𝑧 = 𝑁)))
56 eqcom 2805 . . . . . . . . 9 (𝑧 = 𝑁𝑁 = 𝑧)
5756imbi2i 339 . . . . . . . 8 ((𝑠 = 𝑅𝑧 = 𝑁) ↔ (𝑠 = 𝑅𝑁 = 𝑧))
5855, 57bitr3di 289 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) → ((((𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑)) ∧ 𝑠 = 𝑅) → 𝑧 = 𝑁) ↔ (𝑠 = 𝑅𝑁 = 𝑧)))
5942, 58bitr3id 288 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) → (((𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑)) → (𝑠 = 𝑅𝑧 = 𝑁)) ↔ (𝑠 = 𝑅𝑁 = 𝑧)))
6041, 59bitrd 282 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) → (((𝑠𝐴 ∧ (¬ 𝑠 𝑊𝜑)) → ((𝑠 (𝑅 𝑊)) = 𝑅𝑧 = (𝑁 (𝑅 𝑊)))) ↔ (𝑠 = 𝑅𝑁 = 𝑧)))
616, 60syl5bb 286 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) → ((𝑠𝐴 → (((¬ 𝑠 𝑊𝜑) ∧ (𝑠 (𝑅 𝑊)) = 𝑅) → 𝑧 = (𝑁 (𝑅 𝑊)))) ↔ (𝑠 = 𝑅𝑁 = 𝑧)))
6261albidv 1921 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) → (∀𝑠(𝑠𝐴 → (((¬ 𝑠 𝑊𝜑) ∧ (𝑠 (𝑅 𝑊)) = 𝑅) → 𝑧 = (𝑁 (𝑅 𝑊)))) ↔ ∀𝑠(𝑠 = 𝑅𝑁 = 𝑧)))
631, 62syl5bb 286 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) → (∀𝑠𝐴 (((¬ 𝑠 𝑊𝜑) ∧ (𝑠 (𝑅 𝑊)) = 𝑅) → 𝑧 = (𝑁 (𝑅 𝑊))) ↔ ∀𝑠(𝑠 = 𝑅𝑁 = 𝑧)))
64 nfcv 2955 . . . . 5 𝑠𝑧
6564csbiebg 3860 . . . 4 (𝑅𝐴 → (∀𝑠(𝑠 = 𝑅𝑁 = 𝑧) ↔ 𝑅 / 𝑠𝑁 = 𝑧))
6643, 65syl 17 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) → (∀𝑠(𝑠 = 𝑅𝑁 = 𝑧) ↔ 𝑅 / 𝑠𝑁 = 𝑧))
67 eqcom 2805 . . 3 (𝑅 / 𝑠𝑁 = 𝑧𝑧 = 𝑅 / 𝑠𝑁)
6866, 67syl6bb 290 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) → (∀𝑠(𝑠 = 𝑅𝑁 = 𝑧) ↔ 𝑧 = 𝑅 / 𝑠𝑁))
6963, 68bitrd 282 1 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊) ∧ (𝑄𝐴 ∧ ¬ 𝑄 𝑊)) ∧ (𝑃𝑄 ∧ (𝑅𝐴 ∧ ¬ 𝑅 𝑊)) ∧ 𝜓) → (∀𝑠𝐴 (((¬ 𝑠 𝑊𝜑) ∧ (𝑠 (𝑅 𝑊)) = 𝑅) → 𝑧 = (𝑁 (𝑅 𝑊))) ↔ 𝑧 = 𝑅 / 𝑠𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1084  wal 1536   = wceq 1538  wcel 2111  wne 2987  wral 3106  csb 3828   class class class wbr 5030  cfv 6324  (class class class)co 7135  Basecbs 16475  lecple 16564  joincjn 17546  meetcmee 17547  0.cp0 17639  OLcol 36467  Atomscatm 36556  HLchlt 36643  LHypclh 37277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-proset 17530  df-poset 17548  df-plt 17560  df-lub 17576  df-glb 17577  df-join 17578  df-meet 17579  df-p0 17641  df-lat 17648  df-oposet 36469  df-ol 36471  df-oml 36472  df-covers 36559  df-ats 36560  df-atl 36591  df-cvlat 36615  df-hlat 36644  df-lhyp 37281
This theorem is referenced by:  cdlemefrs29bpre1  37690  cdlemefrs32fva  37693  cdlemefr29bpre0N  37699  cdlemefs29bpre0N  37709
  Copyright terms: Public domain W3C validator