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 39183
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 2737 . . . . 5 (lub‘𝐾) = (lub‘𝐾)
3 eqid 2737 . . . . 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 39181 . . . 4 (𝐾 ∈ OP ↔ ((𝐾 ∈ Poset ∧ 𝐵 ∈ dom (lub‘𝐾) ∧ 𝐵 ∈ dom (glb‘𝐾)) ∧ ∀𝑥𝐵𝑦𝐵 ((( 𝑥) ∈ 𝐵 ∧ ( ‘( 𝑥)) = 𝑥 ∧ (𝑥 𝑦 → ( 𝑦) ( 𝑥))) ∧ (𝑥 ( 𝑥)) = 1 ∧ (𝑥 ( 𝑥)) = 0 )))
1110simprbi 496 . . 3 (𝐾 ∈ OP → ∀𝑥𝐵𝑦𝐵 ((( 𝑥) ∈ 𝐵 ∧ ( ‘( 𝑥)) = 𝑥 ∧ (𝑥 𝑦 → ( 𝑦) ( 𝑥))) ∧ (𝑥 ( 𝑥)) = 1 ∧ (𝑥 ( 𝑥)) = 0 ))
12 fveq2 6906 . . . . . . 7 (𝑥 = 𝑋 → ( 𝑥) = ( 𝑋))
1312eleq1d 2826 . . . . . 6 (𝑥 = 𝑋 → (( 𝑥) ∈ 𝐵 ↔ ( 𝑋) ∈ 𝐵))
14 2fveq3 6911 . . . . . . 7 (𝑥 = 𝑋 → ( ‘( 𝑥)) = ( ‘( 𝑋)))
15 id 22 . . . . . . 7 (𝑥 = 𝑋𝑥 = 𝑋)
1614, 15eqeq12d 2753 . . . . . 6 (𝑥 = 𝑋 → (( ‘( 𝑥)) = 𝑥 ↔ ( ‘( 𝑋)) = 𝑋))
17 breq1 5146 . . . . . . 7 (𝑥 = 𝑋 → (𝑥 𝑦𝑋 𝑦))
1812breq2d 5155 . . . . . . 7 (𝑥 = 𝑋 → (( 𝑦) ( 𝑥) ↔ ( 𝑦) ( 𝑋)))
1917, 18imbi12d 344 . . . . . 6 (𝑥 = 𝑋 → ((𝑥 𝑦 → ( 𝑦) ( 𝑥)) ↔ (𝑋 𝑦 → ( 𝑦) ( 𝑋))))
2013, 16, 193anbi123d 1438 . . . . 5 (𝑥 = 𝑋 → ((( 𝑥) ∈ 𝐵 ∧ ( ‘( 𝑥)) = 𝑥 ∧ (𝑥 𝑦 → ( 𝑦) ( 𝑥))) ↔ (( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋 𝑦 → ( 𝑦) ( 𝑋)))))
2115, 12oveq12d 7449 . . . . . 6 (𝑥 = 𝑋 → (𝑥 ( 𝑥)) = (𝑋 ( 𝑋)))
2221eqeq1d 2739 . . . . 5 (𝑥 = 𝑋 → ((𝑥 ( 𝑥)) = 1 ↔ (𝑋 ( 𝑋)) = 1 ))
2315, 12oveq12d 7449 . . . . . 6 (𝑥 = 𝑋 → (𝑥 ( 𝑥)) = (𝑋 ( 𝑋)))
2423eqeq1d 2739 . . . . 5 (𝑥 = 𝑋 → ((𝑥 ( 𝑥)) = 0 ↔ (𝑋 ( 𝑋)) = 0 ))
2520, 22, 243anbi123d 1438 . . . 4 (𝑥 = 𝑋 → (((( 𝑥) ∈ 𝐵 ∧ ( ‘( 𝑥)) = 𝑥 ∧ (𝑥 𝑦 → ( 𝑦) ( 𝑥))) ∧ (𝑥 ( 𝑥)) = 1 ∧ (𝑥 ( 𝑥)) = 0 ) ↔ ((( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋 𝑦 → ( 𝑦) ( 𝑋))) ∧ (𝑋 ( 𝑋)) = 1 ∧ (𝑋 ( 𝑋)) = 0 )))
26 breq2 5147 . . . . . . 7 (𝑦 = 𝑌 → (𝑋 𝑦𝑋 𝑌))
27 fveq2 6906 . . . . . . . 8 (𝑦 = 𝑌 → ( 𝑦) = ( 𝑌))
2827breq1d 5153 . . . . . . 7 (𝑦 = 𝑌 → (( 𝑦) ( 𝑋) ↔ ( 𝑌) ( 𝑋)))
2926, 28imbi12d 344 . . . . . 6 (𝑦 = 𝑌 → ((𝑋 𝑦 → ( 𝑦) ( 𝑋)) ↔ (𝑋 𝑌 → ( 𝑌) ( 𝑋))))
30293anbi3d 1444 . . . . 5 (𝑦 = 𝑌 → ((( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋 𝑦 → ( 𝑦) ( 𝑋))) ↔ (( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋 𝑌 → ( 𝑌) ( 𝑋)))))
31303anbi1d 1442 . . . 4 (𝑦 = 𝑌 → (((( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋 𝑦 → ( 𝑦) ( 𝑋))) ∧ (𝑋 ( 𝑋)) = 1 ∧ (𝑋 ( 𝑋)) = 0 ) ↔ ((( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋 𝑌 → ( 𝑌) ( 𝑋))) ∧ (𝑋 ( 𝑋)) = 1 ∧ (𝑋 ( 𝑋)) = 0 )))
3225, 31rspc2v 3633 . . 3 ((𝑋𝐵𝑌𝐵) → (∀𝑥𝐵𝑦𝐵 ((( 𝑥) ∈ 𝐵 ∧ ( ‘( 𝑥)) = 𝑥 ∧ (𝑥 𝑦 → ( 𝑦) ( 𝑥))) ∧ (𝑥 ( 𝑥)) = 1 ∧ (𝑥 ( 𝑥)) = 0 ) → ((( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋 𝑌 → ( 𝑌) ( 𝑋))) ∧ (𝑋 ( 𝑋)) = 1 ∧ (𝑋 ( 𝑋)) = 0 )))
3311, 32mpan9 506 . 2 ((𝐾 ∈ OP ∧ (𝑋𝐵𝑌𝐵)) → ((( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋 𝑌 → ( 𝑌) ( 𝑋))) ∧ (𝑋 ( 𝑋)) = 1 ∧ (𝑋 ( 𝑋)) = 0 ))
34333impb 1115 1 ((𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵) → ((( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋 𝑌 → ( 𝑌) ( 𝑋))) ∧ (𝑋 ( 𝑋)) = 1 ∧ (𝑋 ( 𝑋)) = 0 ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1087   = wceq 1540  wcel 2108  wral 3061   class class class wbr 5143  dom cdm 5685  cfv 6561  (class class class)co 7431  Basecbs 17247  lecple 17304  occoc 17305  Posetcpo 18353  lubclub 18355  glbcglb 18356  joincjn 18357  meetcmee 18358  0.cp0 18468  1.cp1 18469  OPcops 39173
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-dm 5695  df-iota 6514  df-fv 6569  df-ov 7434  df-oposet 39177
This theorem is referenced by:  opoccl  39195  opococ  39196  oplecon3  39200  opexmid  39208  opnoncon  39209
  Copyright terms: Public domain W3C validator