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

Theorem oposlem 38138
Description: Lemma for orthoposet properties. (Contributed by NM, 20-Oct-2011.)
Hypotheses
Ref Expression
oposlem.b 𝐡 = (Baseβ€˜πΎ)
oposlem.l ≀ = (leβ€˜πΎ)
oposlem.o βŠ₯ = (ocβ€˜πΎ)
oposlem.j ∨ = (joinβ€˜πΎ)
oposlem.m ∧ = (meetβ€˜πΎ)
oposlem.f 0 = (0.β€˜πΎ)
oposlem.u 1 = (1.β€˜πΎ)
Assertion
Ref Expression
oposlem ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ ((( βŠ₯ β€˜π‘‹) ∈ 𝐡 ∧ ( βŠ₯ β€˜( βŠ₯ β€˜π‘‹)) = 𝑋 ∧ (𝑋 ≀ π‘Œ β†’ ( βŠ₯ β€˜π‘Œ) ≀ ( βŠ₯ β€˜π‘‹))) ∧ (𝑋 ∨ ( βŠ₯ β€˜π‘‹)) = 1 ∧ (𝑋 ∧ ( βŠ₯ β€˜π‘‹)) = 0 ))

Proof of Theorem oposlem
Dummy variables π‘₯ 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oposlem.b . . . . 5 𝐡 = (Baseβ€˜πΎ)
2 eqid 2732 . . . . 5 (lubβ€˜πΎ) = (lubβ€˜πΎ)
3 eqid 2732 . . . . 5 (glbβ€˜πΎ) = (glbβ€˜πΎ)
4 oposlem.l . . . . 5 ≀ = (leβ€˜πΎ)
5 oposlem.o . . . . 5 βŠ₯ = (ocβ€˜πΎ)
6 oposlem.j . . . . 5 ∨ = (joinβ€˜πΎ)
7 oposlem.m . . . . 5 ∧ = (meetβ€˜πΎ)
8 oposlem.f . . . . 5 0 = (0.β€˜πΎ)
9 oposlem.u . . . . 5 1 = (1.β€˜πΎ)
101, 2, 3, 4, 5, 6, 7, 8, 9isopos 38136 . . . 4 (𝐾 ∈ OP ↔ ((𝐾 ∈ Poset ∧ 𝐡 ∈ dom (lubβ€˜πΎ) ∧ 𝐡 ∈ dom (glbβ€˜πΎ)) ∧ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 ((( βŠ₯ β€˜π‘₯) ∈ 𝐡 ∧ ( βŠ₯ β€˜( βŠ₯ β€˜π‘₯)) = π‘₯ ∧ (π‘₯ ≀ 𝑦 β†’ ( βŠ₯ β€˜π‘¦) ≀ ( βŠ₯ β€˜π‘₯))) ∧ (π‘₯ ∨ ( βŠ₯ β€˜π‘₯)) = 1 ∧ (π‘₯ ∧ ( βŠ₯ β€˜π‘₯)) = 0 )))
1110simprbi 497 . . 3 (𝐾 ∈ OP β†’ βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 ((( βŠ₯ β€˜π‘₯) ∈ 𝐡 ∧ ( βŠ₯ β€˜( βŠ₯ β€˜π‘₯)) = π‘₯ ∧ (π‘₯ ≀ 𝑦 β†’ ( βŠ₯ β€˜π‘¦) ≀ ( βŠ₯ β€˜π‘₯))) ∧ (π‘₯ ∨ ( βŠ₯ β€˜π‘₯)) = 1 ∧ (π‘₯ ∧ ( βŠ₯ β€˜π‘₯)) = 0 ))
12 fveq2 6891 . . . . . . 7 (π‘₯ = 𝑋 β†’ ( βŠ₯ β€˜π‘₯) = ( βŠ₯ β€˜π‘‹))
1312eleq1d 2818 . . . . . 6 (π‘₯ = 𝑋 β†’ (( βŠ₯ β€˜π‘₯) ∈ 𝐡 ↔ ( βŠ₯ β€˜π‘‹) ∈ 𝐡))
14 2fveq3 6896 . . . . . . 7 (π‘₯ = 𝑋 β†’ ( βŠ₯ β€˜( βŠ₯ β€˜π‘₯)) = ( βŠ₯ β€˜( βŠ₯ β€˜π‘‹)))
15 id 22 . . . . . . 7 (π‘₯ = 𝑋 β†’ π‘₯ = 𝑋)
1614, 15eqeq12d 2748 . . . . . 6 (π‘₯ = 𝑋 β†’ (( βŠ₯ β€˜( βŠ₯ β€˜π‘₯)) = π‘₯ ↔ ( βŠ₯ β€˜( βŠ₯ β€˜π‘‹)) = 𝑋))
17 breq1 5151 . . . . . . 7 (π‘₯ = 𝑋 β†’ (π‘₯ ≀ 𝑦 ↔ 𝑋 ≀ 𝑦))
1812breq2d 5160 . . . . . . 7 (π‘₯ = 𝑋 β†’ (( βŠ₯ β€˜π‘¦) ≀ ( βŠ₯ β€˜π‘₯) ↔ ( βŠ₯ β€˜π‘¦) ≀ ( βŠ₯ β€˜π‘‹)))
1917, 18imbi12d 344 . . . . . 6 (π‘₯ = 𝑋 β†’ ((π‘₯ ≀ 𝑦 β†’ ( βŠ₯ β€˜π‘¦) ≀ ( βŠ₯ β€˜π‘₯)) ↔ (𝑋 ≀ 𝑦 β†’ ( βŠ₯ β€˜π‘¦) ≀ ( βŠ₯ β€˜π‘‹))))
2013, 16, 193anbi123d 1436 . . . . 5 (π‘₯ = 𝑋 β†’ ((( βŠ₯ β€˜π‘₯) ∈ 𝐡 ∧ ( βŠ₯ β€˜( βŠ₯ β€˜π‘₯)) = π‘₯ ∧ (π‘₯ ≀ 𝑦 β†’ ( βŠ₯ β€˜π‘¦) ≀ ( βŠ₯ β€˜π‘₯))) ↔ (( βŠ₯ β€˜π‘‹) ∈ 𝐡 ∧ ( βŠ₯ β€˜( βŠ₯ β€˜π‘‹)) = 𝑋 ∧ (𝑋 ≀ 𝑦 β†’ ( βŠ₯ β€˜π‘¦) ≀ ( βŠ₯ β€˜π‘‹)))))
2115, 12oveq12d 7429 . . . . . 6 (π‘₯ = 𝑋 β†’ (π‘₯ ∨ ( βŠ₯ β€˜π‘₯)) = (𝑋 ∨ ( βŠ₯ β€˜π‘‹)))
2221eqeq1d 2734 . . . . 5 (π‘₯ = 𝑋 β†’ ((π‘₯ ∨ ( βŠ₯ β€˜π‘₯)) = 1 ↔ (𝑋 ∨ ( βŠ₯ β€˜π‘‹)) = 1 ))
2315, 12oveq12d 7429 . . . . . 6 (π‘₯ = 𝑋 β†’ (π‘₯ ∧ ( βŠ₯ β€˜π‘₯)) = (𝑋 ∧ ( βŠ₯ β€˜π‘‹)))
2423eqeq1d 2734 . . . . 5 (π‘₯ = 𝑋 β†’ ((π‘₯ ∧ ( βŠ₯ β€˜π‘₯)) = 0 ↔ (𝑋 ∧ ( βŠ₯ β€˜π‘‹)) = 0 ))
2520, 22, 243anbi123d 1436 . . . 4 (π‘₯ = 𝑋 β†’ (((( βŠ₯ β€˜π‘₯) ∈ 𝐡 ∧ ( βŠ₯ β€˜( βŠ₯ β€˜π‘₯)) = π‘₯ ∧ (π‘₯ ≀ 𝑦 β†’ ( βŠ₯ β€˜π‘¦) ≀ ( βŠ₯ β€˜π‘₯))) ∧ (π‘₯ ∨ ( βŠ₯ β€˜π‘₯)) = 1 ∧ (π‘₯ ∧ ( βŠ₯ β€˜π‘₯)) = 0 ) ↔ ((( βŠ₯ β€˜π‘‹) ∈ 𝐡 ∧ ( βŠ₯ β€˜( βŠ₯ β€˜π‘‹)) = 𝑋 ∧ (𝑋 ≀ 𝑦 β†’ ( βŠ₯ β€˜π‘¦) ≀ ( βŠ₯ β€˜π‘‹))) ∧ (𝑋 ∨ ( βŠ₯ β€˜π‘‹)) = 1 ∧ (𝑋 ∧ ( βŠ₯ β€˜π‘‹)) = 0 )))
26 breq2 5152 . . . . . . 7 (𝑦 = π‘Œ β†’ (𝑋 ≀ 𝑦 ↔ 𝑋 ≀ π‘Œ))
27 fveq2 6891 . . . . . . . 8 (𝑦 = π‘Œ β†’ ( βŠ₯ β€˜π‘¦) = ( βŠ₯ β€˜π‘Œ))
2827breq1d 5158 . . . . . . 7 (𝑦 = π‘Œ β†’ (( βŠ₯ β€˜π‘¦) ≀ ( βŠ₯ β€˜π‘‹) ↔ ( βŠ₯ β€˜π‘Œ) ≀ ( βŠ₯ β€˜π‘‹)))
2926, 28imbi12d 344 . . . . . 6 (𝑦 = π‘Œ β†’ ((𝑋 ≀ 𝑦 β†’ ( βŠ₯ β€˜π‘¦) ≀ ( βŠ₯ β€˜π‘‹)) ↔ (𝑋 ≀ π‘Œ β†’ ( βŠ₯ β€˜π‘Œ) ≀ ( βŠ₯ β€˜π‘‹))))
30293anbi3d 1442 . . . . 5 (𝑦 = π‘Œ β†’ ((( βŠ₯ β€˜π‘‹) ∈ 𝐡 ∧ ( βŠ₯ β€˜( βŠ₯ β€˜π‘‹)) = 𝑋 ∧ (𝑋 ≀ 𝑦 β†’ ( βŠ₯ β€˜π‘¦) ≀ ( βŠ₯ β€˜π‘‹))) ↔ (( βŠ₯ β€˜π‘‹) ∈ 𝐡 ∧ ( βŠ₯ β€˜( βŠ₯ β€˜π‘‹)) = 𝑋 ∧ (𝑋 ≀ π‘Œ β†’ ( βŠ₯ β€˜π‘Œ) ≀ ( βŠ₯ β€˜π‘‹)))))
31303anbi1d 1440 . . . 4 (𝑦 = π‘Œ β†’ (((( βŠ₯ β€˜π‘‹) ∈ 𝐡 ∧ ( βŠ₯ β€˜( βŠ₯ β€˜π‘‹)) = 𝑋 ∧ (𝑋 ≀ 𝑦 β†’ ( βŠ₯ β€˜π‘¦) ≀ ( βŠ₯ β€˜π‘‹))) ∧ (𝑋 ∨ ( βŠ₯ β€˜π‘‹)) = 1 ∧ (𝑋 ∧ ( βŠ₯ β€˜π‘‹)) = 0 ) ↔ ((( βŠ₯ β€˜π‘‹) ∈ 𝐡 ∧ ( βŠ₯ β€˜( βŠ₯ β€˜π‘‹)) = 𝑋 ∧ (𝑋 ≀ π‘Œ β†’ ( βŠ₯ β€˜π‘Œ) ≀ ( βŠ₯ β€˜π‘‹))) ∧ (𝑋 ∨ ( βŠ₯ β€˜π‘‹)) = 1 ∧ (𝑋 ∧ ( βŠ₯ β€˜π‘‹)) = 0 )))
3225, 31rspc2v 3622 . . 3 ((𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ (βˆ€π‘₯ ∈ 𝐡 βˆ€π‘¦ ∈ 𝐡 ((( βŠ₯ β€˜π‘₯) ∈ 𝐡 ∧ ( βŠ₯ β€˜( βŠ₯ β€˜π‘₯)) = π‘₯ ∧ (π‘₯ ≀ 𝑦 β†’ ( βŠ₯ β€˜π‘¦) ≀ ( βŠ₯ β€˜π‘₯))) ∧ (π‘₯ ∨ ( βŠ₯ β€˜π‘₯)) = 1 ∧ (π‘₯ ∧ ( βŠ₯ β€˜π‘₯)) = 0 ) β†’ ((( βŠ₯ β€˜π‘‹) ∈ 𝐡 ∧ ( βŠ₯ β€˜( βŠ₯ β€˜π‘‹)) = 𝑋 ∧ (𝑋 ≀ π‘Œ β†’ ( βŠ₯ β€˜π‘Œ) ≀ ( βŠ₯ β€˜π‘‹))) ∧ (𝑋 ∨ ( βŠ₯ β€˜π‘‹)) = 1 ∧ (𝑋 ∧ ( βŠ₯ β€˜π‘‹)) = 0 )))
3311, 32mpan9 507 . 2 ((𝐾 ∈ OP ∧ (𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡)) β†’ ((( βŠ₯ β€˜π‘‹) ∈ 𝐡 ∧ ( βŠ₯ β€˜( βŠ₯ β€˜π‘‹)) = 𝑋 ∧ (𝑋 ≀ π‘Œ β†’ ( βŠ₯ β€˜π‘Œ) ≀ ( βŠ₯ β€˜π‘‹))) ∧ (𝑋 ∨ ( βŠ₯ β€˜π‘‹)) = 1 ∧ (𝑋 ∧ ( βŠ₯ β€˜π‘‹)) = 0 ))
34333impb 1115 1 ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐡 ∧ π‘Œ ∈ 𝐡) β†’ ((( βŠ₯ β€˜π‘‹) ∈ 𝐡 ∧ ( βŠ₯ β€˜( βŠ₯ β€˜π‘‹)) = 𝑋 ∧ (𝑋 ≀ π‘Œ β†’ ( βŠ₯ β€˜π‘Œ) ≀ ( βŠ₯ β€˜π‘‹))) ∧ (𝑋 ∨ ( βŠ₯ β€˜π‘‹)) = 1 ∧ (𝑋 ∧ ( βŠ₯ β€˜π‘‹)) = 0 ))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  βˆ€wral 3061   class class class wbr 5148  dom cdm 5676  β€˜cfv 6543  (class class class)co 7411  Basecbs 17146  lecple 17206  occoc 17207  Posetcpo 18262  lubclub 18264  glbcglb 18265  joincjn 18266  meetcmee 18267  0.cp0 18378  1.cp1 18379  OPcops 38128
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-nul 5306
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-dm 5686  df-iota 6495  df-fv 6551  df-ov 7414  df-oposet 38132
This theorem is referenced by:  opoccl  38150  opococ  38151  oplecon3  38155  opexmid  38163  opnoncon  38164
  Copyright terms: Public domain W3C validator