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