Metamath Proof Explorer

Theorem isosolem

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

Ref Expression
Assertion isosolem ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝑆 Or 𝐵 → 𝑅 Or 𝐴 ) )

Proof

Step Hyp Ref Expression
1 isopolem ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝑆 Po 𝐵 → 𝑅 Po 𝐴 ) )
2 isof1o ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐻 : 𝐴 –1-1-onto→ 𝐵 )
3 f1of ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → 𝐻 : 𝐴 ⟶ 𝐵 )
4 ffvelrn ⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝑐 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑐 ) ∈ 𝐵 )
5 4 ex ⊢ ( 𝐻 : 𝐴 ⟶ 𝐵 → ( 𝑐 ∈ 𝐴 → ( 𝐻 ‘ 𝑐 ) ∈ 𝐵 ) )
6 ffvelrn ⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝑑 ∈ 𝐴 ) → ( 𝐻 ‘ 𝑑 ) ∈ 𝐵 )
7 6 ex ⊢ ( 𝐻 : 𝐴 ⟶ 𝐵 → ( 𝑑 ∈ 𝐴 → ( 𝐻 ‘ 𝑑 ) ∈ 𝐵 ) )
8 5 7 anim12d ⊢ ( 𝐻 : 𝐴 ⟶ 𝐵 → ( ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑐 ) ∈ 𝐵 ∧ ( 𝐻 ‘ 𝑑 ) ∈ 𝐵 ) ) )
9 2 3 8 3syl ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) → ( ( 𝐻 ‘ 𝑐 ) ∈ 𝐵 ∧ ( 𝐻 ‘ 𝑑 ) ∈ 𝐵 ) ) )
10 9 imp ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) → ( ( 𝐻 ‘ 𝑐 ) ∈ 𝐵 ∧ ( 𝐻 ‘ 𝑑 ) ∈ 𝐵 ) )
11 breq1 ⊢ ( 𝑎 = ( 𝐻 ‘ 𝑐 ) → ( 𝑎 𝑆 𝑏 ↔ ( 𝐻 ‘ 𝑐 ) 𝑆 𝑏 ) )
12 eqeq1 ⊢ ( 𝑎 = ( 𝐻 ‘ 𝑐 ) → ( 𝑎 = 𝑏 ↔ ( 𝐻 ‘ 𝑐 ) = 𝑏 ) )
13 breq2 ⊢ ( 𝑎 = ( 𝐻 ‘ 𝑐 ) → ( 𝑏 𝑆 𝑎 ↔ 𝑏 𝑆 ( 𝐻 ‘ 𝑐 ) ) )
14 11 12 13 3orbi123d ⊢ ( 𝑎 = ( 𝐻 ‘ 𝑐 ) → ( ( 𝑎 𝑆 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑆 𝑎 ) ↔ ( ( 𝐻 ‘ 𝑐 ) 𝑆 𝑏 ∨ ( 𝐻 ‘ 𝑐 ) = 𝑏 ∨ 𝑏 𝑆 ( 𝐻 ‘ 𝑐 ) ) ) )
15 breq2 ⊢ ( 𝑏 = ( 𝐻 ‘ 𝑑 ) → ( ( 𝐻 ‘ 𝑐 ) 𝑆 𝑏 ↔ ( 𝐻 ‘ 𝑐 ) 𝑆 ( 𝐻 ‘ 𝑑 ) ) )
16 eqeq2 ⊢ ( 𝑏 = ( 𝐻 ‘ 𝑑 ) → ( ( 𝐻 ‘ 𝑐 ) = 𝑏 ↔ ( 𝐻 ‘ 𝑐 ) = ( 𝐻 ‘ 𝑑 ) ) )
17 breq1 ⊢ ( 𝑏 = ( 𝐻 ‘ 𝑑 ) → ( 𝑏 𝑆 ( 𝐻 ‘ 𝑐 ) ↔ ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑐 ) ) )
18 15 16 17 3orbi123d ⊢ ( 𝑏 = ( 𝐻 ‘ 𝑑 ) → ( ( ( 𝐻 ‘ 𝑐 ) 𝑆 𝑏 ∨ ( 𝐻 ‘ 𝑐 ) = 𝑏 ∨ 𝑏 𝑆 ( 𝐻 ‘ 𝑐 ) ) ↔ ( ( 𝐻 ‘ 𝑐 ) 𝑆 ( 𝐻 ‘ 𝑑 ) ∨ ( 𝐻 ‘ 𝑐 ) = ( 𝐻 ‘ 𝑑 ) ∨ ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑐 ) ) ) )
19 14 18 rspc2v ⊢ ( ( ( 𝐻 ‘ 𝑐 ) ∈ 𝐵 ∧ ( 𝐻 ‘ 𝑑 ) ∈ 𝐵 ) → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 𝑆 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑆 𝑎 ) → ( ( 𝐻 ‘ 𝑐 ) 𝑆 ( 𝐻 ‘ 𝑑 ) ∨ ( 𝐻 ‘ 𝑐 ) = ( 𝐻 ‘ 𝑑 ) ∨ ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑐 ) ) ) )
20 10 19 syl ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 𝑆 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑆 𝑎 ) → ( ( 𝐻 ‘ 𝑐 ) 𝑆 ( 𝐻 ‘ 𝑑 ) ∨ ( 𝐻 ‘ 𝑐 ) = ( 𝐻 ‘ 𝑑 ) ∨ ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑐 ) ) ) )
21 isorel ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) → ( 𝑐 𝑅 𝑑 ↔ ( 𝐻 ‘ 𝑐 ) 𝑆 ( 𝐻 ‘ 𝑑 ) ) )
22 f1of1 ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → 𝐻 : 𝐴 –1-1→ 𝐵 )
23 2 22 syl ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐻 : 𝐴 –1-1→ 𝐵 )
24 f1fveq ⊢ ( ( 𝐻 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) → ( ( 𝐻 ‘ 𝑐 ) = ( 𝐻 ‘ 𝑑 ) ↔ 𝑐 = 𝑑 ) )
25 23 24 sylan ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) → ( ( 𝐻 ‘ 𝑐 ) = ( 𝐻 ‘ 𝑑 ) ↔ 𝑐 = 𝑑 ) )
26 25 bicomd ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) → ( 𝑐 = 𝑑 ↔ ( 𝐻 ‘ 𝑐 ) = ( 𝐻 ‘ 𝑑 ) ) )
27 isorel ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) → ( 𝑑 𝑅 𝑐 ↔ ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑐 ) ) )
28 27 ancom2s ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) → ( 𝑑 𝑅 𝑐 ↔ ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑐 ) ) )
29 21 26 28 3orbi123d ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) → ( ( 𝑐 𝑅 𝑑 ∨ 𝑐 = 𝑑 ∨ 𝑑 𝑅 𝑐 ) ↔ ( ( 𝐻 ‘ 𝑐 ) 𝑆 ( 𝐻 ‘ 𝑑 ) ∨ ( 𝐻 ‘ 𝑐 ) = ( 𝐻 ‘ 𝑑 ) ∨ ( 𝐻 ‘ 𝑑 ) 𝑆 ( 𝐻 ‘ 𝑐 ) ) ) )
30 20 29 sylibrd ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ) → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 𝑆 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑆 𝑎 ) → ( 𝑐 𝑅 𝑑 ∨ 𝑐 = 𝑑 ∨ 𝑑 𝑅 𝑐 ) ) )
31 30 ralrimdvva ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 𝑆 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑆 𝑎 ) → ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐴 ( 𝑐 𝑅 𝑑 ∨ 𝑐 = 𝑑 ∨ 𝑑 𝑅 𝑐 ) ) )
32 1 31 anim12d ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( ( 𝑆 Po 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 𝑆 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑆 𝑎 ) ) → ( 𝑅 Po 𝐴 ∧ ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐴 ( 𝑐 𝑅 𝑑 ∨ 𝑐 = 𝑑 ∨ 𝑑 𝑅 𝑐 ) ) ) )
33 df-so ⊢ ( 𝑆 Or 𝐵 ↔ ( 𝑆 Po 𝐵 ∧ ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( 𝑎 𝑆 𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏 𝑆 𝑎 ) ) )
34 df-so ⊢ ( 𝑅 Or 𝐴 ↔ ( 𝑅 Po 𝐴 ∧ ∀ 𝑐 ∈ 𝐴 ∀ 𝑑 ∈ 𝐴 ( 𝑐 𝑅 𝑑 ∨ 𝑐 = 𝑑 ∨ 𝑑 𝑅 𝑐 ) ) )
35 32 33 34 3imtr4g ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝑆 Or 𝐵 → 𝑅 Or 𝐴 ) )