Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  joinlem Structured version   Visualization version   GIF version

Theorem joinlem 17397
 Description: Lemma for join properties. (Contributed by NM, 16-Sep-2011.) (Revised by NM, 12-Sep-2018.)
Hypotheses
Ref Expression
joinval2.b 𝐵 = (Base‘𝐾)
joinval2.l = (le‘𝐾)
joinval2.j = (join‘𝐾)
joinval2.k (𝜑𝐾𝑉)
joinval2.x (𝜑𝑋𝐵)
joinval2.y (𝜑𝑌𝐵)
joinlem.e (𝜑 → ⟨𝑋, 𝑌⟩ ∈ dom )
Assertion
Ref Expression
joinlem (𝜑 → ((𝑋 (𝑋 𝑌) ∧ 𝑌 (𝑋 𝑌)) ∧ ∀𝑧𝐵 ((𝑋 𝑧𝑌 𝑧) → (𝑋 𝑌) 𝑧)))
Distinct variable groups:   𝑧,𝐵   𝑧,   𝑧,𝐾   𝑧,𝑋   𝑧,𝑌
Allowed substitution hints:   𝜑(𝑧)   (𝑧)   𝑉(𝑧)

Proof of Theorem joinlem
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 joinval2.b . . . . 5 𝐵 = (Base‘𝐾)
2 joinval2.l . . . . 5 = (le‘𝐾)
3 joinval2.j . . . . 5 = (join‘𝐾)
4 joinval2.k . . . . 5 (𝜑𝐾𝑉)
5 joinval2.x . . . . 5 (𝜑𝑋𝐵)
6 joinval2.y . . . . 5 (𝜑𝑌𝐵)
7 joinlem.e . . . . 5 (𝜑 → ⟨𝑋, 𝑌⟩ ∈ dom )
81, 2, 3, 4, 5, 6, 7joineu 17396 . . . 4 (𝜑 → ∃!𝑥𝐵 ((𝑋 𝑥𝑌 𝑥) ∧ ∀𝑧𝐵 ((𝑋 𝑧𝑌 𝑧) → 𝑥 𝑧)))
9 riotasbc 6898 . . . 4 (∃!𝑥𝐵 ((𝑋 𝑥𝑌 𝑥) ∧ ∀𝑧𝐵 ((𝑋 𝑧𝑌 𝑧) → 𝑥 𝑧)) → [(𝑥𝐵 ((𝑋 𝑥𝑌 𝑥) ∧ ∀𝑧𝐵 ((𝑋 𝑧𝑌 𝑧) → 𝑥 𝑧))) / 𝑥]((𝑋 𝑥𝑌 𝑥) ∧ ∀𝑧𝐵 ((𝑋 𝑧𝑌 𝑧) → 𝑥 𝑧)))
108, 9syl 17 . . 3 (𝜑[(𝑥𝐵 ((𝑋 𝑥𝑌 𝑥) ∧ ∀𝑧𝐵 ((𝑋 𝑧𝑌 𝑧) → 𝑥 𝑧))) / 𝑥]((𝑋 𝑥𝑌 𝑥) ∧ ∀𝑧𝐵 ((𝑋 𝑧𝑌 𝑧) → 𝑥 𝑧)))
111, 2, 3, 4, 5, 6joinval2 17395 . . . 4 (𝜑 → (𝑋 𝑌) = (𝑥𝐵 ((𝑋 𝑥𝑌 𝑥) ∧ ∀𝑧𝐵 ((𝑋 𝑧𝑌 𝑧) → 𝑥 𝑧))))
1211sbceq1d 3657 . . 3 (𝜑 → ([(𝑋 𝑌) / 𝑥]((𝑋 𝑥𝑌 𝑥) ∧ ∀𝑧𝐵 ((𝑋 𝑧𝑌 𝑧) → 𝑥 𝑧)) ↔ [(𝑥𝐵 ((𝑋 𝑥𝑌 𝑥) ∧ ∀𝑧𝐵 ((𝑋 𝑧𝑌 𝑧) → 𝑥 𝑧))) / 𝑥]((𝑋 𝑥𝑌 𝑥) ∧ ∀𝑧𝐵 ((𝑋 𝑧𝑌 𝑧) → 𝑥 𝑧))))
1310, 12mpbird 249 . 2 (𝜑[(𝑋 𝑌) / 𝑥]((𝑋 𝑥𝑌 𝑥) ∧ ∀𝑧𝐵 ((𝑋 𝑧𝑌 𝑧) → 𝑥 𝑧)))
14 ovex 6954 . . 3 (𝑋 𝑌) ∈ V
15 breq2 4890 . . . . 5 (𝑥 = (𝑋 𝑌) → (𝑋 𝑥𝑋 (𝑋 𝑌)))
16 breq2 4890 . . . . 5 (𝑥 = (𝑋 𝑌) → (𝑌 𝑥𝑌 (𝑋 𝑌)))
1715, 16anbi12d 624 . . . 4 (𝑥 = (𝑋 𝑌) → ((𝑋 𝑥𝑌 𝑥) ↔ (𝑋 (𝑋 𝑌) ∧ 𝑌 (𝑋 𝑌))))
18 breq1 4889 . . . . . 6 (𝑥 = (𝑋 𝑌) → (𝑥 𝑧 ↔ (𝑋 𝑌) 𝑧))
1918imbi2d 332 . . . . 5 (𝑥 = (𝑋 𝑌) → (((𝑋 𝑧𝑌 𝑧) → 𝑥 𝑧) ↔ ((𝑋 𝑧𝑌 𝑧) → (𝑋 𝑌) 𝑧)))
2019ralbidv 3168 . . . 4 (𝑥 = (𝑋 𝑌) → (∀𝑧𝐵 ((𝑋 𝑧𝑌 𝑧) → 𝑥 𝑧) ↔ ∀𝑧𝐵 ((𝑋 𝑧𝑌 𝑧) → (𝑋 𝑌) 𝑧)))
2117, 20anbi12d 624 . . 3 (𝑥 = (𝑋 𝑌) → (((𝑋 𝑥𝑌 𝑥) ∧ ∀𝑧𝐵 ((𝑋 𝑧𝑌 𝑧) → 𝑥 𝑧)) ↔ ((𝑋 (𝑋 𝑌) ∧ 𝑌 (𝑋 𝑌)) ∧ ∀𝑧𝐵 ((𝑋 𝑧𝑌 𝑧) → (𝑋 𝑌) 𝑧))))
2214, 21sbcie 3687 . 2 ([(𝑋 𝑌) / 𝑥]((𝑋 𝑥𝑌 𝑥) ∧ ∀𝑧𝐵 ((𝑋 𝑧𝑌 𝑧) → 𝑥 𝑧)) ↔ ((𝑋 (𝑋 𝑌) ∧ 𝑌 (𝑋 𝑌)) ∧ ∀𝑧𝐵 ((𝑋 𝑧𝑌 𝑧) → (𝑋 𝑌) 𝑧)))
2313, 22sylib 210 1 (𝜑 → ((𝑋 (𝑋 𝑌) ∧ 𝑌 (𝑋 𝑌)) ∧ ∀𝑧𝐵 ((𝑋 𝑧𝑌 𝑧) → (𝑋 𝑌) 𝑧)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 386   = wceq 1601   ∈ wcel 2107  ∀wral 3090  ∃!wreu 3092  [wsbc 3652  ⟨cop 4404   class class class wbr 4886  dom cdm 5355  ‘cfv 6135  ℩crio 6882  (class class class)co 6922  Basecbs 16255  lecple 16345  joincjn 17330 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-riota 6883  df-ov 6925  df-oprab 6926  df-lub 17360  df-join 17362 This theorem is referenced by:  lejoin1  17398  lejoin2  17399  joinle  17400
 Copyright terms: Public domain W3C validator