This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) → 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simprl ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) → 𝐻 : 𝐴 –onto→ 𝐵 )
2 fof ⊢ ( 𝐻 : 𝐴 –onto→ 𝐵 → 𝐻 : 𝐴 ⟶ 𝐵 )
3 1 2 syl ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) → 𝐻 : 𝐴 ⟶ 𝐵 )
4 sotrieq ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( 𝑎 = 𝑏 ↔ ¬ ( 𝑎 𝑅 𝑏 ∨ 𝑏 𝑅 𝑎 ) ) )
5 4 con2bid ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( ( 𝑎 𝑅 𝑏 ∨ 𝑏 𝑅 𝑎 ) ↔ ¬ 𝑎 = 𝑏 ) )
6 5 ad4ant14 ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( ( 𝑎 𝑅 𝑏 ∨ 𝑏 𝑅 𝑎 ) ↔ ¬ 𝑎 = 𝑏 ) )
7 simprr ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) )
8 breq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 𝑅 𝑦 ↔ 𝑎 𝑅 𝑦 ) )
9 fveq2 ⊢ ( 𝑥 = 𝑎 → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑎 ) )
10 9 breq1d ⊢ ( 𝑥 = 𝑎 → ( ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ↔ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) )
11 8 10 imbi12d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ↔ ( 𝑎 𝑅 𝑦 → ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) )
12 breq2 ⊢ ( 𝑦 = 𝑏 → ( 𝑎 𝑅 𝑦 ↔ 𝑎 𝑅 𝑏 ) )
13 fveq2 ⊢ ( 𝑦 = 𝑏 → ( 𝐻 ‘ 𝑦 ) = ( 𝐻 ‘ 𝑏 ) )
14 13 breq2d ⊢ ( 𝑦 = 𝑏 → ( ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ↔ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) )
15 12 14 imbi12d ⊢ ( 𝑦 = 𝑏 → ( ( 𝑎 𝑅 𝑦 → ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ↔ ( 𝑎 𝑅 𝑏 → ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) ) )
16 11 15 rspc2va ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) → ( 𝑎 𝑅 𝑏 → ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) )
17 16 ancoms ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( 𝑎 𝑅 𝑏 → ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) )
18 7 17 sylan ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( 𝑎 𝑅 𝑏 → ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) )
19 simpllr ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → 𝑆 Po 𝐵 )
20 simplrl ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → 𝐻 : 𝐴 –onto→ 𝐵 )
21 20 2 syl ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → 𝐻 : 𝐴 ⟶ 𝐵 )
22 simprr ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → 𝑏 ∈ 𝐴 )
23 21 22 ffvelcdmd ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( 𝐻 ‘ 𝑏 ) ∈ 𝐵 )
24 poirr ⊢ ( ( 𝑆 Po 𝐵 ∧ ( 𝐻 ‘ 𝑏 ) ∈ 𝐵 ) → ¬ ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑏 ) )
25 breq1 ⊢ ( ( 𝐻 ‘ 𝑎 ) = ( 𝐻 ‘ 𝑏 ) → ( ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ↔ ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) )
26 25 notbid ⊢ ( ( 𝐻 ‘ 𝑎 ) = ( 𝐻 ‘ 𝑏 ) → ( ¬ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ↔ ¬ ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) )
27 24 26 syl5ibrcom ⊢ ( ( 𝑆 Po 𝐵 ∧ ( 𝐻 ‘ 𝑏 ) ∈ 𝐵 ) → ( ( 𝐻 ‘ 𝑎 ) = ( 𝐻 ‘ 𝑏 ) → ¬ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) )
28 19 23 27 syl2anc ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( ( 𝐻 ‘ 𝑎 ) = ( 𝐻 ‘ 𝑏 ) → ¬ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) )
29 28 con2d ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) → ¬ ( 𝐻 ‘ 𝑎 ) = ( 𝐻 ‘ 𝑏 ) ) )
30 18 29 syld ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( 𝑎 𝑅 𝑏 → ¬ ( 𝐻 ‘ 𝑎 ) = ( 𝐻 ‘ 𝑏 ) ) )
31 breq1 ⊢ ( 𝑥 = 𝑏 → ( 𝑥 𝑅 𝑦 ↔ 𝑏 𝑅 𝑦 ) )
32 fveq2 ⊢ ( 𝑥 = 𝑏 → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑏 ) )
33 32 breq1d ⊢ ( 𝑥 = 𝑏 → ( ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ↔ ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) )
34 31 33 imbi12d ⊢ ( 𝑥 = 𝑏 → ( ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ↔ ( 𝑏 𝑅 𝑦 → ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) )
35 breq2 ⊢ ( 𝑦 = 𝑎 → ( 𝑏 𝑅 𝑦 ↔ 𝑏 𝑅 𝑎 ) )
36 fveq2 ⊢ ( 𝑦 = 𝑎 → ( 𝐻 ‘ 𝑦 ) = ( 𝐻 ‘ 𝑎 ) )
37 36 breq2d ⊢ ( 𝑦 = 𝑎 → ( ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ↔ ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑎 ) ) )
38 35 37 imbi12d ⊢ ( 𝑦 = 𝑎 → ( ( 𝑏 𝑅 𝑦 → ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ↔ ( 𝑏 𝑅 𝑎 → ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑎 ) ) ) )
39 34 38 rspc2va ⊢ ( ( ( 𝑏 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) → ( 𝑏 𝑅 𝑎 → ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑎 ) ) )
40 39 ancoms ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ) ) → ( 𝑏 𝑅 𝑎 → ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑎 ) ) )
41 40 ancom2s ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( 𝑏 𝑅 𝑎 → ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑎 ) ) )
42 7 41 sylan ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( 𝑏 𝑅 𝑎 → ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑎 ) ) )
43 breq2 ⊢ ( ( 𝐻 ‘ 𝑎 ) = ( 𝐻 ‘ 𝑏 ) → ( ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑎 ) ↔ ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) )
44 43 notbid ⊢ ( ( 𝐻 ‘ 𝑎 ) = ( 𝐻 ‘ 𝑏 ) → ( ¬ ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑎 ) ↔ ¬ ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) )
45 24 44 syl5ibrcom ⊢ ( ( 𝑆 Po 𝐵 ∧ ( 𝐻 ‘ 𝑏 ) ∈ 𝐵 ) → ( ( 𝐻 ‘ 𝑎 ) = ( 𝐻 ‘ 𝑏 ) → ¬ ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑎 ) ) )
46 19 23 45 syl2anc ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( ( 𝐻 ‘ 𝑎 ) = ( 𝐻 ‘ 𝑏 ) → ¬ ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑎 ) ) )
47 46 con2d ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑎 ) → ¬ ( 𝐻 ‘ 𝑎 ) = ( 𝐻 ‘ 𝑏 ) ) )
48 42 47 syld ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( 𝑏 𝑅 𝑎 → ¬ ( 𝐻 ‘ 𝑎 ) = ( 𝐻 ‘ 𝑏 ) ) )
49 30 48 jaod ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( ( 𝑎 𝑅 𝑏 ∨ 𝑏 𝑅 𝑎 ) → ¬ ( 𝐻 ‘ 𝑎 ) = ( 𝐻 ‘ 𝑏 ) ) )
50 6 49 sylbird ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( ¬ 𝑎 = 𝑏 → ¬ ( 𝐻 ‘ 𝑎 ) = ( 𝐻 ‘ 𝑏 ) ) )
51 50 con4d ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( ( 𝐻 ‘ 𝑎 ) = ( 𝐻 ‘ 𝑏 ) → 𝑎 = 𝑏 ) )
52 51 ralrimivva ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) → ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( ( 𝐻 ‘ 𝑎 ) = ( 𝐻 ‘ 𝑏 ) → 𝑎 = 𝑏 ) )
53 dff13 ⊢ ( 𝐻 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( ( 𝐻 ‘ 𝑎 ) = ( 𝐻 ‘ 𝑏 ) → 𝑎 = 𝑏 ) ) )
54 3 52 53 sylanbrc ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) → 𝐻 : 𝐴 –1-1→ 𝐵 )
55 df-f1o ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ 𝐻 : 𝐴 –onto→ 𝐵 ) )
56 54 1 55 sylanbrc ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) → 𝐻 : 𝐴 –1-1-onto→ 𝐵 )
57 sotric ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( 𝑎 𝑅 𝑏 ↔ ¬ ( 𝑎 = 𝑏 ∨ 𝑏 𝑅 𝑎 ) ) )
58 57 con2bid ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( ( 𝑎 = 𝑏 ∨ 𝑏 𝑅 𝑎 ) ↔ ¬ 𝑎 𝑅 𝑏 ) )
59 58 ad4ant14 ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( ( 𝑎 = 𝑏 ∨ 𝑏 𝑅 𝑎 ) ↔ ¬ 𝑎 𝑅 𝑏 ) )
60 fveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝐻 ‘ 𝑎 ) = ( 𝐻 ‘ 𝑏 ) )
61 60 breq1d ⊢ ( 𝑎 = 𝑏 → ( ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ↔ ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) )
62 61 notbid ⊢ ( 𝑎 = 𝑏 → ( ¬ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ↔ ¬ ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) )
63 24 62 syl5ibrcom ⊢ ( ( 𝑆 Po 𝐵 ∧ ( 𝐻 ‘ 𝑏 ) ∈ 𝐵 ) → ( 𝑎 = 𝑏 → ¬ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) )
64 19 23 63 syl2anc ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( 𝑎 = 𝑏 → ¬ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) )
65 simprl ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → 𝑎 ∈ 𝐴 )
66 21 65 ffvelcdmd ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( 𝐻 ‘ 𝑎 ) ∈ 𝐵 )
67 po2nr ⊢ ( ( 𝑆 Po 𝐵 ∧ ( ( 𝐻 ‘ 𝑏 ) ∈ 𝐵 ∧ ( 𝐻 ‘ 𝑎 ) ∈ 𝐵 ) ) → ¬ ( ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑎 ) ∧ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) )
68 imnan ⊢ ( ( ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑎 ) → ¬ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) ↔ ¬ ( ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑎 ) ∧ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) )
69 67 68 sylibr ⊢ ( ( 𝑆 Po 𝐵 ∧ ( ( 𝐻 ‘ 𝑏 ) ∈ 𝐵 ∧ ( 𝐻 ‘ 𝑎 ) ∈ 𝐵 ) ) → ( ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑎 ) → ¬ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) )
70 19 23 66 69 syl12anc ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( ( 𝐻 ‘ 𝑏 ) 𝑆 ( 𝐻 ‘ 𝑎 ) → ¬ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) )
71 42 70 syld ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( 𝑏 𝑅 𝑎 → ¬ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) )
72 64 71 jaod ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( ( 𝑎 = 𝑏 ∨ 𝑏 𝑅 𝑎 ) → ¬ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) )
73 59 72 sylbird ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( ¬ 𝑎 𝑅 𝑏 → ¬ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) )
74 18 73 impcon4bid ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → ( 𝑎 𝑅 𝑏 ↔ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) )
75 74 ralrimivva ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) → ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 𝑅 𝑏 ↔ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) )
76 df-isom ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐴 ( 𝑎 𝑅 𝑏 ↔ ( 𝐻 ‘ 𝑎 ) 𝑆 ( 𝐻 ‘ 𝑏 ) ) ) )
77 56 75 76 sylanbrc ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝐻 : 𝐴 –onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ) → 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )