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 37500
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 37498 . . . 4 (𝐾 ∈ OP ↔ ((𝐾 ∈ Poset ∧ 𝐵 ∈ dom (lub‘𝐾) ∧ 𝐵 ∈ dom (glb‘𝐾)) ∧ ∀𝑥𝐵𝑦𝐵 ((( 𝑥) ∈ 𝐵 ∧ ( ‘( 𝑥)) = 𝑥 ∧ (𝑥 𝑦 → ( 𝑦) ( 𝑥))) ∧ (𝑥 ( 𝑥)) = 1 ∧ (𝑥 ( 𝑥)) = 0 )))
1110simprbi 498 . . 3 (𝐾 ∈ OP → ∀𝑥𝐵𝑦𝐵 ((( 𝑥) ∈ 𝐵 ∧ ( ‘( 𝑥)) = 𝑥 ∧ (𝑥 𝑦 → ( 𝑦) ( 𝑥))) ∧ (𝑥 ( 𝑥)) = 1 ∧ (𝑥 ( 𝑥)) = 0 ))
12 fveq2 6829 . . . . . . 7 (𝑥 = 𝑋 → ( 𝑥) = ( 𝑋))
1312eleq1d 2822 . . . . . 6 (𝑥 = 𝑋 → (( 𝑥) ∈ 𝐵 ↔ ( 𝑋) ∈ 𝐵))
14 2fveq3 6834 . . . . . . 7 (𝑥 = 𝑋 → ( ‘( 𝑥)) = ( ‘( 𝑋)))
15 id 22 . . . . . . 7 (𝑥 = 𝑋𝑥 = 𝑋)
1614, 15eqeq12d 2753 . . . . . 6 (𝑥 = 𝑋 → (( ‘( 𝑥)) = 𝑥 ↔ ( ‘( 𝑋)) = 𝑋))
17 breq1 5099 . . . . . . 7 (𝑥 = 𝑋 → (𝑥 𝑦𝑋 𝑦))
1812breq2d 5108 . . . . . . 7 (𝑥 = 𝑋 → (( 𝑦) ( 𝑥) ↔ ( 𝑦) ( 𝑋)))
1917, 18imbi12d 345 . . . . . 6 (𝑥 = 𝑋 → ((𝑥 𝑦 → ( 𝑦) ( 𝑥)) ↔ (𝑋 𝑦 → ( 𝑦) ( 𝑋))))
2013, 16, 193anbi123d 1436 . . . . 5 (𝑥 = 𝑋 → ((( 𝑥) ∈ 𝐵 ∧ ( ‘( 𝑥)) = 𝑥 ∧ (𝑥 𝑦 → ( 𝑦) ( 𝑥))) ↔ (( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋 𝑦 → ( 𝑦) ( 𝑋)))))
2115, 12oveq12d 7359 . . . . . 6 (𝑥 = 𝑋 → (𝑥 ( 𝑥)) = (𝑋 ( 𝑋)))
2221eqeq1d 2739 . . . . 5 (𝑥 = 𝑋 → ((𝑥 ( 𝑥)) = 1 ↔ (𝑋 ( 𝑋)) = 1 ))
2315, 12oveq12d 7359 . . . . . 6 (𝑥 = 𝑋 → (𝑥 ( 𝑥)) = (𝑋 ( 𝑋)))
2423eqeq1d 2739 . . . . 5 (𝑥 = 𝑋 → ((𝑥 ( 𝑥)) = 0 ↔ (𝑋 ( 𝑋)) = 0 ))
2520, 22, 243anbi123d 1436 . . . 4 (𝑥 = 𝑋 → (((( 𝑥) ∈ 𝐵 ∧ ( ‘( 𝑥)) = 𝑥 ∧ (𝑥 𝑦 → ( 𝑦) ( 𝑥))) ∧ (𝑥 ( 𝑥)) = 1 ∧ (𝑥 ( 𝑥)) = 0 ) ↔ ((( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋 𝑦 → ( 𝑦) ( 𝑋))) ∧ (𝑋 ( 𝑋)) = 1 ∧ (𝑋 ( 𝑋)) = 0 )))
26 breq2 5100 . . . . . . 7 (𝑦 = 𝑌 → (𝑋 𝑦𝑋 𝑌))
27 fveq2 6829 . . . . . . . 8 (𝑦 = 𝑌 → ( 𝑦) = ( 𝑌))
2827breq1d 5106 . . . . . . 7 (𝑦 = 𝑌 → (( 𝑦) ( 𝑋) ↔ ( 𝑌) ( 𝑋)))
2926, 28imbi12d 345 . . . . . 6 (𝑦 = 𝑌 → ((𝑋 𝑦 → ( 𝑦) ( 𝑋)) ↔ (𝑋 𝑌 → ( 𝑌) ( 𝑋))))
30293anbi3d 1442 . . . . 5 (𝑦 = 𝑌 → ((( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋 𝑦 → ( 𝑦) ( 𝑋))) ↔ (( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋 𝑌 → ( 𝑌) ( 𝑋)))))
31303anbi1d 1440 . . . 4 (𝑦 = 𝑌 → (((( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋 𝑦 → ( 𝑦) ( 𝑋))) ∧ (𝑋 ( 𝑋)) = 1 ∧ (𝑋 ( 𝑋)) = 0 ) ↔ ((( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋 𝑌 → ( 𝑌) ( 𝑋))) ∧ (𝑋 ( 𝑋)) = 1 ∧ (𝑋 ( 𝑋)) = 0 )))
3225, 31rspc2v 3582 . . 3 ((𝑋𝐵𝑌𝐵) → (∀𝑥𝐵𝑦𝐵 ((( 𝑥) ∈ 𝐵 ∧ ( ‘( 𝑥)) = 𝑥 ∧ (𝑥 𝑦 → ( 𝑦) ( 𝑥))) ∧ (𝑥 ( 𝑥)) = 1 ∧ (𝑥 ( 𝑥)) = 0 ) → ((( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋 𝑌 → ( 𝑌) ( 𝑋))) ∧ (𝑋 ( 𝑋)) = 1 ∧ (𝑋 ( 𝑋)) = 0 )))
3311, 32mpan9 508 . 2 ((𝐾 ∈ OP ∧ (𝑋𝐵𝑌𝐵)) → ((( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋 𝑌 → ( 𝑌) ( 𝑋))) ∧ (𝑋 ( 𝑋)) = 1 ∧ (𝑋 ( 𝑋)) = 0 ))
34333impb 1115 1 ((𝐾 ∈ OP ∧ 𝑋𝐵𝑌𝐵) → ((( 𝑋) ∈ 𝐵 ∧ ( ‘( 𝑋)) = 𝑋 ∧ (𝑋 𝑌 → ( 𝑌) ( 𝑋))) ∧ (𝑋 ( 𝑋)) = 1 ∧ (𝑋 ( 𝑋)) = 0 ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1087   = wceq 1541  wcel 2106  wral 3062   class class class wbr 5096  dom cdm 5624  cfv 6483  (class class class)co 7341  Basecbs 17009  lecple 17066  occoc 17067  Posetcpo 18122  lubclub 18124  glbcglb 18125  joincjn 18126  meetcmee 18127  0.cp0 18238  1.cp1 18239  OPcops 37490
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 2708  ax-nul 5254
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2942  df-ral 3063  df-rab 3405  df-v 3444  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4274  df-if 4478  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4857  df-br 5097  df-dm 5634  df-iota 6435  df-fv 6491  df-ov 7344  df-oposet 37494
This theorem is referenced by:  opoccl  37512  opococ  37513  oplecon3  37517  opexmid  37525  opnoncon  37526
  Copyright terms: Public domain W3C validator