Theorem soisoi 7325

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 770	. . . . 5 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻:𝐴–onto→𝐵)
2		fof 6806	. . . . 5 ⊢ (𝐻:𝐴–onto→𝐵 → 𝐻:𝐴⟶𝐵)
3	1, 2	syl 17	. . . 4 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻:𝐴⟶𝐵)
4		sotrieq 5618	. . . . . . . . 9 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎 = 𝑏 ↔ ¬ (𝑎𝑅𝑏 ∨ 𝑏𝑅𝑎)))
5	4	con2bid 355	. . . . . . . 8 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎𝑅𝑏 ∨ 𝑏𝑅𝑎) ↔ ¬ 𝑎 = 𝑏))
6	5	ad4ant14 751	. . . . . . 7 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎𝑅𝑏 ∨ 𝑏𝑅𝑎) ↔ ¬ 𝑎 = 𝑏))
7		simprr 772	. . . . . . . . . 10 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
8		breq1 5152	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑎 → (𝑥𝑅𝑦 ↔ 𝑎𝑅𝑦))
9		fveq2 6892	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑎 → (𝐻‘𝑥) = (𝐻‘𝑎))
10	9	breq1d 5159	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑎 → ((𝐻‘𝑥)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑦)))
11	8, 10	imbi12d 345	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑎 → ((𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ (𝑎𝑅𝑦 → (𝐻‘𝑎)𝑆(𝐻‘𝑦))))
12		breq2 5153	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑏 → (𝑎𝑅𝑦 ↔ 𝑎𝑅𝑏))
13		fveq2 6892	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑏 → (𝐻‘𝑦) = (𝐻‘𝑏))
14	13	breq2d 5161	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑏 → ((𝐻‘𝑎)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
15	12, 14	imbi12d 345	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → ((𝑎𝑅𝑦 → (𝐻‘𝑎)𝑆(𝐻‘𝑦)) ↔ (𝑎𝑅𝑏 → (𝐻‘𝑎)𝑆(𝐻‘𝑏))))
16	11, 15	rspc2va 3624	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦))) → (𝑎𝑅𝑏 → (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
17	16	ancoms 460	. . . . . . . . . 10 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎𝑅𝑏 → (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
18	7, 17	sylan 581	. . . . . . . . 9 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎𝑅𝑏 → (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
19		simpllr 775	. . . . . . . . . . 11 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑆 Po 𝐵)
20		simplrl 776	. . . . . . . . . . . . 13 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝐻:𝐴–onto→𝐵)
21	20, 2	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝐻:𝐴⟶𝐵)
22		simprr 772	. . . . . . . . . . . 12 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑏 ∈ 𝐴)
23	21, 22	ffvelcdmd 7088	. . . . . . . . . . 11 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝐻‘𝑏) ∈ 𝐵)
24		poirr 5601	. . . . . . . . . . . 12 ⊢ ((𝑆 Po 𝐵 ∧ (𝐻‘𝑏) ∈ 𝐵) → ¬ (𝐻‘𝑏)𝑆(𝐻‘𝑏))
25		breq1 5152	. . . . . . . . . . . . 13 ⊢ ((𝐻‘𝑎) = (𝐻‘𝑏) → ((𝐻‘𝑎)𝑆(𝐻‘𝑏) ↔ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
26	25	notbid 318	. . . . . . . . . . . 12 ⊢ ((𝐻‘𝑎) = (𝐻‘𝑏) → (¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏) ↔ ¬ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
27	24, 26	syl5ibrcom 246	. . . . . . . . . . 11 ⊢ ((𝑆 Po 𝐵 ∧ (𝐻‘𝑏) ∈ 𝐵) → ((𝐻‘𝑎) = (𝐻‘𝑏) → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
28	19, 23, 27	syl2anc 585	. . . . . . . . . 10 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐻‘𝑎) = (𝐻‘𝑏) → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
29	28	con2d 134	. . . . . . . . 9 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐻‘𝑎)𝑆(𝐻‘𝑏) → ¬ (𝐻‘𝑎) = (𝐻‘𝑏)))
30	18, 29	syld 47	. . . . . . . 8 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎𝑅𝑏 → ¬ (𝐻‘𝑎) = (𝐻‘𝑏)))
31		breq1 5152	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑏 → (𝑥𝑅𝑦 ↔ 𝑏𝑅𝑦))
32		fveq2 6892	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑏 → (𝐻‘𝑥) = (𝐻‘𝑏))
33	32	breq1d 5159	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑏 → ((𝐻‘𝑥)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝑏)𝑆(𝐻‘𝑦)))
34	31, 33	imbi12d 345	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑏 → ((𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ (𝑏𝑅𝑦 → (𝐻‘𝑏)𝑆(𝐻‘𝑦))))
35		breq2 5153	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑎 → (𝑏𝑅𝑦 ↔ 𝑏𝑅𝑎))
36		fveq2 6892	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑎 → (𝐻‘𝑦) = (𝐻‘𝑎))
37	36	breq2d 5161	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑎 → ((𝐻‘𝑏)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
38	35, 37	imbi12d 345	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑎 → ((𝑏𝑅𝑦 → (𝐻‘𝑏)𝑆(𝐻‘𝑦)) ↔ (𝑏𝑅𝑎 → (𝐻‘𝑏)𝑆(𝐻‘𝑎))))
39	34, 38	rspc2va 3624	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦))) → (𝑏𝑅𝑎 → (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
40	39	ancoms 460	. . . . . . . . . . 11 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ∧ (𝑏 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴)) → (𝑏𝑅𝑎 → (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
41	40	ancom2s 649	. . . . . . . . . 10 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑏𝑅𝑎 → (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
42	7, 41	sylan 581	. . . . . . . . 9 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑏𝑅𝑎 → (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
43		breq2 5153	. . . . . . . . . . . . 13 ⊢ ((𝐻‘𝑎) = (𝐻‘𝑏) → ((𝐻‘𝑏)𝑆(𝐻‘𝑎) ↔ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
44	43	notbid 318	. . . . . . . . . . . 12 ⊢ ((𝐻‘𝑎) = (𝐻‘𝑏) → (¬ (𝐻‘𝑏)𝑆(𝐻‘𝑎) ↔ ¬ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
45	24, 44	syl5ibrcom 246	. . . . . . . . . . 11 ⊢ ((𝑆 Po 𝐵 ∧ (𝐻‘𝑏) ∈ 𝐵) → ((𝐻‘𝑎) = (𝐻‘𝑏) → ¬ (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
46	19, 23, 45	syl2anc 585	. . . . . . . . . 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 858	. . . . . . 7 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎𝑅𝑏 ∨ 𝑏𝑅𝑎) → ¬ (𝐻‘𝑎) = (𝐻‘𝑏)))
50	6, 49	sylbird 260	. . . . . 6 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (¬ 𝑎 = 𝑏 → ¬ (𝐻‘𝑎) = (𝐻‘𝑏)))
51	50	con4d 115	. . . . 5 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐻‘𝑎) = (𝐻‘𝑏) → 𝑎 = 𝑏))
52	51	ralrimivva 3201	. . . 4 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ((𝐻‘𝑎) = (𝐻‘𝑏) → 𝑎 = 𝑏))
53		dff13 7254	. . . 4 ⊢ (𝐻:𝐴–1-1→𝐵 ↔ (𝐻:𝐴⟶𝐵 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ((𝐻‘𝑎) = (𝐻‘𝑏) → 𝑎 = 𝑏)))
54	3, 52, 53	sylanbrc 584	. . 3 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻:𝐴–1-1→𝐵)
55		df-f1o 6551	. . 3 ⊢ (𝐻:𝐴–1-1-onto→𝐵 ↔ (𝐻:𝐴–1-1→𝐵 ∧ 𝐻:𝐴–onto→𝐵))
56	54, 1, 55	sylanbrc 584	. 2 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻:𝐴–1-1-onto→𝐵)
57		sotric 5617	. . . . . . 7 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎𝑅𝑏 ↔ ¬ (𝑎 = 𝑏 ∨ 𝑏𝑅𝑎)))
58	57	con2bid 355	. . . . . 6 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎 = 𝑏 ∨ 𝑏𝑅𝑎) ↔ ¬ 𝑎𝑅𝑏))
59	58	ad4ant14 751	. . . . 5 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎 = 𝑏 ∨ 𝑏𝑅𝑎) ↔ ¬ 𝑎𝑅𝑏))
60		fveq2 6892	. . . . . . . . . 10 ⊢ (𝑎 = 𝑏 → (𝐻‘𝑎) = (𝐻‘𝑏))
61	60	breq1d 5159	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → ((𝐻‘𝑎)𝑆(𝐻‘𝑏) ↔ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
62	61	notbid 318	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏) ↔ ¬ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
63	24, 62	syl5ibrcom 246	. . . . . . 7 ⊢ ((𝑆 Po 𝐵 ∧ (𝐻‘𝑏) ∈ 𝐵) → (𝑎 = 𝑏 → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
64	19, 23, 63	syl2anc 585	. . . . . 6 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎 = 𝑏 → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
65		simprl 770	. . . . . . . . 9 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑎 ∈ 𝐴)
66	21, 65	ffvelcdmd 7088	. . . . . . . 8 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝐻‘𝑎) ∈ 𝐵)
67		po2nr 5603	. . . . . . . . 9 ⊢ ((𝑆 Po 𝐵 ∧ ((𝐻‘𝑏) ∈ 𝐵 ∧ (𝐻‘𝑎) ∈ 𝐵)) → ¬ ((𝐻‘𝑏)𝑆(𝐻‘𝑎) ∧ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
68		imnan 401	. . . . . . . . 9 ⊢ (((𝐻‘𝑏)𝑆(𝐻‘𝑎) → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)) ↔ ¬ ((𝐻‘𝑏)𝑆(𝐻‘𝑎) ∧ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
69	67, 68	sylibr 233	. . . . . . . 8 ⊢ ((𝑆 Po 𝐵 ∧ ((𝐻‘𝑏) ∈ 𝐵 ∧ (𝐻‘𝑎) ∈ 𝐵)) → ((𝐻‘𝑏)𝑆(𝐻‘𝑎) → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
70	19, 23, 66, 69	syl12anc 836	. . . . . . 7 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐻‘𝑏)𝑆(𝐻‘𝑎) → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
71	42, 70	syld 47	. . . . . 6 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑏𝑅𝑎 → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
72	64, 71	jaod 858	. . . . 5 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎 = 𝑏 ∨ 𝑏𝑅𝑎) → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
73	59, 72	sylbird 260	. . . 4 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (¬ 𝑎𝑅𝑏 → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
74	18, 73	impcon4bid 226	. . 3 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎𝑅𝑏 ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
75	74	ralrimivva 3201	. 2 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎𝑅𝑏 ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
76		df-isom 6553	. 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎𝑅𝑏 ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏))))
77	56, 75, 76	sylanbrc 584	1 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   = wceq 1542   ∈ wcel 2107  ∀wral 3062   class class class wbr 5149   Po wpo 5587   Or wor 5588  ⟶wf 6540  –1-1→wf1 6541  –onto→wfo 6542  –1-1-onto→wf1o 6543  ‘cfv 6544   Isom wiso 6545

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-id 5575  df-po 5589  df-so 5590  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553

This theorem is referenced by:  ordtypelem8  9520  cantnf  9688  fin23lem27  10323  iccpnfhmeo  24461  xrhmeo  24462  logccv  26171  xrge0iifiso  32915