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

Metamath Proof Explorer

Theorem isopolem

Description: Lemma for isopo . (Contributed by Stefan O'Rear, 16-Nov-2014)

Ref Expression
Assertion isopolem ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝑆 Po 𝐵 → 𝑅 Po 𝐴 ) )

Proof

Step Hyp Ref Expression
1 isof1o ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐻 : 𝐴 –1-1-onto→ 𝐵 )
2 f1of ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → 𝐻 : 𝐴 ⟶ 𝐵 )
3 ffvelcdm ⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝑑 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) ∈ 𝐵 )
4 3 ex ⊢ ( 𝐻 : 𝐴 ⟶ 𝐵 → ( 𝑑 ∈ 𝐴 → ( 𝐻 ‘ 𝑑 ) ∈ 𝐵 ) )
5 ffvelcdm ⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝑒 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑒 ) ∈ 𝐵 )
6 5 ex ⊢ ( 𝐻 : 𝐴 ⟶ 𝐵 → ( 𝑒 ∈ 𝐴 → ( 𝐻 ‘ 𝑒 ) ∈ 𝐵 ) )
7 ffvelcdm ⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝑓 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑓 ) ∈ 𝐵 )
8 7 ex ⊢ ( 𝐻 : 𝐴 ⟶ 𝐵 → ( 𝑓 ∈ 𝐴 → ( 𝐻 ‘ 𝑓 ) ∈ 𝐵 ) )
9 4 6 8 3anim123d ⊢ ( 𝐻 : 𝐴 ⟶ 𝐵 → ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑑 ) ∈ 𝐵 ∧ ( 𝐻 ‘ 𝑒 ) ∈ 𝐵 ∧ ( 𝐻 ‘ 𝑓 ) ∈ 𝐵 ) ) )
10 1 2 9 3syl ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑑 ) ∈ 𝐵 ∧ ( 𝐻 ‘ 𝑒 ) ∈ 𝐵 ∧ ( 𝐻 ‘ 𝑓 ) ∈ 𝐵 ) ) )
11 10 imp ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐴 ) ) → ( ( 𝐻 ‘ 𝑑 ) ∈ 𝐵 ∧ ( 𝐻 ‘ 𝑒 ) ∈ 𝐵 ∧ ( 𝐻 ‘ 𝑓 ) ∈ 𝐵 ) )
12 breq12 ⊢ ( ( 𝑎 = ( 𝐻 ‘ 𝑑 ) ∧ 𝑎 = ( 𝐻 ‘ 𝑑 ) ) → ( 𝑎 𝑆 𝑎 ↔ ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑑 ) ) )
13 12 anidms ⊢ ( 𝑎 = ( 𝐻 ‘ 𝑑 ) → ( 𝑎 𝑆 𝑎 ↔ ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑑 ) ) )
14 13 notbid ⊢ ( 𝑎 = ( 𝐻 ‘ 𝑑 ) → ( ¬ 𝑎 𝑆 𝑎 ↔ ¬ ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑑 ) ) )
15 breq1 ⊢ ( 𝑎 = ( 𝐻 ‘ 𝑑 ) → ( 𝑎 𝑆 𝑏 ↔ ( 𝐻 ‘ 𝑑 ) 𝑆 𝑏 ) )
16 15 anbi1d ⊢ ( 𝑎 = ( 𝐻 ‘ 𝑑 ) → ( ( 𝑎 𝑆 𝑏 ∧ 𝑏 𝑆 𝑐 ) ↔ ( ( 𝐻 ‘ 𝑑 ) 𝑆 𝑏 ∧ 𝑏 𝑆 𝑐 ) ) )
17 breq1 ⊢ ( 𝑎 = ( 𝐻 ‘ 𝑑 ) → ( 𝑎 𝑆 𝑐 ↔ ( 𝐻 ‘ 𝑑 ) 𝑆 𝑐 ) )
18 16 17 imbi12d ⊢ ( 𝑎 = ( 𝐻 ‘ 𝑑 ) → ( ( ( 𝑎 𝑆 𝑏 ∧ 𝑏 𝑆 𝑐 ) → 𝑎 𝑆 𝑐 ) ↔ ( ( ( 𝐻 ‘ 𝑑 ) 𝑆 𝑏 ∧ 𝑏 𝑆 𝑐 ) → ( 𝐻 ‘ 𝑑 ) 𝑆 𝑐 ) ) )
19 14 18 anbi12d ⊢ ( 𝑎 = ( 𝐻 ‘ 𝑑 ) → ( ( ¬ 𝑎 𝑆 𝑎 ∧ ( ( 𝑎 𝑆 𝑏 ∧ 𝑏 𝑆 𝑐 ) → 𝑎 𝑆 𝑐 ) ) ↔ ( ¬ ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑑 ) ∧ ( ( ( 𝐻 ‘ 𝑑 ) 𝑆 𝑏 ∧ 𝑏 𝑆 𝑐 ) → ( 𝐻 ‘ 𝑑 ) 𝑆 𝑐 ) ) ) )
20 breq2 ⊢ ( 𝑏 = ( 𝐻 ‘ 𝑒 ) → ( ( 𝐻 ‘ 𝑑 ) 𝑆 𝑏 ↔ ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑒 ) ) )
21 breq1 ⊢ ( 𝑏 = ( 𝐻 ‘ 𝑒 ) → ( 𝑏 𝑆 𝑐 ↔ ( 𝐻 ‘ 𝑒 ) 𝑆 𝑐 ) )
22 20 21 anbi12d ⊢ ( 𝑏 = ( 𝐻 ‘ 𝑒 ) → ( ( ( 𝐻 ‘ 𝑑 ) 𝑆 𝑏 ∧ 𝑏 𝑆 𝑐 ) ↔ ( ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑒 ) ∧ ( 𝐻 ‘ 𝑒 ) 𝑆 𝑐 ) ) )
23 22 imbi1d ⊢ ( 𝑏 = ( 𝐻 ‘ 𝑒 ) → ( ( ( ( 𝐻 ‘ 𝑑 ) 𝑆 𝑏 ∧ 𝑏 𝑆 𝑐 ) → ( 𝐻 ‘ 𝑑 ) 𝑆 𝑐 ) ↔ ( ( ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑒 ) ∧ ( 𝐻 ‘ 𝑒 ) 𝑆 𝑐 ) → ( 𝐻 ‘ 𝑑 ) 𝑆 𝑐 ) ) )
24 23 anbi2d ⊢ ( 𝑏 = ( 𝐻 ‘ 𝑒 ) → ( ( ¬ ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑑 ) ∧ ( ( ( 𝐻 ‘ 𝑑 ) 𝑆 𝑏 ∧ 𝑏 𝑆 𝑐 ) → ( 𝐻 ‘ 𝑑 ) 𝑆 𝑐 ) ) ↔ ( ¬ ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑑 ) ∧ ( ( ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑒 ) ∧ ( 𝐻 ‘ 𝑒 ) 𝑆 𝑐 ) → ( 𝐻 ‘ 𝑑 ) 𝑆 𝑐 ) ) ) )
25 breq2 ⊢ ( 𝑐 = ( 𝐻 ‘ 𝑓 ) → ( ( 𝐻 ‘ 𝑒 ) 𝑆 𝑐 ↔ ( 𝐻 ‘ 𝑒 ) 𝑆 ( 𝐻 ‘ 𝑓 ) ) )
26 25 anbi2d ⊢ ( 𝑐 = ( 𝐻 ‘ 𝑓 ) → ( ( ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑒 ) ∧ ( 𝐻 ‘ 𝑒 ) 𝑆 𝑐 ) ↔ ( ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑒 ) ∧ ( 𝐻 ‘ 𝑒 ) 𝑆 ( 𝐻 ‘ 𝑓 ) ) ) )
27 breq2 ⊢ ( 𝑐 = ( 𝐻 ‘ 𝑓 ) → ( ( 𝐻 ‘ 𝑑 ) 𝑆 𝑐 ↔ ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑓 ) ) )
28 26 27 imbi12d ⊢ ( 𝑐 = ( 𝐻 ‘ 𝑓 ) → ( ( ( ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑒 ) ∧ ( 𝐻 ‘ 𝑒 ) 𝑆 𝑐 ) → ( 𝐻 ‘ 𝑑 ) 𝑆 𝑐 ) ↔ ( ( ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑒 ) ∧ ( 𝐻 ‘ 𝑒 ) 𝑆 ( 𝐻 ‘ 𝑓 ) ) → ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑓 ) ) ) )
29 28 anbi2d ⊢ ( 𝑐 = ( 𝐻 ‘ 𝑓 ) → ( ( ¬ ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑑 ) ∧ ( ( ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑒 ) ∧ ( 𝐻 ‘ 𝑒 ) 𝑆 𝑐 ) → ( 𝐻 ‘ 𝑑 ) 𝑆 𝑐 ) ) ↔ ( ¬ ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑑 ) ∧ ( ( ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑒 ) ∧ ( 𝐻 ‘ 𝑒 ) 𝑆 ( 𝐻 ‘ 𝑓 ) ) → ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑓 ) ) ) ) )
30 19 24 29 rspc3v ⊢ ( ( ( 𝐻 ‘ 𝑑 ) ∈ 𝐵 ∧ ( 𝐻 ‘ 𝑒 ) ∈ 𝐵 ∧ ( 𝐻 ‘ 𝑓 ) ∈ 𝐵 ) → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑎 𝑆 𝑎 ∧ ( ( 𝑎 𝑆 𝑏 ∧ 𝑏 𝑆 𝑐 ) → 𝑎 𝑆 𝑐 ) ) → ( ¬ ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑑 ) ∧ ( ( ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑒 ) ∧ ( 𝐻 ‘ 𝑒 ) 𝑆 ( 𝐻 ‘ 𝑓 ) ) → ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑓 ) ) ) ) )
31 11 30 syl ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐴 ) ) → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑎 𝑆 𝑎 ∧ ( ( 𝑎 𝑆 𝑏 ∧ 𝑏 𝑆 𝑐 ) → 𝑎 𝑆 𝑐 ) ) → ( ¬ ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑑 ) ∧ ( ( ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑒 ) ∧ ( 𝐻 ‘ 𝑒 ) 𝑆 ( 𝐻 ‘ 𝑓 ) ) → ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑓 ) ) ) ) )
32 simpl ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐴 ) ) → 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
33 simpr1 ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐴 ) ) → 𝑑 ∈ 𝐴 )
34 isorel ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) → ( 𝑑 𝑅 𝑑 ↔ ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑑 ) ) )
35 32 33 33 34 syl12anc ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐴 ) ) → ( 𝑑 𝑅 𝑑 ↔ ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑑 ) ) )
36 35 notbid ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐴 ) ) → ( ¬ 𝑑 𝑅 𝑑 ↔ ¬ ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑑 ) ) )
37 simpr2 ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐴 ) ) → 𝑒 ∈ 𝐴 )
38 isorel ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ) → ( 𝑑 𝑅 𝑒 ↔ ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑒 ) ) )
39 32 33 37 38 syl12anc ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐴 ) ) → ( 𝑑 𝑅 𝑒 ↔ ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑒 ) ) )
40 simpr3 ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐴 ) ) → 𝑓 ∈ 𝐴 )
41 isorel ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐴 ) ) → ( 𝑒 𝑅 𝑓 ↔ ( 𝐻 ‘ 𝑒 ) 𝑆 ( 𝐻 ‘ 𝑓 ) ) )
42 32 37 40 41 syl12anc ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐴 ) ) → ( 𝑒 𝑅 𝑓 ↔ ( 𝐻 ‘ 𝑒 ) 𝑆 ( 𝐻 ‘ 𝑓 ) ) )
43 39 42 anbi12d ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐴 ) ) → ( ( 𝑑 𝑅 𝑒 ∧ 𝑒 𝑅 𝑓 ) ↔ ( ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑒 ) ∧ ( 𝐻 ‘ 𝑒 ) 𝑆 ( 𝐻 ‘ 𝑓 ) ) ) )
44 isorel ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑓 ∈ 𝐴 ) ) → ( 𝑑 𝑅 𝑓 ↔ ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑓 ) ) )
45 32 33 40 44 syl12anc ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐴 ) ) → ( 𝑑 𝑅 𝑓 ↔ ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑓 ) ) )
46 43 45 imbi12d ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐴 ) ) → ( ( ( 𝑑 𝑅 𝑒 ∧ 𝑒 𝑅 𝑓 ) → 𝑑 𝑅 𝑓 ) ↔ ( ( ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑒 ) ∧ ( 𝐻 ‘ 𝑒 ) 𝑆 ( 𝐻 ‘ 𝑓 ) ) → ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑓 ) ) ) )
47 36 46 anbi12d ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐴 ) ) → ( ( ¬ 𝑑 𝑅 𝑑 ∧ ( ( 𝑑 𝑅 𝑒 ∧ 𝑒 𝑅 𝑓 ) → 𝑑 𝑅 𝑓 ) ) ↔ ( ¬ ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑑 ) ∧ ( ( ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑒 ) ∧ ( 𝐻 ‘ 𝑒 ) 𝑆 ( 𝐻 ‘ 𝑓 ) ) → ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑓 ) ) ) ) )
48 31 47 sylibrd ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐴 ) ) → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑎 𝑆 𝑎 ∧ ( ( 𝑎 𝑆 𝑏 ∧ 𝑏 𝑆 𝑐 ) → 𝑎 𝑆 𝑐 ) ) → ( ¬ 𝑑 𝑅 𝑑 ∧ ( ( 𝑑 𝑅 𝑒 ∧ 𝑒 𝑅 𝑓 ) → 𝑑 𝑅 𝑓 ) ) ) )
49 48 ex ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐴 ) → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑎 𝑆 𝑎 ∧ ( ( 𝑎 𝑆 𝑏 ∧ 𝑏 𝑆 𝑐 ) → 𝑎 𝑆 𝑐 ) ) → ( ¬ 𝑑 𝑅 𝑑 ∧ ( ( 𝑑 𝑅 𝑒 ∧ 𝑒 𝑅 𝑓 ) → 𝑑 𝑅 𝑓 ) ) ) ) )
50 49 com23 ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑎 𝑆 𝑎 ∧ ( ( 𝑎 𝑆 𝑏 ∧ 𝑏 𝑆 𝑐 ) → 𝑎 𝑆 𝑐 ) ) → ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐴 ) → ( ¬ 𝑑 𝑅 𝑑 ∧ ( ( 𝑑 𝑅 𝑒 ∧ 𝑒 𝑅 𝑓 ) → 𝑑 𝑅 𝑓 ) ) ) ) )
51 50 imp31 ⊢ ( ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑎 𝑆 𝑎 ∧ ( ( 𝑎 𝑆 𝑏 ∧ 𝑏 𝑆 𝑐 ) → 𝑎 𝑆 𝑐 ) ) ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐴 ) ) → ( ¬ 𝑑 𝑅 𝑑 ∧ ( ( 𝑑 𝑅 𝑒 ∧ 𝑒 𝑅 𝑓 ) → 𝑑 𝑅 𝑓 ) ) )
52 51 ralrimivvva ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑎 𝑆 𝑎 ∧ ( ( 𝑎 𝑆 𝑏 ∧ 𝑏 𝑆 𝑐 ) → 𝑎 𝑆 𝑐 ) ) ) → ∀ 𝑑 ∈ 𝐴 ∀ 𝑒 ∈ 𝐴 ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑑 𝑅 𝑑 ∧ ( ( 𝑑 𝑅 𝑒 ∧ 𝑒 𝑅 𝑓 ) → 𝑑 𝑅 𝑓 ) ) )
53 52 ex ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑎 𝑆 𝑎 ∧ ( ( 𝑎 𝑆 𝑏 ∧ 𝑏 𝑆 𝑐 ) → 𝑎 𝑆 𝑐 ) ) → ∀ 𝑑 ∈ 𝐴 ∀ 𝑒 ∈ 𝐴 ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑑 𝑅 𝑑 ∧ ( ( 𝑑 𝑅 𝑒 ∧ 𝑒 𝑅 𝑓 ) → 𝑑 𝑅 𝑓 ) ) ) )
54 df-po ⊢ ( 𝑆 Po 𝐵 ↔ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑎 𝑆 𝑎 ∧ ( ( 𝑎 𝑆 𝑏 ∧ 𝑏 𝑆 𝑐 ) → 𝑎 𝑆 𝑐 ) ) )
55 df-po ⊢ ( 𝑅 Po 𝐴 ↔ ∀ 𝑑 ∈ 𝐴 ∀ 𝑒 ∈ 𝐴 ∀ 𝑓 ∈ 𝐴 ( ¬ 𝑑 𝑅 𝑑 ∧ ( ( 𝑑 𝑅 𝑒 ∧ 𝑒 𝑅 𝑓 ) → 𝑑 𝑅 𝑓 ) ) )
56 53 54 55 3imtr4g ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝑆 Po 𝐵 → 𝑅 Po 𝐴 ) )