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

Theorem isopolem 5382
 Description: Lemma for isopo 5383. (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 5368 . . . . . . . . . . 11 (𝐻 Isom 𝑅, 𝑆 (A, B) → 𝐻:A1-1-ontoB)
2 f1of 5047 . . . . . . . . . . 11 (𝐻:A1-1-ontoB𝐻:AB)
3 ffvelrn 5221 . . . . . . . . . . . . 13 ((𝐻:AB 𝑑 A) → (𝐻𝑑) B)
43ex 108 . . . . . . . . . . . 12 (𝐻:AB → (𝑑 A → (𝐻𝑑) B))
5 ffvelrn 5221 . . . . . . . . . . . . 13 ((𝐻:AB 𝑒 A) → (𝐻𝑒) B)
65ex 108 . . . . . . . . . . . 12 (𝐻:AB → (𝑒 A → (𝐻𝑒) B))
7 ffvelrn 5221 . . . . . . . . . . . . 13 ((𝐻:AB f A) → (𝐻f) B)
87ex 108 . . . . . . . . . . . 12 (𝐻:AB → (f A → (𝐻f) B))
94, 6, 83anim123d 1197 . . . . . . . . . . 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 3739 . . . . . . . . . . . . 13 ((𝑎 = (𝐻𝑑) 𝑎 = (𝐻𝑑)) → (𝑎𝑆𝑎 ↔ (𝐻𝑑)𝑆(𝐻𝑑)))
1312anidms 379 . . . . . . . . . . . 12 (𝑎 = (𝐻𝑑) → (𝑎𝑆𝑎 ↔ (𝐻𝑑)𝑆(𝐻𝑑)))
1413notbid 579 . . . . . . . . . . 11 (𝑎 = (𝐻𝑑) → (¬ 𝑎𝑆𝑎 ↔ ¬ (𝐻𝑑)𝑆(𝐻𝑑)))
15 breq1 3737 . . . . . . . . . . . . 13 (𝑎 = (𝐻𝑑) → (𝑎𝑆𝑏 ↔ (𝐻𝑑)𝑆𝑏))
1615anbi1d 441 . . . . . . . . . . . 12 (𝑎 = (𝐻𝑑) → ((𝑎𝑆𝑏 𝑏𝑆𝑐) ↔ ((𝐻𝑑)𝑆𝑏 𝑏𝑆𝑐)))
17 breq1 3737 . . . . . . . . . . . 12 (𝑎 = (𝐻𝑑) → (𝑎𝑆𝑐 ↔ (𝐻𝑑)𝑆𝑐))
1816, 17imbi12d 223 . . . . . . . . . . 11 (𝑎 = (𝐻𝑑) → (((𝑎𝑆𝑏 𝑏𝑆𝑐) → 𝑎𝑆𝑐) ↔ (((𝐻𝑑)𝑆𝑏 𝑏𝑆𝑐) → (𝐻𝑑)𝑆𝑐)))
1914, 18anbi12d 445 . . . . . . . . . 10 (𝑎 = (𝐻𝑑) → ((¬ 𝑎𝑆𝑎 ((𝑎𝑆𝑏 𝑏𝑆𝑐) → 𝑎𝑆𝑐)) ↔ (¬ (𝐻𝑑)𝑆(𝐻𝑑) (((𝐻𝑑)𝑆𝑏 𝑏𝑆𝑐) → (𝐻𝑑)𝑆𝑐))))
20 breq2 3738 . . . . . . . . . . . . 13 (𝑏 = (𝐻𝑒) → ((𝐻𝑑)𝑆𝑏 ↔ (𝐻𝑑)𝑆(𝐻𝑒)))
21 breq1 3737 . . . . . . . . . . . . 13 (𝑏 = (𝐻𝑒) → (𝑏𝑆𝑐 ↔ (𝐻𝑒)𝑆𝑐))
2220, 21anbi12d 445 . . . . . . . . . . . 12 (𝑏 = (𝐻𝑒) → (((𝐻𝑑)𝑆𝑏 𝑏𝑆𝑐) ↔ ((𝐻𝑑)𝑆(𝐻𝑒) (𝐻𝑒)𝑆𝑐)))
2322imbi1d 220 . . . . . . . . . . 11 (𝑏 = (𝐻𝑒) → ((((𝐻𝑑)𝑆𝑏 𝑏𝑆𝑐) → (𝐻𝑑)𝑆𝑐) ↔ (((𝐻𝑑)𝑆(𝐻𝑒) (𝐻𝑒)𝑆𝑐) → (𝐻𝑑)𝑆𝑐)))
2423anbi2d 440 . . . . . . . . . 10 (𝑏 = (𝐻𝑒) → ((¬ (𝐻𝑑)𝑆(𝐻𝑑) (((𝐻𝑑)𝑆𝑏 𝑏𝑆𝑐) → (𝐻𝑑)𝑆𝑐)) ↔ (¬ (𝐻𝑑)𝑆(𝐻𝑑) (((𝐻𝑑)𝑆(𝐻𝑒) (𝐻𝑒)𝑆𝑐) → (𝐻𝑑)𝑆𝑐))))
25 breq2 3738 . . . . . . . . . . . . 13 (𝑐 = (𝐻f) → ((𝐻𝑒)𝑆𝑐 ↔ (𝐻𝑒)𝑆(𝐻f)))
2625anbi2d 440 . . . . . . . . . . . 12 (𝑐 = (𝐻f) → (((𝐻𝑑)𝑆(𝐻𝑒) (𝐻𝑒)𝑆𝑐) ↔ ((𝐻𝑑)𝑆(𝐻𝑒) (𝐻𝑒)𝑆(𝐻f))))
27 breq2 3738 . . . . . . . . . . . 12 (𝑐 = (𝐻f) → ((𝐻𝑑)𝑆𝑐 ↔ (𝐻𝑑)𝑆(𝐻f)))
2826, 27imbi12d 223 . . . . . . . . . . 11 (𝑐 = (𝐻f) → ((((𝐻𝑑)𝑆(𝐻𝑒) (𝐻𝑒)𝑆𝑐) → (𝐻𝑑)𝑆𝑐) ↔ (((𝐻𝑑)𝑆(𝐻𝑒) (𝐻𝑒)𝑆(𝐻f)) → (𝐻𝑑)𝑆(𝐻f))))
2928anbi2d 440 . . . . . . . . . 10 (𝑐 = (𝐻f) → ((¬ (𝐻𝑑)𝑆(𝐻𝑑) (((𝐻𝑑)𝑆(𝐻𝑒) (𝐻𝑒)𝑆𝑐) → (𝐻𝑑)𝑆𝑐)) ↔ (¬ (𝐻𝑑)𝑆(𝐻𝑑) (((𝐻𝑑)𝑆(𝐻𝑒) (𝐻𝑒)𝑆(𝐻f)) → (𝐻𝑑)𝑆(𝐻f)))))
3019, 24, 29rspc3v 2638 . . . . . . . . 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 896 . . . . . . . . . . 11 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A 𝑒 A f A)) → 𝑑 A)
34 isorel 5369 . . . . . . . . . . 11 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A 𝑑 A)) → (𝑑𝑅𝑑 ↔ (𝐻𝑑)𝑆(𝐻𝑑)))
3532, 33, 33, 34syl12anc 1117 . . . . . . . . . 10 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A 𝑒 A f A)) → (𝑑𝑅𝑑 ↔ (𝐻𝑑)𝑆(𝐻𝑑)))
3635notbid 579 . . . . . . . . 9 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A 𝑒 A f A)) → (¬ 𝑑𝑅𝑑 ↔ ¬ (𝐻𝑑)𝑆(𝐻𝑑)))
37 simpr2 897 . . . . . . . . . . . 12 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A 𝑒 A f A)) → 𝑒 A)
38 isorel 5369 . . . . . . . . . . . 12 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A 𝑒 A)) → (𝑑𝑅𝑒 ↔ (𝐻𝑑)𝑆(𝐻𝑒)))
3932, 33, 37, 38syl12anc 1117 . . . . . . . . . . 11 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A 𝑒 A f A)) → (𝑑𝑅𝑒 ↔ (𝐻𝑑)𝑆(𝐻𝑒)))
40 simpr3 898 . . . . . . . . . . . 12 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A 𝑒 A f A)) → f A)
41 isorel 5369 . . . . . . . . . . . 12 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑒 A f A)) → (𝑒𝑅f ↔ (𝐻𝑒)𝑆(𝐻f)))
4232, 37, 40, 41syl12anc 1117 . . . . . . . . . . 11 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A 𝑒 A f A)) → (𝑒𝑅f ↔ (𝐻𝑒)𝑆(𝐻f)))
4339, 42anbi12d 445 . . . . . . . . . 10 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A 𝑒 A f A)) → ((𝑑𝑅𝑒 𝑒𝑅f) ↔ ((𝐻𝑑)𝑆(𝐻𝑒) (𝐻𝑒)𝑆(𝐻f))))
44 isorel 5369 . . . . . . . . . . 11 ((𝐻 Isom 𝑅, 𝑆 (A, B) (𝑑 A f A)) → (𝑑𝑅f ↔ (𝐻𝑑)𝑆(𝐻f)))
4532, 33, 40, 44syl12anc 1117 . . . . . . . . . 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 445 . . . . . . . 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 2376 . . 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 4003 . 2 (𝑆 Po B𝑎 B 𝑏 B 𝑐 B𝑎𝑆𝑎 ((𝑎𝑆𝑏 𝑏𝑆𝑐) → 𝑎𝑆𝑐)))
55 df-po 4003 . 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 871   = wceq 1226   ∈ wcel 1370  ∀wral 2280   class class class wbr 3734   Po wpo 4001  ⟶wf 4821  –1-1-onto→wf1o 4824  ‘cfv 4825   Isom wiso 4826 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 532  ax-in2 533  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-sep 3845  ax-pow 3897  ax-pr 3914 This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-eu 1881  df-mo 1882  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ral 2285  df-rex 2286  df-v 2533  df-sbc 2738  df-un 2895  df-in 2897  df-ss 2904  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-uni 3551  df-br 3735  df-opab 3789  df-id 4000  df-po 4003  df-xp 4274  df-rel 4275  df-cnv 4276  df-co 4277  df-dm 4278  df-rn 4279  df-iota 4790  df-fun 4827  df-fn 4828  df-f 4829  df-f1 4830  df-f1o 4832  df-fv 4833  df-isom 4834 This theorem is referenced by:  isopo  5383  isosolem  5384
 Copyright terms: Public domain W3C validator