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		ffvelrn	⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝑑 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) ∈ 𝐵 )
4	3	ex	⊢ ( 𝐻 : 𝐴 ⟶ 𝐵 → ( 𝑑 ∈ 𝐴 → ( 𝐻 ‘ 𝑑 ) ∈ 𝐵 ) )
5		ffvelrn	⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝑒 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑒 ) ∈ 𝐵 )
6	5	ex	⊢ ( 𝐻 : 𝐴 ⟶ 𝐵 → ( 𝑒 ∈ 𝐴 → ( 𝐻 ‘ 𝑒 ) ∈ 𝐵 ) )
7		ffvelrn	⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝑓 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑓 ) ∈ 𝐵 )
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 𝐴 ) )