Metamath Proof Explorer

Theorem isopolem

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

Ref Expression
Assertion isopolem ⊢ H Isom R , S A B → S Po B → R Po A

Proof

Step Hyp Ref Expression
1 isof1o ⊢ H Isom R , S A B → H : A ⟶ 1-1 onto B
2 f1of ⊢ H : A ⟶ 1-1 onto B → H : A ⟶ B
3 ffvelrn ⊢ H : A ⟶ B ∧ d ∈ A → H ⁡ d ∈ B
4 3 ex ⊢ H : A ⟶ B → d ∈ A → H ⁡ d ∈ B
5 ffvelrn ⊢ H : A ⟶ B ∧ e ∈ A → H ⁡ e ∈ B
6 5 ex ⊢ H : A ⟶ B → e ∈ A → H ⁡ e ∈ B
7 ffvelrn ⊢ H : A ⟶ B ∧ f ∈ A → H ⁡ f ∈ B
8 7 ex ⊢ H : A ⟶ B → f ∈ A → H ⁡ f ∈ B
9 4 6 8 3anim123d ⊢ H : A ⟶ B → d ∈ A ∧ e ∈ A ∧ f ∈ A → H ⁡ d ∈ B ∧ H ⁡ e ∈ B ∧ H ⁡ f ∈ B
10 1 2 9 3syl ⊢ H Isom R , S A B → d ∈ A ∧ e ∈ A ∧ f ∈ A → H ⁡ d ∈ B ∧ H ⁡ e ∈ B ∧ H ⁡ f ∈ B
11 10 imp ⊢ H Isom R , S A B ∧ d ∈ A ∧ e ∈ A ∧ f ∈ A → H ⁡ d ∈ B ∧ H ⁡ e ∈ B ∧ H ⁡ f ∈ B
12 breq12 ⊢ a = H ⁡ d ∧ a = H ⁡ d → a S a ↔ H ⁡ d S H ⁡ d
13 12 anidms ⊢ a = H ⁡ d → a S a ↔ H ⁡ d S H ⁡ d
14 13 notbid ⊢ a = H ⁡ d → ¬ a S a ↔ ¬ H ⁡ d S H ⁡ d
15 breq1 ⊢ a = H ⁡ d → a S b ↔ H ⁡ d S b
16 15 anbi1d ⊢ a = H ⁡ d → a S b ∧ b S c ↔ H ⁡ d S b ∧ b S c
17 breq1 ⊢ a = H ⁡ d → a S c ↔ H ⁡ d S c
18 16 17 imbi12d ⊢ a = H ⁡ d → a S b ∧ b S c → a S c ↔ H ⁡ d S b ∧ b S c → H ⁡ d S c
19 14 18 anbi12d ⊢ a = H ⁡ d → ¬ a S a ∧ a S b ∧ b S c → a S c ↔ ¬ H ⁡ d S H ⁡ d ∧ H ⁡ d S b ∧ b S c → H ⁡ d S c
20 breq2 ⊢ b = H ⁡ e → H ⁡ d S b ↔ H ⁡ d S H ⁡ e
21 breq1 ⊢ b = H ⁡ e → b S c ↔ H ⁡ e S c
22 20 21 anbi12d ⊢ b = H ⁡ e → H ⁡ d S b ∧ b S c ↔ H ⁡ d S H ⁡ e ∧ H ⁡ e S c
23 22 imbi1d ⊢ b = H ⁡ e → H ⁡ d S b ∧ b S c → H ⁡ d S c ↔ H ⁡ d S H ⁡ e ∧ H ⁡ e S c → H ⁡ d S c
24 23 anbi2d ⊢ b = H ⁡ e → ¬ H ⁡ d S H ⁡ d ∧ H ⁡ d S b ∧ b S c → H ⁡ d S c ↔ ¬ H ⁡ d S H ⁡ d ∧ H ⁡ d S H ⁡ e ∧ H ⁡ e S c → H ⁡ d S c
25 breq2 ⊢ c = H ⁡ f → H ⁡ e S c ↔ H ⁡ e S H ⁡ f
26 25 anbi2d ⊢ c = H ⁡ f → H ⁡ d S H ⁡ e ∧ H ⁡ e S c ↔ H ⁡ d S H ⁡ e ∧ H ⁡ e S H ⁡ f
27 breq2 ⊢ c = H ⁡ f → H ⁡ d S c ↔ H ⁡ d S H ⁡ f
28 26 27 imbi12d ⊢ c = H ⁡ f → H ⁡ d S H ⁡ e ∧ H ⁡ e S c → H ⁡ d S c ↔ H ⁡ d S H ⁡ e ∧ H ⁡ e S H ⁡ f → H ⁡ d S H ⁡ f
29 28 anbi2d ⊢ c = H ⁡ f → ¬ H ⁡ d S H ⁡ d ∧ H ⁡ d S H ⁡ e ∧ H ⁡ e S c → H ⁡ d S c ↔ ¬ H ⁡ d S H ⁡ d ∧ H ⁡ d S H ⁡ e ∧ H ⁡ e S H ⁡ f → H ⁡ d S H ⁡ f
30 19 24 29 rspc3v ⊢ H ⁡ d ∈ B ∧ H ⁡ e ∈ B ∧ H ⁡ f ∈ B → ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B ¬ a S a ∧ a S b ∧ b S c → a S c → ¬ H ⁡ d S H ⁡ d ∧ H ⁡ d S H ⁡ e ∧ H ⁡ e S H ⁡ f → H ⁡ d S H ⁡ f
31 11 30 syl ⊢ H Isom R , S A B ∧ d ∈ A ∧ e ∈ A ∧ f ∈ A → ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B ¬ a S a ∧ a S b ∧ b S c → a S c → ¬ H ⁡ d S H ⁡ d ∧ H ⁡ d S H ⁡ e ∧ H ⁡ e S H ⁡ f → H ⁡ d S H ⁡ f
32 simpl ⊢ H Isom R , S A B ∧ d ∈ A ∧ e ∈ A ∧ f ∈ A → H Isom R , S A B
33 simpr1 ⊢ H Isom R , S A B ∧ d ∈ A ∧ e ∈ A ∧ f ∈ A → d ∈ A
34 isorel ⊢ H Isom R , S A B ∧ d ∈ A ∧ d ∈ A → d R d ↔ H ⁡ d S H ⁡ d
35 32 33 33 34 syl12anc ⊢ H Isom R , S A B ∧ d ∈ A ∧ e ∈ A ∧ f ∈ A → d R d ↔ H ⁡ d S H ⁡ d
36 35 notbid ⊢ H Isom R , S A B ∧ d ∈ A ∧ e ∈ A ∧ f ∈ A → ¬ d R d ↔ ¬ H ⁡ d S H ⁡ d
37 simpr2 ⊢ H Isom R , S A B ∧ d ∈ A ∧ e ∈ A ∧ f ∈ A → e ∈ A
38 isorel ⊢ H Isom R , S A B ∧ d ∈ A ∧ e ∈ A → d R e ↔ H ⁡ d S H ⁡ e
39 32 33 37 38 syl12anc ⊢ H Isom R , S A B ∧ d ∈ A ∧ e ∈ A ∧ f ∈ A → d R e ↔ H ⁡ d S H ⁡ e
40 simpr3 ⊢ H Isom R , S A B ∧ d ∈ A ∧ e ∈ A ∧ f ∈ A → f ∈ A
41 isorel ⊢ H Isom R , S A B ∧ e ∈ A ∧ f ∈ A → e R f ↔ H ⁡ e S H ⁡ f
42 32 37 40 41 syl12anc ⊢ H Isom R , S A B ∧ d ∈ A ∧ e ∈ A ∧ f ∈ A → e R f ↔ H ⁡ e S H ⁡ f
43 39 42 anbi12d ⊢ H Isom R , S A B ∧ d ∈ A ∧ e ∈ A ∧ f ∈ A → d R e ∧ e R f ↔ H ⁡ d S H ⁡ e ∧ H ⁡ e S H ⁡ f
44 isorel ⊢ H Isom R , S A B ∧ d ∈ A ∧ f ∈ A → d R f ↔ H ⁡ d S H ⁡ f
45 32 33 40 44 syl12anc ⊢ H Isom R , S A B ∧ d ∈ A ∧ e ∈ A ∧ f ∈ A → d R f ↔ H ⁡ d S H ⁡ f
46 43 45 imbi12d ⊢ H Isom R , S A B ∧ d ∈ A ∧ e ∈ A ∧ f ∈ A → d R e ∧ e R f → d R f ↔ H ⁡ d S H ⁡ e ∧ H ⁡ e S H ⁡ f → H ⁡ d S H ⁡ f
47 36 46 anbi12d ⊢ H Isom R , S A B ∧ d ∈ A ∧ e ∈ A ∧ f ∈ A → ¬ d R d ∧ d R e ∧ e R f → d R f ↔ ¬ H ⁡ d S H ⁡ d ∧ H ⁡ d S H ⁡ e ∧ H ⁡ e S H ⁡ f → H ⁡ d S H ⁡ f
48 31 47 sylibrd ⊢ H Isom R , S A B ∧ d ∈ A ∧ e ∈ A ∧ f ∈ A → ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B ¬ a S a ∧ a S b ∧ b S c → a S c → ¬ d R d ∧ d R e ∧ e R f → d R f
49 48 ex ⊢ H Isom R , S A B → d ∈ A ∧ e ∈ A ∧ f ∈ A → ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B ¬ a S a ∧ a S b ∧ b S c → a S c → ¬ d R d ∧ d R e ∧ e R f → d R f
50 49 com23 ⊢ H Isom R , S A B → ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B ¬ a S a ∧ a S b ∧ b S c → a S c → d ∈ A ∧ e ∈ A ∧ f ∈ A → ¬ d R d ∧ d R e ∧ e R f → d R f
51 50 imp31 ⊢ H Isom R , S A B ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B ¬ a S a ∧ a S b ∧ b S c → a S c ∧ d ∈ A ∧ e ∈ A ∧ f ∈ A → ¬ d R d ∧ d R e ∧ e R f → d R f
52 51 ralrimivvva ⊢ H Isom R , S A B ∧ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B ¬ a S a ∧ a S b ∧ b S c → a S c → ∀ d ∈ A ∀ e ∈ A ∀ f ∈ A ¬ d R d ∧ d R e ∧ e R f → d R f
53 52 ex ⊢ H Isom R , S A B → ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B ¬ a S a ∧ a S b ∧ b S c → a S c → ∀ d ∈ A ∀ e ∈ A ∀ f ∈ A ¬ d R d ∧ d R e ∧ e R f → d R f
54 df-po ⊢ S Po B ↔ ∀ a ∈ B ∀ b ∈ B ∀ c ∈ B ¬ a S a ∧ a S b ∧ b S c → a S c
55 df-po ⊢ R Po A ↔ ∀ d ∈ A ∀ e ∈ A ∀ f ∈ A ¬ d R d ∧ d R e ∧ e R f → d R f
56 53 54 55 3imtr4g ⊢ H Isom R , S A B → S Po B → R Po A