Metamath Proof Explorer

Theorem isosolem

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

Ref Expression
Assertion isosolem ⊢ H Isom R , S A B → S Or B → R Or A

Proof

Step Hyp Ref Expression
1 isopolem ⊢ H Isom R , S A B → S Po B → R Po A
2 isof1o ⊢ H Isom R , S A B → H : A ⟶ 1-1 onto B
3 f1of ⊢ H : A ⟶ 1-1 onto B → H : A ⟶ B
4 ffvelcdm ⊢ H : A ⟶ B ∧ c ∈ A → H ⁡ c ∈ B
5 4 ex ⊢ H : A ⟶ B → c ∈ A → H ⁡ c ∈ B
6 ffvelcdm ⊢ H : A ⟶ B ∧ d ∈ A → H ⁡ d ∈ B
7 6 ex ⊢ H : A ⟶ B → d ∈ A → H ⁡ d ∈ B
8 5 7 anim12d ⊢ H : A ⟶ B → c ∈ A ∧ d ∈ A → H ⁡ c ∈ B ∧ H ⁡ d ∈ B
9 2 3 8 3syl ⊢ H Isom R , S A B → c ∈ A ∧ d ∈ A → H ⁡ c ∈ B ∧ H ⁡ d ∈ B
10 9 imp ⊢ H Isom R , S A B ∧ c ∈ A ∧ d ∈ A → H ⁡ c ∈ B ∧ H ⁡ d ∈ B
11 breq1 ⊢ a = H ⁡ c → a S b ↔ H ⁡ c S b
12 eqeq1 ⊢ a = H ⁡ c → a = b ↔ H ⁡ c = b
13 breq2 ⊢ a = H ⁡ c → b S a ↔ b S H ⁡ c
14 11 12 13 3orbi123d ⊢ a = H ⁡ c → a S b ∨ a = b ∨ b S a ↔ H ⁡ c S b ∨ H ⁡ c = b ∨ b S H ⁡ c
15 breq2 ⊢ b = H ⁡ d → H ⁡ c S b ↔ H ⁡ c S H ⁡ d
16 eqeq2 ⊢ b = H ⁡ d → H ⁡ c = b ↔ H ⁡ c = H ⁡ d
17 breq1 ⊢ b = H ⁡ d → b S H ⁡ c ↔ H ⁡ d S H ⁡ c
18 15 16 17 3orbi123d ⊢ b = H ⁡ d → H ⁡ c S b ∨ H ⁡ c = b ∨ b S H ⁡ c ↔ H ⁡ c S H ⁡ d ∨ H ⁡ c = H ⁡ d ∨ H ⁡ d S H ⁡ c
19 14 18 rspc2v ⊢ H ⁡ c ∈ B ∧ H ⁡ d ∈ B → ∀ a ∈ B ∀ b ∈ B a S b ∨ a = b ∨ b S a → H ⁡ c S H ⁡ d ∨ H ⁡ c = H ⁡ d ∨ H ⁡ d S H ⁡ c
20 10 19 syl ⊢ H Isom R , S A B ∧ c ∈ A ∧ d ∈ A → ∀ a ∈ B ∀ b ∈ B a S b ∨ a = b ∨ b S a → H ⁡ c S H ⁡ d ∨ H ⁡ c = H ⁡ d ∨ H ⁡ d S H ⁡ c
21 isorel ⊢ H Isom R , S A B ∧ c ∈ A ∧ d ∈ A → c R d ↔ H ⁡ c S H ⁡ d
22 f1of1 ⊢ H : A ⟶ 1-1 onto B → H : A ⟶ 1-1 B
23 2 22 syl ⊢ H Isom R , S A B → H : A ⟶ 1-1 B
24 f1fveq ⊢ H : A ⟶ 1-1 B ∧ c ∈ A ∧ d ∈ A → H ⁡ c = H ⁡ d ↔ c = d
25 23 24 sylan ⊢ H Isom R , S A B ∧ c ∈ A ∧ d ∈ A → H ⁡ c = H ⁡ d ↔ c = d
26 25 bicomd ⊢ H Isom R , S A B ∧ c ∈ A ∧ d ∈ A → c = d ↔ H ⁡ c = H ⁡ d
27 isorel ⊢ H Isom R , S A B ∧ d ∈ A ∧ c ∈ A → d R c ↔ H ⁡ d S H ⁡ c
28 27 ancom2s ⊢ H Isom R , S A B ∧ c ∈ A ∧ d ∈ A → d R c ↔ H ⁡ d S H ⁡ c
29 21 26 28 3orbi123d ⊢ H Isom R , S A B ∧ c ∈ A ∧ d ∈ A → c R d ∨ c = d ∨ d R c ↔ H ⁡ c S H ⁡ d ∨ H ⁡ c = H ⁡ d ∨ H ⁡ d S H ⁡ c
30 20 29 sylibrd ⊢ H Isom R , S A B ∧ c ∈ A ∧ d ∈ A → ∀ a ∈ B ∀ b ∈ B a S b ∨ a = b ∨ b S a → c R d ∨ c = d ∨ d R c
31 30 ralrimdvva ⊢ H Isom R , S A B → ∀ a ∈ B ∀ b ∈ B a S b ∨ a = b ∨ b S a → ∀ c ∈ A ∀ d ∈ A c R d ∨ c = d ∨ d R c
32 1 31 anim12d ⊢ H Isom R , S A B → S Po B ∧ ∀ a ∈ B ∀ b ∈ B a S b ∨ a = b ∨ b S a → R Po A ∧ ∀ c ∈ A ∀ d ∈ A c R d ∨ c = d ∨ d R c
33 df-so ⊢ S Or B ↔ S Po B ∧ ∀ a ∈ B ∀ b ∈ B a S b ∨ a = b ∨ b S a
34 df-so ⊢ R Or A ↔ R Po A ∧ ∀ c ∈ A ∀ d ∈ A c R d ∨ c = d ∨ d R c
35 32 33 34 3imtr4g ⊢ H Isom R , S A B → S Or B → R Or A