ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  isopolem Structured version   GIF version

Theorem isopolem 5404
Description: Lemma for isopo 5405. (Contributed by Stefan O'Rear, 16-Nov-2014.)
Assertion
Ref Expression
isopolem (𝐻 Isom 𝑅, 𝑆 (A, B) → (𝑆 Po B𝑅 Po A))

Proof of Theorem isopolem
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 f are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isof1o 5390 . . . . . . . . . . 11 (𝐻 Isom 𝑅, 𝑆 (A, B) → 𝐻:A1-1-ontoB)
2 f1of 5069 . . . . . . . . . . 11 (𝐻:A1-1-ontoB𝐻:AB)
3 ffvelrn 5243 . . . . . . . . . . . . 13 ((𝐻:AB 𝑑 A) → (𝐻𝑑) B)
43ex 108 . . . . . . . . . . . 12 (𝐻:AB → (𝑑 A → (𝐻𝑑) B))
5 ffvelrn 5243 . . . . . . . . . . . . 13 ((𝐻:AB 𝑒 A) → (𝐻𝑒) B)
65ex 108 . . . . . . . . . . . 12 (𝐻:AB → (𝑒 A → (𝐻𝑒) B))
7 ffvelrn 5243 . . . . . . . . . . . . 13 ((𝐻:AB f A) → (𝐻f) B)
87ex 108 . . . . . . . . . . . 12 (𝐻:AB → (f A → (𝐻f) B))
94, 6, 83anim123d 1213 . . . . . . . . . . 11 (𝐻:AB → ((𝑑 A 𝑒 A f A) → ((𝐻𝑑) B (𝐻𝑒) B (𝐻f) B)))
101, 2, 93syl 17 . . . . . . . . . 10 (𝐻 Isom 𝑅, 𝑆 (A, B) → ((𝑑 A 𝑒 A f A) → ((𝐻𝑑) B (𝐻𝑒) B (𝐻f) B)))
1110imp 115 . . . . . . . . 9 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A 𝑒 A f A)) → ((𝐻𝑑) B (𝐻𝑒) B (𝐻f) B))
12 breq12 3760 . . . . . . . . . . . . 13 ((𝑎 = (𝐻𝑑) 𝑎 = (𝐻𝑑)) → (𝑎𝑆𝑎 ↔ (𝐻𝑑)𝑆(𝐻𝑑)))
1312anidms 377 . . . . . . . . . . . 12 (𝑎 = (𝐻𝑑) → (𝑎𝑆𝑎 ↔ (𝐻𝑑)𝑆(𝐻𝑑)))
1413notbid 591 . . . . . . . . . . 11 (𝑎 = (𝐻𝑑) → (¬ 𝑎𝑆𝑎 ↔ ¬ (𝐻𝑑)𝑆(𝐻𝑑)))
15 breq1 3758 . . . . . . . . . . . . 13 (𝑎 = (𝐻𝑑) → (𝑎𝑆𝑏 ↔ (𝐻𝑑)𝑆𝑏))
1615anbi1d 438 . . . . . . . . . . . 12 (𝑎 = (𝐻𝑑) → ((𝑎𝑆𝑏 𝑏𝑆𝑐) ↔ ((𝐻𝑑)𝑆𝑏 𝑏𝑆𝑐)))
17 breq1 3758 . . . . . . . . . . . 12 (𝑎 = (𝐻𝑑) → (𝑎𝑆𝑐 ↔ (𝐻𝑑)𝑆𝑐))
1816, 17imbi12d 223 . . . . . . . . . . 11 (𝑎 = (𝐻𝑑) → (((𝑎𝑆𝑏 𝑏𝑆𝑐) → 𝑎𝑆𝑐) ↔ (((𝐻𝑑)𝑆𝑏 𝑏𝑆𝑐) → (𝐻𝑑)𝑆𝑐)))
1914, 18anbi12d 442 . . . . . . . . . 10 (𝑎 = (𝐻𝑑) → ((¬ 𝑎𝑆𝑎 ((𝑎𝑆𝑏 𝑏𝑆𝑐) → 𝑎𝑆𝑐)) ↔ (¬ (𝐻𝑑)𝑆(𝐻𝑑) (((𝐻𝑑)𝑆𝑏 𝑏𝑆𝑐) → (𝐻𝑑)𝑆𝑐))))
20 breq2 3759 . . . . . . . . . . . . 13 (𝑏 = (𝐻𝑒) → ((𝐻𝑑)𝑆𝑏 ↔ (𝐻𝑑)𝑆(𝐻𝑒)))
21 breq1 3758 . . . . . . . . . . . . 13 (𝑏 = (𝐻𝑒) → (𝑏𝑆𝑐 ↔ (𝐻𝑒)𝑆𝑐))
2220, 21anbi12d 442 . . . . . . . . . . . 12 (𝑏 = (𝐻𝑒) → (((𝐻𝑑)𝑆𝑏 𝑏𝑆𝑐) ↔ ((𝐻𝑑)𝑆(𝐻𝑒) (𝐻𝑒)𝑆𝑐)))
2322imbi1d 220 . . . . . . . . . . 11 (𝑏 = (𝐻𝑒) → ((((𝐻𝑑)𝑆𝑏 𝑏𝑆𝑐) → (𝐻𝑑)𝑆𝑐) ↔ (((𝐻𝑑)𝑆(𝐻𝑒) (𝐻𝑒)𝑆𝑐) → (𝐻𝑑)𝑆𝑐)))
2423anbi2d 437 . . . . . . . . . 10 (𝑏 = (𝐻𝑒) → ((¬ (𝐻𝑑)𝑆(𝐻𝑑) (((𝐻𝑑)𝑆𝑏 𝑏𝑆𝑐) → (𝐻𝑑)𝑆𝑐)) ↔ (¬ (𝐻𝑑)𝑆(𝐻𝑑) (((𝐻𝑑)𝑆(𝐻𝑒) (𝐻𝑒)𝑆𝑐) → (𝐻𝑑)𝑆𝑐))))
25 breq2 3759 . . . . . . . . . . . . 13 (𝑐 = (𝐻f) → ((𝐻𝑒)𝑆𝑐 ↔ (𝐻𝑒)𝑆(𝐻f)))
2625anbi2d 437 . . . . . . . . . . . 12 (𝑐 = (𝐻f) → (((𝐻𝑑)𝑆(𝐻𝑒) (𝐻𝑒)𝑆𝑐) ↔ ((𝐻𝑑)𝑆(𝐻𝑒) (𝐻𝑒)𝑆(𝐻f))))
27 breq2 3759 . . . . . . . . . . . 12 (𝑐 = (𝐻f) → ((𝐻𝑑)𝑆𝑐 ↔ (𝐻𝑑)𝑆(𝐻f)))
2826, 27imbi12d 223 . . . . . . . . . . 11 (𝑐 = (𝐻f) → ((((𝐻𝑑)𝑆(𝐻𝑒) (𝐻𝑒)𝑆𝑐) → (𝐻𝑑)𝑆𝑐) ↔ (((𝐻𝑑)𝑆(𝐻𝑒) (𝐻𝑒)𝑆(𝐻f)) → (𝐻𝑑)𝑆(𝐻f))))
2928anbi2d 437 . . . . . . . . . 10 (𝑐 = (𝐻f) → ((¬ (𝐻𝑑)𝑆(𝐻𝑑) (((𝐻𝑑)𝑆(𝐻𝑒) (𝐻𝑒)𝑆𝑐) → (𝐻𝑑)𝑆𝑐)) ↔ (¬ (𝐻𝑑)𝑆(𝐻𝑑) (((𝐻𝑑)𝑆(𝐻𝑒) (𝐻𝑒)𝑆(𝐻f)) → (𝐻𝑑)𝑆(𝐻f)))))
3019, 24, 29rspc3v 2659 . . . . . . . . 9 (((𝐻𝑑) B (𝐻𝑒) B (𝐻f) B) → (𝑎 B 𝑏 B 𝑐 B𝑎𝑆𝑎 ((𝑎𝑆𝑏 𝑏𝑆𝑐) → 𝑎𝑆𝑐)) → (¬ (𝐻𝑑)𝑆(𝐻𝑑) (((𝐻𝑑)𝑆(𝐻𝑒) (𝐻𝑒)𝑆(𝐻f)) → (𝐻𝑑)𝑆(𝐻f)))))
3111, 30syl 14 . . . . . . . 8 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A 𝑒 A f A)) → (𝑎 B 𝑏 B 𝑐 B𝑎𝑆𝑎 ((𝑎𝑆𝑏 𝑏𝑆𝑐) → 𝑎𝑆𝑐)) → (¬ (𝐻𝑑)𝑆(𝐻𝑑) (((𝐻𝑑)𝑆(𝐻𝑒) (𝐻𝑒)𝑆(𝐻f)) → (𝐻𝑑)𝑆(𝐻f)))))
32 simpl 102 . . . . . . . . . . 11 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A 𝑒 A f A)) → 𝐻 Isom 𝑅, 𝑆 (A, B))
33 simpr1 909 . . . . . . . . . . 11 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A 𝑒 A f A)) → 𝑑 A)
34 isorel 5391 . . . . . . . . . . 11 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A 𝑑 A)) → (𝑑𝑅𝑑 ↔ (𝐻𝑑)𝑆(𝐻𝑑)))
3532, 33, 33, 34syl12anc 1132 . . . . . . . . . 10 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A 𝑒 A f A)) → (𝑑𝑅𝑑 ↔ (𝐻𝑑)𝑆(𝐻𝑑)))
3635notbid 591 . . . . . . . . 9 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A 𝑒 A f A)) → (¬ 𝑑𝑅𝑑 ↔ ¬ (𝐻𝑑)𝑆(𝐻𝑑)))
37 simpr2 910 . . . . . . . . . . . 12 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A 𝑒 A f A)) → 𝑒 A)
38 isorel 5391 . . . . . . . . . . . 12 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A 𝑒 A)) → (𝑑𝑅𝑒 ↔ (𝐻𝑑)𝑆(𝐻𝑒)))
3932, 33, 37, 38syl12anc 1132 . . . . . . . . . . 11 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A 𝑒 A f A)) → (𝑑𝑅𝑒 ↔ (𝐻𝑑)𝑆(𝐻𝑒)))
40 simpr3 911 . . . . . . . . . . . 12 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A 𝑒 A f A)) → f A)
41 isorel 5391 . . . . . . . . . . . 12 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑒 A f A)) → (𝑒𝑅f ↔ (𝐻𝑒)𝑆(𝐻f)))
4232, 37, 40, 41syl12anc 1132 . . . . . . . . . . 11 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A 𝑒 A f A)) → (𝑒𝑅f ↔ (𝐻𝑒)𝑆(𝐻f)))
4339, 42anbi12d 442 . . . . . . . . . 10 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A 𝑒 A f A)) → ((𝑑𝑅𝑒 𝑒𝑅f) ↔ ((𝐻𝑑)𝑆(𝐻𝑒) (𝐻𝑒)𝑆(𝐻f))))
44 isorel 5391 . . . . . . . . . . 11 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A f A)) → (𝑑𝑅f ↔ (𝐻𝑑)𝑆(𝐻f)))
4532, 33, 40, 44syl12anc 1132 . . . . . . . . . 10 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A 𝑒 A f A)) → (𝑑𝑅f ↔ (𝐻𝑑)𝑆(𝐻f)))
4643, 45imbi12d 223 . . . . . . . . 9 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A 𝑒 A f A)) → (((𝑑𝑅𝑒 𝑒𝑅f) → 𝑑𝑅f) ↔ (((𝐻𝑑)𝑆(𝐻𝑒) (𝐻𝑒)𝑆(𝐻f)) → (𝐻𝑑)𝑆(𝐻f))))
4736, 46anbi12d 442 . . . . . . . 8 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A 𝑒 A f A)) → ((¬ 𝑑𝑅𝑑 ((𝑑𝑅𝑒 𝑒𝑅f) → 𝑑𝑅f)) ↔ (¬ (𝐻𝑑)𝑆(𝐻𝑑) (((𝐻𝑑)𝑆(𝐻𝑒) (𝐻𝑒)𝑆(𝐻f)) → (𝐻𝑑)𝑆(𝐻f)))))
4831, 47sylibrd 158 . . . . . . 7 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A 𝑒 A f A)) → (𝑎 B 𝑏 B 𝑐 B𝑎𝑆𝑎 ((𝑎𝑆𝑏 𝑏𝑆𝑐) → 𝑎𝑆𝑐)) → (¬ 𝑑𝑅𝑑 ((𝑑𝑅𝑒 𝑒𝑅f) → 𝑑𝑅f))))
4948ex 108 . . . . . 6 (𝐻 Isom 𝑅, 𝑆 (A, B) → ((𝑑 A 𝑒 A f A) → (𝑎 B 𝑏 B 𝑐 B𝑎𝑆𝑎 ((𝑎𝑆𝑏 𝑏𝑆𝑐) → 𝑎𝑆𝑐)) → (¬ 𝑑𝑅𝑑 ((𝑑𝑅𝑒 𝑒𝑅f) → 𝑑𝑅f)))))
5049com23 72 . . . . 5 (𝐻 Isom 𝑅, 𝑆 (A, B) → (𝑎 B 𝑏 B 𝑐 B𝑎𝑆𝑎 ((𝑎𝑆𝑏 𝑏𝑆𝑐) → 𝑎𝑆𝑐)) → ((𝑑 A 𝑒 A f A) → (¬ 𝑑𝑅𝑑 ((𝑑𝑅𝑒 𝑒𝑅f) → 𝑑𝑅f)))))
5150imp31 243 . . . 4 (((𝐻 Isom 𝑅, 𝑆 (A, B) 𝑎 B 𝑏 B 𝑐 B𝑎𝑆𝑎 ((𝑎𝑆𝑏 𝑏𝑆𝑐) → 𝑎𝑆𝑐))) (𝑑 A 𝑒 A f A)) → (¬ 𝑑𝑅𝑑 ((𝑑𝑅𝑒 𝑒𝑅f) → 𝑑𝑅f)))
5251ralrimivvva 2396 . . 3 ((𝐻 Isom 𝑅, 𝑆 (A, B) 𝑎 B 𝑏 B 𝑐 B𝑎𝑆𝑎 ((𝑎𝑆𝑏 𝑏𝑆𝑐) → 𝑎𝑆𝑐))) → 𝑑 A 𝑒 A f A𝑑𝑅𝑑 ((𝑑𝑅𝑒 𝑒𝑅f) → 𝑑𝑅f)))
5352ex 108 . 2 (𝐻 Isom 𝑅, 𝑆 (A, B) → (𝑎 B 𝑏 B 𝑐 B𝑎𝑆𝑎 ((𝑎𝑆𝑏 𝑏𝑆𝑐) → 𝑎𝑆𝑐)) → 𝑑 A 𝑒 A f A𝑑𝑅𝑑 ((𝑑𝑅𝑒 𝑒𝑅f) → 𝑑𝑅f))))
54 df-po 4024 . 2 (𝑆 Po B𝑎 B 𝑏 B 𝑐 B𝑎𝑆𝑎 ((𝑎𝑆𝑏 𝑏𝑆𝑐) → 𝑎𝑆𝑐)))
55 df-po 4024 . 2 (𝑅 Po A𝑑 A 𝑒 A f A𝑑𝑅𝑑 ((𝑑𝑅𝑒 𝑒𝑅f) → 𝑑𝑅f)))
5653, 54, 553imtr4g 194 1 (𝐻 Isom 𝑅, 𝑆 (A, B) → (𝑆 Po B𝑅 Po A))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4   wa 97  wb 98   w3a 884   = wceq 1242   wcel 1390  wral 2300   class class class wbr 3755   Po wpo 4022  wf 4841  1-1-ontowf1o 4844  cfv 4845   Isom wiso 4846
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-sbc 2759  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-id 4021  df-po 4024  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-f1o 4852  df-fv 4853  df-isom 4854
This theorem is referenced by:  isopo  5405  isosolem  5406
  Copyright terms: Public domain W3C validator