Theorem soisoi 6478

Description: Infer isomorphism from one direction of an order proof for isomorphisms between strict orders. (Contributed by Stefan O'Rear, 2-Nov-2014.)

Assertion

Ref	Expression
soisoi	⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵))

Distinct variable groups:   𝑥,𝑅,𝑦   𝑥,𝑆,𝑦   𝑥,𝐻,𝑦   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦

Proof of Theorem soisoi

Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simprl 790	. . . . 5 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻:𝐴–onto→𝐵)
2		fof 6028	. . . . 5 ⊢ (𝐻:𝐴–onto→𝐵 → 𝐻:𝐴⟶𝐵)
3	1, 2	syl 17	. . . 4 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻:𝐴⟶𝐵)
4		simpll 786	. . . . . . . 8 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝑅 Or 𝐴)
5		sotrieq 4986	. . . . . . . . 9 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎 = 𝑏 ↔ ¬ (𝑎𝑅𝑏 ∨ 𝑏𝑅𝑎)))
6	5	con2bid 343	. . . . . . . 8 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎𝑅𝑏 ∨ 𝑏𝑅𝑎) ↔ ¬ 𝑎 = 𝑏))
7	4, 6	sylan 487	. . . . . . 7 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎𝑅𝑏 ∨ 𝑏𝑅𝑎) ↔ ¬ 𝑎 = 𝑏))
8		simprr 792	. . . . . . . . . 10 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
9		breq1 4586	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑎 → (𝑥𝑅𝑦 ↔ 𝑎𝑅𝑦))
10		fveq2 6103	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑎 → (𝐻‘𝑥) = (𝐻‘𝑎))
11	10	breq1d 4593	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑎 → ((𝐻‘𝑥)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑦)))
12	9, 11	imbi12d 333	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑎 → ((𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ (𝑎𝑅𝑦 → (𝐻‘𝑎)𝑆(𝐻‘𝑦))))
13		breq2 4587	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑏 → (𝑎𝑅𝑦 ↔ 𝑎𝑅𝑏))
14		fveq2 6103	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑏 → (𝐻‘𝑦) = (𝐻‘𝑏))
15	14	breq2d 4595	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑏 → ((𝐻‘𝑎)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
16	13, 15	imbi12d 333	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → ((𝑎𝑅𝑦 → (𝐻‘𝑎)𝑆(𝐻‘𝑦)) ↔ (𝑎𝑅𝑏 → (𝐻‘𝑎)𝑆(𝐻‘𝑏))))
17	12, 16	rspc2va 3294	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦))) → (𝑎𝑅𝑏 → (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
18	17	ancoms 468	. . . . . . . . . 10 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎𝑅𝑏 → (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
19	8, 18	sylan 487	. . . . . . . . 9 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎𝑅𝑏 → (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
20		simpllr 795	. . . . . . . . . . 11 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑆 Po 𝐵)
21		simplrl 796	. . . . . . . . . . . . 13 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝐻:𝐴–onto→𝐵)
22	21, 2	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝐻:𝐴⟶𝐵)
23		simprr 792	. . . . . . . . . . . 12 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑏 ∈ 𝐴)
24	22, 23	ffvelrnd 6268	. . . . . . . . . . 11 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝐻‘𝑏) ∈ 𝐵)
25		poirr 4970	. . . . . . . . . . . 12 ⊢ ((𝑆 Po 𝐵 ∧ (𝐻‘𝑏) ∈ 𝐵) → ¬ (𝐻‘𝑏)𝑆(𝐻‘𝑏))
26		breq1 4586	. . . . . . . . . . . . 13 ⊢ ((𝐻‘𝑎) = (𝐻‘𝑏) → ((𝐻‘𝑎)𝑆(𝐻‘𝑏) ↔ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
27	26	notbid 307	. . . . . . . . . . . 12 ⊢ ((𝐻‘𝑎) = (𝐻‘𝑏) → (¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏) ↔ ¬ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
28	25, 27	syl5ibrcom 236	. . . . . . . . . . 11 ⊢ ((𝑆 Po 𝐵 ∧ (𝐻‘𝑏) ∈ 𝐵) → ((𝐻‘𝑎) = (𝐻‘𝑏) → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
29	20, 24, 28	syl2anc 691	. . . . . . . . . 10 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐻‘𝑎) = (𝐻‘𝑏) → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
30	29	con2d 128	. . . . . . . . 9 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐻‘𝑎)𝑆(𝐻‘𝑏) → ¬ (𝐻‘𝑎) = (𝐻‘𝑏)))
31	19, 30	syld 46	. . . . . . . 8 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎𝑅𝑏 → ¬ (𝐻‘𝑎) = (𝐻‘𝑏)))
32		breq1 4586	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑏 → (𝑥𝑅𝑦 ↔ 𝑏𝑅𝑦))
33		fveq2 6103	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑏 → (𝐻‘𝑥) = (𝐻‘𝑏))
34	33	breq1d 4593	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑏 → ((𝐻‘𝑥)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝑏)𝑆(𝐻‘𝑦)))
35	32, 34	imbi12d 333	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑏 → ((𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ (𝑏𝑅𝑦 → (𝐻‘𝑏)𝑆(𝐻‘𝑦))))
36		breq2 4587	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑎 → (𝑏𝑅𝑦 ↔ 𝑏𝑅𝑎))
37		fveq2 6103	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑎 → (𝐻‘𝑦) = (𝐻‘𝑎))
38	37	breq2d 4595	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑎 → ((𝐻‘𝑏)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
39	36, 38	imbi12d 333	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑎 → ((𝑏𝑅𝑦 → (𝐻‘𝑏)𝑆(𝐻‘𝑦)) ↔ (𝑏𝑅𝑎 → (𝐻‘𝑏)𝑆(𝐻‘𝑎))))
40	35, 39	rspc2va 3294	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦))) → (𝑏𝑅𝑎 → (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
41	40	ancoms 468	. . . . . . . . . . 11 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ∧ (𝑏 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴)) → (𝑏𝑅𝑎 → (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
42	41	ancom2s 840	. . . . . . . . . 10 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑏𝑅𝑎 → (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
43	8, 42	sylan 487	. . . . . . . . 9 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑏𝑅𝑎 → (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
44		breq2 4587	. . . . . . . . . . . . 13 ⊢ ((𝐻‘𝑎) = (𝐻‘𝑏) → ((𝐻‘𝑏)𝑆(𝐻‘𝑎) ↔ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
45	44	notbid 307	. . . . . . . . . . . 12 ⊢ ((𝐻‘𝑎) = (𝐻‘𝑏) → (¬ (𝐻‘𝑏)𝑆(𝐻‘𝑎) ↔ ¬ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
46	25, 45	syl5ibrcom 236	. . . . . . . . . . 11 ⊢ ((𝑆 Po 𝐵 ∧ (𝐻‘𝑏) ∈ 𝐵) → ((𝐻‘𝑎) = (𝐻‘𝑏) → ¬ (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
47	20, 24, 46	syl2anc 691	. . . . . . . . . 10 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐻‘𝑎) = (𝐻‘𝑏) → ¬ (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
48	47	con2d 128	. . . . . . . . 9 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐻‘𝑏)𝑆(𝐻‘𝑎) → ¬ (𝐻‘𝑎) = (𝐻‘𝑏)))
49	43, 48	syld 46	. . . . . . . 8 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑏𝑅𝑎 → ¬ (𝐻‘𝑎) = (𝐻‘𝑏)))
50	31, 49	jaod 394	. . . . . . 7 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎𝑅𝑏 ∨ 𝑏𝑅𝑎) → ¬ (𝐻‘𝑎) = (𝐻‘𝑏)))
51	7, 50	sylbird 249	. . . . . 6 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (¬ 𝑎 = 𝑏 → ¬ (𝐻‘𝑎) = (𝐻‘𝑏)))
52	51	con4d 113	. . . . 5 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐻‘𝑎) = (𝐻‘𝑏) → 𝑎 = 𝑏))
53	52	ralrimivva 2954	. . . 4 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ((𝐻‘𝑎) = (𝐻‘𝑏) → 𝑎 = 𝑏))
54		dff13 6416	. . . 4 ⊢ (𝐻:𝐴–1-1→𝐵 ↔ (𝐻:𝐴⟶𝐵 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ((𝐻‘𝑎) = (𝐻‘𝑏) → 𝑎 = 𝑏)))
55	3, 53, 54	sylanbrc 695	. . 3 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻:𝐴–1-1→𝐵)
56		df-f1o 5811	. . 3 ⊢ (𝐻:𝐴–1-1-onto→𝐵 ↔ (𝐻:𝐴–1-1→𝐵 ∧ 𝐻:𝐴–onto→𝐵))
57	55, 1, 56	sylanbrc 695	. 2 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻:𝐴–1-1-onto→𝐵)
58		sotric 4985	. . . . . . 7 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎𝑅𝑏 ↔ ¬ (𝑎 = 𝑏 ∨ 𝑏𝑅𝑎)))
59	58	con2bid 343	. . . . . 6 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎 = 𝑏 ∨ 𝑏𝑅𝑎) ↔ ¬ 𝑎𝑅𝑏))
60	4, 59	sylan 487	. . . . 5 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎 = 𝑏 ∨ 𝑏𝑅𝑎) ↔ ¬ 𝑎𝑅𝑏))
61		fveq2 6103	. . . . . . . . . 10 ⊢ (𝑎 = 𝑏 → (𝐻‘𝑎) = (𝐻‘𝑏))
62	61	breq1d 4593	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → ((𝐻‘𝑎)𝑆(𝐻‘𝑏) ↔ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
63	62	notbid 307	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏) ↔ ¬ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
64	25, 63	syl5ibrcom 236	. . . . . . 7 ⊢ ((𝑆 Po 𝐵 ∧ (𝐻‘𝑏) ∈ 𝐵) → (𝑎 = 𝑏 → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
65	20, 24, 64	syl2anc 691	. . . . . 6 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎 = 𝑏 → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
66		simprl 790	. . . . . . . . 9 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑎 ∈ 𝐴)
67	22, 66	ffvelrnd 6268	. . . . . . . 8 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝐻‘𝑎) ∈ 𝐵)
68		po2nr 4972	. . . . . . . . 9 ⊢ ((𝑆 Po 𝐵 ∧ ((𝐻‘𝑏) ∈ 𝐵 ∧ (𝐻‘𝑎) ∈ 𝐵)) → ¬ ((𝐻‘𝑏)𝑆(𝐻‘𝑎) ∧ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
69		imnan 437	. . . . . . . . 9 ⊢ (((𝐻‘𝑏)𝑆(𝐻‘𝑎) → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)) ↔ ¬ ((𝐻‘𝑏)𝑆(𝐻‘𝑎) ∧ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
70	68, 69	sylibr 223	. . . . . . . 8 ⊢ ((𝑆 Po 𝐵 ∧ ((𝐻‘𝑏) ∈ 𝐵 ∧ (𝐻‘𝑎) ∈ 𝐵)) → ((𝐻‘𝑏)𝑆(𝐻‘𝑎) → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
71	20, 24, 67, 70	syl12anc 1316	. . . . . . 7 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐻‘𝑏)𝑆(𝐻‘𝑎) → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
72	43, 71	syld 46	. . . . . 6 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑏𝑅𝑎 → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
73	65, 72	jaod 394	. . . . 5 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎 = 𝑏 ∨ 𝑏𝑅𝑎) → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
74	60, 73	sylbird 249	. . . 4 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (¬ 𝑎𝑅𝑏 → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
75	19, 74	impcon4bid 216	. . 3 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎𝑅𝑏 ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
76	75	ralrimivva 2954	. 2 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎𝑅𝑏 ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
77		df-isom 5813	. 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎𝑅𝑏 ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏))))
78	57, 76, 77	sylanbrc 695	1 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896   class class class wbr 4583   Po wpo 4957   Or wor 4958  ⟶wf 5800  –1-1→wf1 5801  –onto→wfo 5802  –1-1-onto→wf1o 5803  ‘cfv 5804   Isom wiso 5805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-id 4953  df-po 4959  df-so 4960  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813

This theorem is referenced by:  ordtypelem8  8313  cantnf  8473  fin23lem27  9033  iccpnfhmeo  22552  xrhmeo  22553  logccv  24209  xrge0iifiso  29309