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 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )