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