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

Theorem isosolem 7346
Description: Lemma for isoso 7347. (Contributed by Stefan O'Rear, 16-Nov-2014.)
Assertion
Ref Expression
isosolem (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑆 Or 𝐵𝑅 Or 𝐴))

Proof of Theorem isosolem
Dummy variables 𝑎 𝑏 𝑐 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isopolem 7344 . . 3 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑆 Po 𝐵𝑅 Po 𝐴))
2 isof1o 7322 . . . . . . . 8 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴1-1-onto𝐵)
3 f1of 6833 . . . . . . . 8 (𝐻:𝐴1-1-onto𝐵𝐻:𝐴𝐵)
4 ffvelcdm 7083 . . . . . . . . . 10 ((𝐻:𝐴𝐵𝑐𝐴) → (𝐻𝑐) ∈ 𝐵)
54ex 413 . . . . . . . . 9 (𝐻:𝐴𝐵 → (𝑐𝐴 → (𝐻𝑐) ∈ 𝐵))
6 ffvelcdm 7083 . . . . . . . . . 10 ((𝐻:𝐴𝐵𝑑𝐴) → (𝐻𝑑) ∈ 𝐵)
76ex 413 . . . . . . . . 9 (𝐻:𝐴𝐵 → (𝑑𝐴 → (𝐻𝑑) ∈ 𝐵))
85, 7anim12d 609 . . . . . . . 8 (𝐻:𝐴𝐵 → ((𝑐𝐴𝑑𝐴) → ((𝐻𝑐) ∈ 𝐵 ∧ (𝐻𝑑) ∈ 𝐵)))
92, 3, 83syl 18 . . . . . . 7 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → ((𝑐𝐴𝑑𝐴) → ((𝐻𝑐) ∈ 𝐵 ∧ (𝐻𝑑) ∈ 𝐵)))
109imp 407 . . . . . 6 ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝑐𝐴𝑑𝐴)) → ((𝐻𝑐) ∈ 𝐵 ∧ (𝐻𝑑) ∈ 𝐵))
11 breq1 5151 . . . . . . . 8 (𝑎 = (𝐻𝑐) → (𝑎𝑆𝑏 ↔ (𝐻𝑐)𝑆𝑏))
12 eqeq1 2736 . . . . . . . 8 (𝑎 = (𝐻𝑐) → (𝑎 = 𝑏 ↔ (𝐻𝑐) = 𝑏))
13 breq2 5152 . . . . . . . 8 (𝑎 = (𝐻𝑐) → (𝑏𝑆𝑎𝑏𝑆(𝐻𝑐)))
1411, 12, 133orbi123d 1435 . . . . . . 7 (𝑎 = (𝐻𝑐) → ((𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎) ↔ ((𝐻𝑐)𝑆𝑏 ∨ (𝐻𝑐) = 𝑏𝑏𝑆(𝐻𝑐))))
15 breq2 5152 . . . . . . . 8 (𝑏 = (𝐻𝑑) → ((𝐻𝑐)𝑆𝑏 ↔ (𝐻𝑐)𝑆(𝐻𝑑)))
16 eqeq2 2744 . . . . . . . 8 (𝑏 = (𝐻𝑑) → ((𝐻𝑐) = 𝑏 ↔ (𝐻𝑐) = (𝐻𝑑)))
17 breq1 5151 . . . . . . . 8 (𝑏 = (𝐻𝑑) → (𝑏𝑆(𝐻𝑐) ↔ (𝐻𝑑)𝑆(𝐻𝑐)))
1815, 16, 173orbi123d 1435 . . . . . . 7 (𝑏 = (𝐻𝑑) → (((𝐻𝑐)𝑆𝑏 ∨ (𝐻𝑐) = 𝑏𝑏𝑆(𝐻𝑐)) ↔ ((𝐻𝑐)𝑆(𝐻𝑑) ∨ (𝐻𝑐) = (𝐻𝑑) ∨ (𝐻𝑑)𝑆(𝐻𝑐))))
1914, 18rspc2v 3622 . . . . . 6 (((𝐻𝑐) ∈ 𝐵 ∧ (𝐻𝑑) ∈ 𝐵) → (∀𝑎𝐵𝑏𝐵 (𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎) → ((𝐻𝑐)𝑆(𝐻𝑑) ∨ (𝐻𝑐) = (𝐻𝑑) ∨ (𝐻𝑑)𝑆(𝐻𝑐))))
2010, 19syl 17 . . . . 5 ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝑐𝐴𝑑𝐴)) → (∀𝑎𝐵𝑏𝐵 (𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎) → ((𝐻𝑐)𝑆(𝐻𝑑) ∨ (𝐻𝑐) = (𝐻𝑑) ∨ (𝐻𝑑)𝑆(𝐻𝑐))))
21 isorel 7325 . . . . . 6 ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝑐𝐴𝑑𝐴)) → (𝑐𝑅𝑑 ↔ (𝐻𝑐)𝑆(𝐻𝑑)))
22 f1of1 6832 . . . . . . . . 9 (𝐻:𝐴1-1-onto𝐵𝐻:𝐴1-1𝐵)
232, 22syl 17 . . . . . . . 8 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴1-1𝐵)
24 f1fveq 7263 . . . . . . . 8 ((𝐻:𝐴1-1𝐵 ∧ (𝑐𝐴𝑑𝐴)) → ((𝐻𝑐) = (𝐻𝑑) ↔ 𝑐 = 𝑑))
2523, 24sylan 580 . . . . . . 7 ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝑐𝐴𝑑𝐴)) → ((𝐻𝑐) = (𝐻𝑑) ↔ 𝑐 = 𝑑))
2625bicomd 222 . . . . . 6 ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝑐𝐴𝑑𝐴)) → (𝑐 = 𝑑 ↔ (𝐻𝑐) = (𝐻𝑑)))
27 isorel 7325 . . . . . . 7 ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝑑𝐴𝑐𝐴)) → (𝑑𝑅𝑐 ↔ (𝐻𝑑)𝑆(𝐻𝑐)))
2827ancom2s 648 . . . . . 6 ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝑐𝐴𝑑𝐴)) → (𝑑𝑅𝑐 ↔ (𝐻𝑑)𝑆(𝐻𝑐)))
2921, 26, 283orbi123d 1435 . . . . 5 ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝑐𝐴𝑑𝐴)) → ((𝑐𝑅𝑑𝑐 = 𝑑𝑑𝑅𝑐) ↔ ((𝐻𝑐)𝑆(𝐻𝑑) ∨ (𝐻𝑐) = (𝐻𝑑) ∨ (𝐻𝑑)𝑆(𝐻𝑐))))
3020, 29sylibrd 258 . . . 4 ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝑐𝐴𝑑𝐴)) → (∀𝑎𝐵𝑏𝐵 (𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎) → (𝑐𝑅𝑑𝑐 = 𝑑𝑑𝑅𝑐)))
3130ralrimdvva 3209 . . 3 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (∀𝑎𝐵𝑏𝐵 (𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎) → ∀𝑐𝐴𝑑𝐴 (𝑐𝑅𝑑𝑐 = 𝑑𝑑𝑅𝑐)))
321, 31anim12d 609 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → ((𝑆 Po 𝐵 ∧ ∀𝑎𝐵𝑏𝐵 (𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎)) → (𝑅 Po 𝐴 ∧ ∀𝑐𝐴𝑑𝐴 (𝑐𝑅𝑑𝑐 = 𝑑𝑑𝑅𝑐))))
33 df-so 5589 . 2 (𝑆 Or 𝐵 ↔ (𝑆 Po 𝐵 ∧ ∀𝑎𝐵𝑏𝐵 (𝑎𝑆𝑏𝑎 = 𝑏𝑏𝑆𝑎)))
34 df-so 5589 . 2 (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑐𝐴𝑑𝐴 (𝑐𝑅𝑑𝑐 = 𝑑𝑑𝑅𝑐)))
3532, 33, 343imtr4g 295 1 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → (𝑆 Or 𝐵𝑅 Or 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3o 1086   = wceq 1541  wcel 2106  wral 3061   class class class wbr 5148   Po wpo 5586   Or wor 5587  wf 6539  1-1wf1 6540  1-1-ontowf1o 6542  cfv 6543   Isom wiso 6544
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-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  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-opab 5211  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-f1o 6550  df-fv 6551  df-isom 6552
This theorem is referenced by:  isoso  7347  isowe2  7349
  Copyright terms: Public domain W3C validator