Metamath Proof Explorer

Theorem soisoi

Description: Infer isomorphism from one direction of an order proof for isomorphisms between strict orders. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Assertion soisoi ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y→HIsomR,SAB

Proof

Step Hyp Ref Expression
1 simprl ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y→H:A⟶ontoB
2 fof ⊢H:A⟶ontoB→H:A⟶B
3 1 2 syl ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y→H:A⟶B
4 sotrieq ⊢ROrA∧a∈A∧b∈A→a=b↔¬aRb∨bRa
5 4 con2bid ⊢ROrA∧a∈A∧b∈A→aRb∨bRa↔¬a=b
6 5 ad4ant14 ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→aRb∨bRa↔¬a=b
7 simprr ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y→∀x∈A∀y∈AxRy→H⁡xSH⁡y
8 breq1 ⊢x=a→xRy↔aRy
9 fveq2 ⊢x=a→H⁡x=H⁡a
10 9 breq1d ⊢x=a→H⁡xSH⁡y↔H⁡aSH⁡y
11 8 10 imbi12d ⊢x=a→xRy→H⁡xSH⁡y↔aRy→H⁡aSH⁡y
12 breq2 ⊢y=b→aRy↔aRb
13 fveq2 ⊢y=b→H⁡y=H⁡b
14 13 breq2d ⊢y=b→H⁡aSH⁡y↔H⁡aSH⁡b
15 12 14 imbi12d ⊢y=b→aRy→H⁡aSH⁡y↔aRb→H⁡aSH⁡b
16 11 15 rspc2va ⊢a∈A∧b∈A∧∀x∈A∀y∈AxRy→H⁡xSH⁡y→aRb→H⁡aSH⁡b
17 16 ancoms ⊢∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→aRb→H⁡aSH⁡b
18 7 17 sylan ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→aRb→H⁡aSH⁡b
19 simpllr ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→SPoB
20 simplrl ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→H:A⟶ontoB
21 20 2 syl ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→H:A⟶B
22 simprr ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→b∈A
23 21 22 ffvelcdmd ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→H⁡b∈B
24 poirr ⊢SPoB∧H⁡b∈B→¬H⁡bSH⁡b
25 breq1 ⊢H⁡a=H⁡b→H⁡aSH⁡b↔H⁡bSH⁡b
26 25 notbid ⊢H⁡a=H⁡b→¬H⁡aSH⁡b↔¬H⁡bSH⁡b
27 24 26 syl5ibrcom ⊢SPoB∧H⁡b∈B→H⁡a=H⁡b→¬H⁡aSH⁡b
28 19 23 27 syl2anc ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→H⁡a=H⁡b→¬H⁡aSH⁡b
29 28 con2d ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→H⁡aSH⁡b→¬H⁡a=H⁡b
30 18 29 syld ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→aRb→¬H⁡a=H⁡b
31 breq1 ⊢x=b→xRy↔bRy
32 fveq2 ⊢x=b→H⁡x=H⁡b
33 32 breq1d ⊢x=b→H⁡xSH⁡y↔H⁡bSH⁡y
34 31 33 imbi12d ⊢x=b→xRy→H⁡xSH⁡y↔bRy→H⁡bSH⁡y
35 breq2 ⊢y=a→bRy↔bRa
36 fveq2 ⊢y=a→H⁡y=H⁡a
37 36 breq2d ⊢y=a→H⁡bSH⁡y↔H⁡bSH⁡a
38 35 37 imbi12d ⊢y=a→bRy→H⁡bSH⁡y↔bRa→H⁡bSH⁡a
39 34 38 rspc2va ⊢b∈A∧a∈A∧∀x∈A∀y∈AxRy→H⁡xSH⁡y→bRa→H⁡bSH⁡a
40 39 ancoms ⊢∀x∈A∀y∈AxRy→H⁡xSH⁡y∧b∈A∧a∈A→bRa→H⁡bSH⁡a
41 40 ancom2s ⊢∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→bRa→H⁡bSH⁡a
42 7 41 sylan ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→bRa→H⁡bSH⁡a
43 breq2 ⊢H⁡a=H⁡b→H⁡bSH⁡a↔H⁡bSH⁡b
44 43 notbid ⊢H⁡a=H⁡b→¬H⁡bSH⁡a↔¬H⁡bSH⁡b
45 24 44 syl5ibrcom ⊢SPoB∧H⁡b∈B→H⁡a=H⁡b→¬H⁡bSH⁡a
46 19 23 45 syl2anc ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→H⁡a=H⁡b→¬H⁡bSH⁡a
47 46 con2d ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→H⁡bSH⁡a→¬H⁡a=H⁡b
48 42 47 syld ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→bRa→¬H⁡a=H⁡b
49 30 48 jaod ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→aRb∨bRa→¬H⁡a=H⁡b
50 6 49 sylbird ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→¬a=b→¬H⁡a=H⁡b
51 50 con4d ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→H⁡a=H⁡b→a=b
52 51 ralrimivva ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y→∀a∈A∀b∈AH⁡a=H⁡b→a=b
53 dff13 ⊢H:A⟶1-1B↔H:A⟶B∧∀a∈A∀b∈AH⁡a=H⁡b→a=b
54 3 52 53 sylanbrc ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y→H:A⟶1-1B
55 df-f1o ⊢H:A⟶1-1 ontoB↔H:A⟶1-1B∧H:A⟶ontoB
56 54 1 55 sylanbrc ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y→H:A⟶1-1 ontoB
57 sotric ⊢ROrA∧a∈A∧b∈A→aRb↔¬a=b∨bRa
58 57 con2bid ⊢ROrA∧a∈A∧b∈A→a=b∨bRa↔¬aRb
59 58 ad4ant14 ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→a=b∨bRa↔¬aRb
60 fveq2 ⊢a=b→H⁡a=H⁡b
61 60 breq1d ⊢a=b→H⁡aSH⁡b↔H⁡bSH⁡b
62 61 notbid ⊢a=b→¬H⁡aSH⁡b↔¬H⁡bSH⁡b
63 24 62 syl5ibrcom ⊢SPoB∧H⁡b∈B→a=b→¬H⁡aSH⁡b
64 19 23 63 syl2anc ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→a=b→¬H⁡aSH⁡b
65 simprl ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→a∈A
66 21 65 ffvelcdmd ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→H⁡a∈B
67 po2nr ⊢SPoB∧H⁡b∈B∧H⁡a∈B→¬H⁡bSH⁡a∧H⁡aSH⁡b
68 imnan ⊢H⁡bSH⁡a→¬H⁡aSH⁡b↔¬H⁡bSH⁡a∧H⁡aSH⁡b
69 67 68 sylibr ⊢SPoB∧H⁡b∈B∧H⁡a∈B→H⁡bSH⁡a→¬H⁡aSH⁡b
70 19 23 66 69 syl12anc ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→H⁡bSH⁡a→¬H⁡aSH⁡b
71 42 70 syld ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→bRa→¬H⁡aSH⁡b
72 64 71 jaod ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→a=b∨bRa→¬H⁡aSH⁡b
73 59 72 sylbird ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→¬aRb→¬H⁡aSH⁡b
74 18 73 impcon4bid ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y∧a∈A∧b∈A→aRb↔H⁡aSH⁡b
75 74 ralrimivva ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y→∀a∈A∀b∈AaRb↔H⁡aSH⁡b
76 df-isom ⊢HIsomR,SAB↔H:A⟶1-1 ontoB∧∀a∈A∀b∈AaRb↔H⁡aSH⁡b
77 56 75 76 sylanbrc ⊢ROrA∧SPoB∧H:A⟶ontoB∧∀x∈A∀y∈AxRy→H⁡xSH⁡y→HIsomR,SAB