Theorem soisoi 7199

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 768	. . . . 5 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻:𝐴–onto→𝐵)
2		fof 6688	. . . . 5 ⊢ (𝐻:𝐴–onto→𝐵 → 𝐻:𝐴⟶𝐵)
3	1, 2	syl 17	. . . 4 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻:𝐴⟶𝐵)
4		sotrieq 5532	. . . . . . . . 9 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎 = 𝑏 ↔ ¬ (𝑎𝑅𝑏 ∨ 𝑏𝑅𝑎)))
5	4	con2bid 355	. . . . . . . 8 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎𝑅𝑏 ∨ 𝑏𝑅𝑎) ↔ ¬ 𝑎 = 𝑏))
6	5	ad4ant14 749	. . . . . . 7 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎𝑅𝑏 ∨ 𝑏𝑅𝑎) ↔ ¬ 𝑎 = 𝑏))
7		simprr 770	. . . . . . . . . 10 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
8		breq1 5077	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑎 → (𝑥𝑅𝑦 ↔ 𝑎𝑅𝑦))
9		fveq2 6774	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑎 → (𝐻‘𝑥) = (𝐻‘𝑎))
10	9	breq1d 5084	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑎 → ((𝐻‘𝑥)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑦)))
11	8, 10	imbi12d 345	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑎 → ((𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ (𝑎𝑅𝑦 → (𝐻‘𝑎)𝑆(𝐻‘𝑦))))
12		breq2 5078	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑏 → (𝑎𝑅𝑦 ↔ 𝑎𝑅𝑏))
13		fveq2 6774	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑏 → (𝐻‘𝑦) = (𝐻‘𝑏))
14	13	breq2d 5086	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑏 → ((𝐻‘𝑎)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
15	12, 14	imbi12d 345	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → ((𝑎𝑅𝑦 → (𝐻‘𝑎)𝑆(𝐻‘𝑦)) ↔ (𝑎𝑅𝑏 → (𝐻‘𝑎)𝑆(𝐻‘𝑏))))
16	11, 15	rspc2va 3571	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦))) → (𝑎𝑅𝑏 → (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
17	16	ancoms 459	. . . . . . . . . 10 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎𝑅𝑏 → (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
18	7, 17	sylan 580	. . . . . . . . 9 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎𝑅𝑏 → (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
19		simpllr 773	. . . . . . . . . . 11 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑆 Po 𝐵)
20		simplrl 774	. . . . . . . . . . . . 13 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝐻:𝐴–onto→𝐵)
21	20, 2	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝐻:𝐴⟶𝐵)
22		simprr 770	. . . . . . . . . . . 12 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑏 ∈ 𝐴)
23	21, 22	ffvelrnd 6962	. . . . . . . . . . 11 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝐻‘𝑏) ∈ 𝐵)
24		poirr 5515	. . . . . . . . . . . 12 ⊢ ((𝑆 Po 𝐵 ∧ (𝐻‘𝑏) ∈ 𝐵) → ¬ (𝐻‘𝑏)𝑆(𝐻‘𝑏))
25		breq1 5077	. . . . . . . . . . . . 13 ⊢ ((𝐻‘𝑎) = (𝐻‘𝑏) → ((𝐻‘𝑎)𝑆(𝐻‘𝑏) ↔ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
26	25	notbid 318	. . . . . . . . . . . 12 ⊢ ((𝐻‘𝑎) = (𝐻‘𝑏) → (¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏) ↔ ¬ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
27	24, 26	syl5ibrcom 246	. . . . . . . . . . 11 ⊢ ((𝑆 Po 𝐵 ∧ (𝐻‘𝑏) ∈ 𝐵) → ((𝐻‘𝑎) = (𝐻‘𝑏) → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
28	19, 23, 27	syl2anc 584	. . . . . . . . . 10 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐻‘𝑎) = (𝐻‘𝑏) → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
29	28	con2d 134	. . . . . . . . 9 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐻‘𝑎)𝑆(𝐻‘𝑏) → ¬ (𝐻‘𝑎) = (𝐻‘𝑏)))
30	18, 29	syld 47	. . . . . . . 8 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎𝑅𝑏 → ¬ (𝐻‘𝑎) = (𝐻‘𝑏)))
31		breq1 5077	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑏 → (𝑥𝑅𝑦 ↔ 𝑏𝑅𝑦))
32		fveq2 6774	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑏 → (𝐻‘𝑥) = (𝐻‘𝑏))
33	32	breq1d 5084	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑏 → ((𝐻‘𝑥)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝑏)𝑆(𝐻‘𝑦)))
34	31, 33	imbi12d 345	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑏 → ((𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ (𝑏𝑅𝑦 → (𝐻‘𝑏)𝑆(𝐻‘𝑦))))
35		breq2 5078	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑎 → (𝑏𝑅𝑦 ↔ 𝑏𝑅𝑎))
36		fveq2 6774	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑎 → (𝐻‘𝑦) = (𝐻‘𝑎))
37	36	breq2d 5086	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑎 → ((𝐻‘𝑏)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
38	35, 37	imbi12d 345	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑎 → ((𝑏𝑅𝑦 → (𝐻‘𝑏)𝑆(𝐻‘𝑦)) ↔ (𝑏𝑅𝑎 → (𝐻‘𝑏)𝑆(𝐻‘𝑎))))
39	34, 38	rspc2va 3571	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦))) → (𝑏𝑅𝑎 → (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
40	39	ancoms 459	. . . . . . . . . . 11 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ∧ (𝑏 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴)) → (𝑏𝑅𝑎 → (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
41	40	ancom2s 647	. . . . . . . . . 10 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑏𝑅𝑎 → (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
42	7, 41	sylan 580	. . . . . . . . 9 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑏𝑅𝑎 → (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
43		breq2 5078	. . . . . . . . . . . . 13 ⊢ ((𝐻‘𝑎) = (𝐻‘𝑏) → ((𝐻‘𝑏)𝑆(𝐻‘𝑎) ↔ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
44	43	notbid 318	. . . . . . . . . . . 12 ⊢ ((𝐻‘𝑎) = (𝐻‘𝑏) → (¬ (𝐻‘𝑏)𝑆(𝐻‘𝑎) ↔ ¬ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
45	24, 44	syl5ibrcom 246	. . . . . . . . . . 11 ⊢ ((𝑆 Po 𝐵 ∧ (𝐻‘𝑏) ∈ 𝐵) → ((𝐻‘𝑎) = (𝐻‘𝑏) → ¬ (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
46	19, 23, 45	syl2anc 584	. . . . . . . . . 10 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐻‘𝑎) = (𝐻‘𝑏) → ¬ (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
47	46	con2d 134	. . . . . . . . 9 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐻‘𝑏)𝑆(𝐻‘𝑎) → ¬ (𝐻‘𝑎) = (𝐻‘𝑏)))
48	42, 47	syld 47	. . . . . . . 8 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑏𝑅𝑎 → ¬ (𝐻‘𝑎) = (𝐻‘𝑏)))
49	30, 48	jaod 856	. . . . . . 7 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎𝑅𝑏 ∨ 𝑏𝑅𝑎) → ¬ (𝐻‘𝑎) = (𝐻‘𝑏)))
50	6, 49	sylbird 259	. . . . . 6 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (¬ 𝑎 = 𝑏 → ¬ (𝐻‘𝑎) = (𝐻‘𝑏)))
51	50	con4d 115	. . . . 5 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐻‘𝑎) = (𝐻‘𝑏) → 𝑎 = 𝑏))
52	51	ralrimivva 3123	. . . 4 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ((𝐻‘𝑎) = (𝐻‘𝑏) → 𝑎 = 𝑏))
53		dff13 7128	. . . 4 ⊢ (𝐻:𝐴–1-1→𝐵 ↔ (𝐻:𝐴⟶𝐵 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ((𝐻‘𝑎) = (𝐻‘𝑏) → 𝑎 = 𝑏)))
54	3, 52, 53	sylanbrc 583	. . 3 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻:𝐴–1-1→𝐵)
55		df-f1o 6440	. . 3 ⊢ (𝐻:𝐴–1-1-onto→𝐵 ↔ (𝐻:𝐴–1-1→𝐵 ∧ 𝐻:𝐴–onto→𝐵))
56	54, 1, 55	sylanbrc 583	. 2 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻:𝐴–1-1-onto→𝐵)
57		sotric 5531	. . . . . . 7 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎𝑅𝑏 ↔ ¬ (𝑎 = 𝑏 ∨ 𝑏𝑅𝑎)))
58	57	con2bid 355	. . . . . 6 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎 = 𝑏 ∨ 𝑏𝑅𝑎) ↔ ¬ 𝑎𝑅𝑏))
59	58	ad4ant14 749	. . . . 5 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎 = 𝑏 ∨ 𝑏𝑅𝑎) ↔ ¬ 𝑎𝑅𝑏))
60		fveq2 6774	. . . . . . . . . 10 ⊢ (𝑎 = 𝑏 → (𝐻‘𝑎) = (𝐻‘𝑏))
61	60	breq1d 5084	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → ((𝐻‘𝑎)𝑆(𝐻‘𝑏) ↔ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
62	61	notbid 318	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏) ↔ ¬ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
63	24, 62	syl5ibrcom 246	. . . . . . 7 ⊢ ((𝑆 Po 𝐵 ∧ (𝐻‘𝑏) ∈ 𝐵) → (𝑎 = 𝑏 → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
64	19, 23, 63	syl2anc 584	. . . . . 6 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎 = 𝑏 → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
65		simprl 768	. . . . . . . . 9 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑎 ∈ 𝐴)
66	21, 65	ffvelrnd 6962	. . . . . . . 8 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝐻‘𝑎) ∈ 𝐵)
67		po2nr 5517	. . . . . . . . 9 ⊢ ((𝑆 Po 𝐵 ∧ ((𝐻‘𝑏) ∈ 𝐵 ∧ (𝐻‘𝑎) ∈ 𝐵)) → ¬ ((𝐻‘𝑏)𝑆(𝐻‘𝑎) ∧ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
68		imnan 400	. . . . . . . . 9 ⊢ (((𝐻‘𝑏)𝑆(𝐻‘𝑎) → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)) ↔ ¬ ((𝐻‘𝑏)𝑆(𝐻‘𝑎) ∧ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
69	67, 68	sylibr 233	. . . . . . . 8 ⊢ ((𝑆 Po 𝐵 ∧ ((𝐻‘𝑏) ∈ 𝐵 ∧ (𝐻‘𝑎) ∈ 𝐵)) → ((𝐻‘𝑏)𝑆(𝐻‘𝑎) → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
70	19, 23, 66, 69	syl12anc 834	. . . . . . 7 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐻‘𝑏)𝑆(𝐻‘𝑎) → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
71	42, 70	syld 47	. . . . . 6 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑏𝑅𝑎 → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
72	64, 71	jaod 856	. . . . 5 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎 = 𝑏 ∨ 𝑏𝑅𝑎) → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
73	59, 72	sylbird 259	. . . 4 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (¬ 𝑎𝑅𝑏 → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
74	18, 73	impcon4bid 226	. . 3 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎𝑅𝑏 ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
75	74	ralrimivva 3123	. 2 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎𝑅𝑏 ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
76		df-isom 6442	. 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎𝑅𝑏 ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏))))
77	56, 75, 76	sylanbrc 583	1 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844   = wceq 1539   ∈ wcel 2106  ∀wral 3064   class class class wbr 5074   Po wpo 5501   Or wor 5502  ⟶wf 6429  –1-1→wf1 6430  –onto→wfo 6431  –1-1-onto→wf1o 6432  ‘cfv 6433   Isom wiso 6434

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-id 5489  df-po 5503  df-so 5504  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442

This theorem is referenced by:  ordtypelem8  9284  cantnf  9451  fin23lem27  10084  iccpnfhmeo  24108  xrhmeo  24109  logccv  25818  xrge0iifiso  31885