Theorem soisoi 7273

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 769	. . . . 5 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻:𝐴–onto→𝐵)
2		fof 6756	. . . . 5 ⊢ (𝐻:𝐴–onto→𝐵 → 𝐻:𝐴⟶𝐵)
3	1, 2	syl 17	. . . 4 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻:𝐴⟶𝐵)
4		sotrieq 5574	. . . . . . . . 9 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎 = 𝑏 ↔ ¬ (𝑎𝑅𝑏 ∨ 𝑏𝑅𝑎)))
5	4	con2bid 354	. . . . . . . 8 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎𝑅𝑏 ∨ 𝑏𝑅𝑎) ↔ ¬ 𝑎 = 𝑏))
6	5	ad4ant14 750	. . . . . . 7 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎𝑅𝑏 ∨ 𝑏𝑅𝑎) ↔ ¬ 𝑎 = 𝑏))
7		simprr 771	. . . . . . . . . 10 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
8		breq1 5108	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑎 → (𝑥𝑅𝑦 ↔ 𝑎𝑅𝑦))
9		fveq2 6842	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑎 → (𝐻‘𝑥) = (𝐻‘𝑎))
10	9	breq1d 5115	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑎 → ((𝐻‘𝑥)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑦)))
11	8, 10	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑎 → ((𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ (𝑎𝑅𝑦 → (𝐻‘𝑎)𝑆(𝐻‘𝑦))))
12		breq2 5109	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑏 → (𝑎𝑅𝑦 ↔ 𝑎𝑅𝑏))
13		fveq2 6842	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑏 → (𝐻‘𝑦) = (𝐻‘𝑏))
14	13	breq2d 5117	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑏 → ((𝐻‘𝑎)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
15	12, 14	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → ((𝑎𝑅𝑦 → (𝐻‘𝑎)𝑆(𝐻‘𝑦)) ↔ (𝑎𝑅𝑏 → (𝐻‘𝑎)𝑆(𝐻‘𝑏))))
16	11, 15	rspc2va 3591	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦))) → (𝑎𝑅𝑏 → (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
17	16	ancoms 459	. . . . . . . . . 10 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎𝑅𝑏 → (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
18	7, 17	sylan 580	. . . . . . . . 9 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎𝑅𝑏 → (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
19		simpllr 774	. . . . . . . . . . 11 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑆 Po 𝐵)
20		simplrl 775	. . . . . . . . . . . . 13 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝐻:𝐴–onto→𝐵)
21	20, 2	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝐻:𝐴⟶𝐵)
22		simprr 771	. . . . . . . . . . . 12 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑏 ∈ 𝐴)
23	21, 22	ffvelcdmd 7036	. . . . . . . . . . 11 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝐻‘𝑏) ∈ 𝐵)
24		poirr 5557	. . . . . . . . . . . 12 ⊢ ((𝑆 Po 𝐵 ∧ (𝐻‘𝑏) ∈ 𝐵) → ¬ (𝐻‘𝑏)𝑆(𝐻‘𝑏))
25		breq1 5108	. . . . . . . . . . . . 13 ⊢ ((𝐻‘𝑎) = (𝐻‘𝑏) → ((𝐻‘𝑎)𝑆(𝐻‘𝑏) ↔ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
26	25	notbid 317	. . . . . . . . . . . 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 5108	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑏 → (𝑥𝑅𝑦 ↔ 𝑏𝑅𝑦))
32		fveq2 6842	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑏 → (𝐻‘𝑥) = (𝐻‘𝑏))
33	32	breq1d 5115	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑏 → ((𝐻‘𝑥)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝑏)𝑆(𝐻‘𝑦)))
34	31, 33	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑏 → ((𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ (𝑏𝑅𝑦 → (𝐻‘𝑏)𝑆(𝐻‘𝑦))))
35		breq2 5109	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑎 → (𝑏𝑅𝑦 ↔ 𝑏𝑅𝑎))
36		fveq2 6842	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑎 → (𝐻‘𝑦) = (𝐻‘𝑎))
37	36	breq2d 5117	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑎 → ((𝐻‘𝑏)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
38	35, 37	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑎 → ((𝑏𝑅𝑦 → (𝐻‘𝑏)𝑆(𝐻‘𝑦)) ↔ (𝑏𝑅𝑎 → (𝐻‘𝑏)𝑆(𝐻‘𝑎))))
39	34, 38	rspc2va 3591	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦))) → (𝑏𝑅𝑎 → (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
40	39	ancoms 459	. . . . . . . . . . 11 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ∧ (𝑏 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴)) → (𝑏𝑅𝑎 → (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
41	40	ancom2s 648	. . . . . . . . . 10 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑏𝑅𝑎 → (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
42	7, 41	sylan 580	. . . . . . . . 9 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑏𝑅𝑎 → (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
43		breq2 5109	. . . . . . . . . . . . 13 ⊢ ((𝐻‘𝑎) = (𝐻‘𝑏) → ((𝐻‘𝑏)𝑆(𝐻‘𝑎) ↔ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
44	43	notbid 317	. . . . . . . . . . . 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 857	. . . . . . 7 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎𝑅𝑏 ∨ 𝑏𝑅𝑎) → ¬ (𝐻‘𝑎) = (𝐻‘𝑏)))
50	6, 49	sylbird 259	. . . . . 6 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (¬ 𝑎 = 𝑏 → ¬ (𝐻‘𝑎) = (𝐻‘𝑏)))
51	50	con4d 115	. . . . 5 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐻‘𝑎) = (𝐻‘𝑏) → 𝑎 = 𝑏))
52	51	ralrimivva 3197	. . . 4 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ((𝐻‘𝑎) = (𝐻‘𝑏) → 𝑎 = 𝑏))
53		dff13 7202	. . . 4 ⊢ (𝐻:𝐴–1-1→𝐵 ↔ (𝐻:𝐴⟶𝐵 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ((𝐻‘𝑎) = (𝐻‘𝑏) → 𝑎 = 𝑏)))
54	3, 52, 53	sylanbrc 583	. . 3 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻:𝐴–1-1→𝐵)
55		df-f1o 6503	. . 3 ⊢ (𝐻:𝐴–1-1-onto→𝐵 ↔ (𝐻:𝐴–1-1→𝐵 ∧ 𝐻:𝐴–onto→𝐵))
56	54, 1, 55	sylanbrc 583	. 2 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻:𝐴–1-1-onto→𝐵)
57		sotric 5573	. . . . . . 7 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎𝑅𝑏 ↔ ¬ (𝑎 = 𝑏 ∨ 𝑏𝑅𝑎)))
58	57	con2bid 354	. . . . . 6 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎 = 𝑏 ∨ 𝑏𝑅𝑎) ↔ ¬ 𝑎𝑅𝑏))
59	58	ad4ant14 750	. . . . 5 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎 = 𝑏 ∨ 𝑏𝑅𝑎) ↔ ¬ 𝑎𝑅𝑏))
60		fveq2 6842	. . . . . . . . . 10 ⊢ (𝑎 = 𝑏 → (𝐻‘𝑎) = (𝐻‘𝑏))
61	60	breq1d 5115	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → ((𝐻‘𝑎)𝑆(𝐻‘𝑏) ↔ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
62	61	notbid 317	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏) ↔ ¬ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
63	24, 62	syl5ibrcom 246	. . . . . . 7 ⊢ ((𝑆 Po 𝐵 ∧ (𝐻‘𝑏) ∈ 𝐵) → (𝑎 = 𝑏 → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
64	19, 23, 63	syl2anc 584	. . . . . 6 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎 = 𝑏 → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
65		simprl 769	. . . . . . . . 9 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑎 ∈ 𝐴)
66	21, 65	ffvelcdmd 7036	. . . . . . . 8 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝐻‘𝑎) ∈ 𝐵)
67		po2nr 5559	. . . . . . . . 9 ⊢ ((𝑆 Po 𝐵 ∧ ((𝐻‘𝑏) ∈ 𝐵 ∧ (𝐻‘𝑎) ∈ 𝐵)) → ¬ ((𝐻‘𝑏)𝑆(𝐻‘𝑎) ∧ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
68		imnan 400	. . . . . . . . 9 ⊢ (((𝐻‘𝑏)𝑆(𝐻‘𝑎) → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)) ↔ ¬ ((𝐻‘𝑏)𝑆(𝐻‘𝑎) ∧ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
69	67, 68	sylibr 233	. . . . . . . 8 ⊢ ((𝑆 Po 𝐵 ∧ ((𝐻‘𝑏) ∈ 𝐵 ∧ (𝐻‘𝑎) ∈ 𝐵)) → ((𝐻‘𝑏)𝑆(𝐻‘𝑎) → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
70	19, 23, 66, 69	syl12anc 835	. . . . . . 7 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐻‘𝑏)𝑆(𝐻‘𝑎) → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
71	42, 70	syld 47	. . . . . 6 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑏𝑅𝑎 → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
72	64, 71	jaod 857	. . . . 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 3197	. 2 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎𝑅𝑏 ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
76		df-isom 6505	. 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 845   = wceq 1541   ∈ wcel 2106  ∀wral 3064   class class class wbr 5105   Po wpo 5543   Or wor 5544  ⟶wf 6492  –1-1→wf1 6493  –onto→wfo 6494  –1-1-onto→wf1o 6495  ‘cfv 6496   Isom wiso 6497

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  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 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-id 5531  df-po 5545  df-so 5546  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505

This theorem is referenced by:  ordtypelem8  9461  cantnf  9629  fin23lem27  10264  iccpnfhmeo  24308  xrhmeo  24309  logccv  26018  xrge0iifiso  32516