This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem soisores

Description: Express the condition of isomorphism on two strict orders for a function's restriction. (Contributed by Mario Carneiro, 22-Jan-2015)

Ref Expression
Assertion soisores ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ) → ( ( 𝐹 ↾ 𝐴 ) Isom 𝑅 , 𝑆 ( 𝐴 , ( 𝐹 “ 𝐴 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 isorel ⊢ ( ( ( 𝐹 ↾ 𝐴 ) Isom 𝑅 , 𝑆 ( 𝐴 , ( 𝐹 “ 𝐴 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) 𝑆 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ) )
2 fvres ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
3 fvres ⊢ ( 𝑦 ∈ 𝐴 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
4 2 3 breqan12d ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) 𝑆 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) )
5 4 adantl ⊢ ( ( ( 𝐹 ↾ 𝐴 ) Isom 𝑅 , 𝑆 ( 𝐴 , ( 𝐹 “ 𝐴 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) 𝑆 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) )
6 1 5 bitrd ⊢ ( ( ( 𝐹 ↾ 𝐴 ) Isom 𝑅 , 𝑆 ( 𝐴 , ( 𝐹 “ 𝐴 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 𝑅 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) )
7 6 biimpd ⊢ ( ( ( 𝐹 ↾ 𝐴 ) Isom 𝑅 , 𝑆 ( 𝐴 , ( 𝐹 “ 𝐴 ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) )
8 7 ralrimivva ⊢ ( ( 𝐹 ↾ 𝐴 ) Isom 𝑅 , 𝑆 ( 𝐴 , ( 𝐹 “ 𝐴 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) )
9 ffn ⊢ ( 𝐹 : 𝐵 ⟶ 𝐶 → 𝐹 Fn 𝐵 )
10 9 ad2antrl ⊢ ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ) → 𝐹 Fn 𝐵 )
11 simprr ⊢ ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ) → 𝐴 ⊆ 𝐵 )
12 fnssres ⊢ ( ( 𝐹 Fn 𝐵 ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐹 ↾ 𝐴 ) Fn 𝐴 )
13 10 11 12 syl2anc ⊢ ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ) → ( 𝐹 ↾ 𝐴 ) Fn 𝐴 )
14 13 3adant3 ⊢ ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ↾ 𝐴 ) Fn 𝐴 )
15 df-ima ⊢ ( 𝐹 “ 𝐴 ) = ran ( 𝐹 ↾ 𝐴 )
16 15 eqcomi ⊢ ran ( 𝐹 ↾ 𝐴 ) = ( 𝐹 “ 𝐴 )
17 16 a1i ⊢ ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) → ran ( 𝐹 ↾ 𝐴 ) = ( 𝐹 “ 𝐴 ) )
18 fvres ⊢ ( 𝑧 ∈ 𝐴 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑧 ) = ( 𝐹 ‘ 𝑧 ) )
19 fvres ⊢ ( 𝑤 ∈ 𝐴 → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) )
20 18 19 eqeqan12d ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑧 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) )
21 20 adantl ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑧 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) )
22 simprl ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → 𝑧 ∈ 𝐴 )
23 simprr ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → 𝑤 ∈ 𝐴 )
24 simpl3 ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) )
25 breq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 𝑅 𝑦 ↔ 𝑧 𝑅 𝑦 ) )
26 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
27 26 breq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) )
28 25 27 imbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑧 𝑅 𝑦 → ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) )
29 breq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑧 𝑅 𝑦 ↔ 𝑧 𝑅 𝑤 ) )
30 fveq2 ⊢ ( 𝑦 = 𝑤 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑤 ) )
31 30 breq2d ⊢ ( 𝑦 = 𝑤 → ( ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ 𝑤 ) ) )
32 29 31 imbi12d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑧 𝑅 𝑦 → ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑧 𝑅 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ 𝑤 ) ) ) )
33 28 32 rspc2va ⊢ ( ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝑧 𝑅 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ 𝑤 ) ) )
34 22 23 24 33 syl21anc ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝑧 𝑅 𝑤 → ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ 𝑤 ) ) )
35 breq1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 𝑅 𝑦 ↔ 𝑤 𝑅 𝑦 ) )
36 fveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑤 ) )
37 36 breq1d ⊢ ( 𝑥 = 𝑤 → ( ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) )
38 35 37 imbi12d ⊢ ( 𝑥 = 𝑤 → ( ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑤 𝑅 𝑦 → ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) )
39 breq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑤 𝑅 𝑦 ↔ 𝑤 𝑅 𝑧 ) )
40 fveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) )
41 40 breq2d ⊢ ( 𝑦 = 𝑧 → ( ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑧 ) ) )
42 39 41 imbi12d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑤 𝑅 𝑦 → ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑤 𝑅 𝑧 → ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑧 ) ) ) )
43 38 42 rspc2va ⊢ ( ( ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝑤 𝑅 𝑧 → ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑧 ) ) )
44 23 22 24 43 syl21anc ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝑤 𝑅 𝑧 → ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑧 ) ) )
45 34 44 orim12d ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( 𝑧 𝑅 𝑤 ∨ 𝑤 𝑅 𝑧 ) → ( ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ 𝑤 ) ∨ ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑧 ) ) ) )
46 45 con3d ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ¬ ( ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ 𝑤 ) ∨ ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑧 ) ) → ¬ ( 𝑧 𝑅 𝑤 ∨ 𝑤 𝑅 𝑧 ) ) )
47 simpl1r ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → 𝑆 Or 𝐶 )
48 simpl2l ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → 𝐹 : 𝐵 ⟶ 𝐶 )
49 simpl2r ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → 𝐴 ⊆ 𝐵 )
50 49 22 sseldd ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → 𝑧 ∈ 𝐵 )
51 48 50 ffvelcdmd ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝐶 )
52 49 23 sseldd ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → 𝑤 ∈ 𝐵 )
53 48 52 ffvelcdmd ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝐶 )
54 sotrieq ⊢ ( ( 𝑆 Or 𝐶 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝐶 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ¬ ( ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ 𝑤 ) ∨ ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑧 ) ) ) )
55 47 51 53 54 syl12anc ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ¬ ( ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ 𝑤 ) ∨ ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑧 ) ) ) )
56 simpl1l ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → 𝑅 Or 𝐵 )
57 sotrieq ⊢ ( ( 𝑅 Or 𝐵 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑧 = 𝑤 ↔ ¬ ( 𝑧 𝑅 𝑤 ∨ 𝑤 𝑅 𝑧 ) ) )
58 56 50 52 57 syl12anc ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝑧 = 𝑤 ↔ ¬ ( 𝑧 𝑅 𝑤 ∨ 𝑤 𝑅 𝑧 ) ) )
59 46 55 58 3imtr4d ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
60 21 59 sylbid ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑧 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
61 60 ralrimivva ⊢ ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) → ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑧 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑤 ) → 𝑧 = 𝑤 ) )
62 dff1o6 ⊢ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1-onto→ ( 𝐹 “ 𝐴 ) ↔ ( ( 𝐹 ↾ 𝐴 ) Fn 𝐴 ∧ ran ( 𝐹 ↾ 𝐴 ) = ( 𝐹 “ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑧 ) = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑤 ) → 𝑧 = 𝑤 ) ) )
63 14 17 61 62 syl3anbrc ⊢ ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1-onto→ ( 𝐹 “ 𝐴 ) )
64 fveq2 ⊢ ( 𝑧 = 𝑤 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) )
65 64 a1i ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝑧 = 𝑤 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ) )
66 65 44 orim12d ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( 𝑧 = 𝑤 ∨ 𝑤 𝑅 𝑧 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ∨ ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑧 ) ) ) )
67 66 con3d ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ¬ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ∨ ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑧 ) ) → ¬ ( 𝑧 = 𝑤 ∨ 𝑤 𝑅 𝑧 ) ) )
68 sotric ⊢ ( ( 𝑆 Or 𝐶 ∧ ( ( 𝐹 ‘ 𝑧 ) ∈ 𝐶 ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝐶 ) ) → ( ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ 𝑤 ) ↔ ¬ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ∨ ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑧 ) ) ) )
69 47 51 53 68 syl12anc ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ 𝑤 ) ↔ ¬ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ∨ ( 𝐹 ‘ 𝑤 ) 𝑆 ( 𝐹 ‘ 𝑧 ) ) ) )
70 sotric ⊢ ( ( 𝑅 Or 𝐵 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵 ) ) → ( 𝑧 𝑅 𝑤 ↔ ¬ ( 𝑧 = 𝑤 ∨ 𝑤 𝑅 𝑧 ) ) )
71 56 50 52 70 syl12anc ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝑧 𝑅 𝑤 ↔ ¬ ( 𝑧 = 𝑤 ∨ 𝑤 𝑅 𝑧 ) ) )
72 67 69 71 3imtr4d ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ 𝑤 ) → 𝑧 𝑅 𝑤 ) )
73 34 72 impbid ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝑧 𝑅 𝑤 ↔ ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ 𝑤 ) ) )
74 18 19 breqan12d ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑧 ) 𝑆 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ 𝑤 ) ) )
75 74 adantl ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑧 ) 𝑆 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑧 ) 𝑆 ( 𝐹 ‘ 𝑤 ) ) )
76 73 75 bitr4d ⊢ ( ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ) → ( 𝑧 𝑅 𝑤 ↔ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑧 ) 𝑆 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑤 ) ) )
77 76 ralrimivva ⊢ ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) → ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 ↔ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑧 ) 𝑆 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑤 ) ) )
78 df-isom ⊢ ( ( 𝐹 ↾ 𝐴 ) Isom 𝑅 , 𝑆 ( 𝐴 , ( 𝐹 “ 𝐴 ) ) ↔ ( ( 𝐹 ↾ 𝐴 ) : 𝐴 –1-1-onto→ ( 𝐹 “ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑤 ∈ 𝐴 ( 𝑧 𝑅 𝑤 ↔ ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑧 ) 𝑆 ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑤 ) ) ) )
79 63 77 78 sylanbrc ⊢ ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ↾ 𝐴 ) Isom 𝑅 , 𝑆 ( 𝐴 , ( 𝐹 “ 𝐴 ) ) )
80 79 3expia ⊢ ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) → ( 𝐹 ↾ 𝐴 ) Isom 𝑅 , 𝑆 ( 𝐴 , ( 𝐹 “ 𝐴 ) ) ) )
81 8 80 impbid2 ⊢ ( ( ( 𝑅 Or 𝐵 ∧ 𝑆 Or 𝐶 ) ∧ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ 𝐴 ⊆ 𝐵 ) ) → ( ( 𝐹 ↾ 𝐴 ) Isom 𝑅 , 𝑆 ( 𝐴 , ( 𝐹 “ 𝐴 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 → ( 𝐹 ‘ 𝑥 ) 𝑆 ( 𝐹 ‘ 𝑦 ) ) ) )