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 𝐴 ) ) |