Theorem soisoi 7083

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 6592	. . . . 5 ⊢ (𝐻:𝐴–onto→𝐵 → 𝐻:𝐴⟶𝐵)
3	1, 2	syl 17	. . . 4 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻:𝐴⟶𝐵)
4		sotrieq 5504	. . . . . . . . 9 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎 = 𝑏 ↔ ¬ (𝑎𝑅𝑏 ∨ 𝑏𝑅𝑎)))
5	4	con2bid 357	. . . . . . . 8 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎𝑅𝑏 ∨ 𝑏𝑅𝑎) ↔ ¬ 𝑎 = 𝑏))
6	5	ad4ant14 750	. . . . . . 7 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎𝑅𝑏 ∨ 𝑏𝑅𝑎) ↔ ¬ 𝑎 = 𝑏))
7		simprr 771	. . . . . . . . . 10 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))
8		breq1 5071	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑎 → (𝑥𝑅𝑦 ↔ 𝑎𝑅𝑦))
9		fveq2 6672	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑎 → (𝐻‘𝑥) = (𝐻‘𝑎))
10	9	breq1d 5078	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑎 → ((𝐻‘𝑥)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑦)))
11	8, 10	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑎 → ((𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ (𝑎𝑅𝑦 → (𝐻‘𝑎)𝑆(𝐻‘𝑦))))
12		breq2 5072	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑏 → (𝑎𝑅𝑦 ↔ 𝑎𝑅𝑏))
13		fveq2 6672	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑏 → (𝐻‘𝑦) = (𝐻‘𝑏))
14	13	breq2d 5080	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑏 → ((𝐻‘𝑎)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
15	12, 14	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → ((𝑎𝑅𝑦 → (𝐻‘𝑎)𝑆(𝐻‘𝑦)) ↔ (𝑎𝑅𝑏 → (𝐻‘𝑎)𝑆(𝐻‘𝑏))))
16	11, 15	rspc2va 3636	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦))) → (𝑎𝑅𝑏 → (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
17	16	ancoms 461	. . . . . . . . . 10 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎𝑅𝑏 → (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
18	7, 17	sylan 582	. . . . . . . . 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	ffvelrnd 6854	. . . . . . . . . . 11 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝐻‘𝑏) ∈ 𝐵)
24		poirr 5487	. . . . . . . . . . . 12 ⊢ ((𝑆 Po 𝐵 ∧ (𝐻‘𝑏) ∈ 𝐵) → ¬ (𝐻‘𝑏)𝑆(𝐻‘𝑏))
25		breq1 5071	. . . . . . . . . . . . 13 ⊢ ((𝐻‘𝑎) = (𝐻‘𝑏) → ((𝐻‘𝑎)𝑆(𝐻‘𝑏) ↔ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
26	25	notbid 320	. . . . . . . . . . . 12 ⊢ ((𝐻‘𝑎) = (𝐻‘𝑏) → (¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏) ↔ ¬ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
27	24, 26	syl5ibrcom 249	. . . . . . . . . . 11 ⊢ ((𝑆 Po 𝐵 ∧ (𝐻‘𝑏) ∈ 𝐵) → ((𝐻‘𝑎) = (𝐻‘𝑏) → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
28	19, 23, 27	syl2anc 586	. . . . . . . . . 10 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐻‘𝑎) = (𝐻‘𝑏) → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
29	28	con2d 136	. . . . . . . . 9 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐻‘𝑎)𝑆(𝐻‘𝑏) → ¬ (𝐻‘𝑎) = (𝐻‘𝑏)))
30	18, 29	syld 47	. . . . . . . 8 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎𝑅𝑏 → ¬ (𝐻‘𝑎) = (𝐻‘𝑏)))
31		breq1 5071	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑏 → (𝑥𝑅𝑦 ↔ 𝑏𝑅𝑦))
32		fveq2 6672	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑏 → (𝐻‘𝑥) = (𝐻‘𝑏))
33	32	breq1d 5078	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑏 → ((𝐻‘𝑥)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝑏)𝑆(𝐻‘𝑦)))
34	31, 33	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑏 → ((𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ (𝑏𝑅𝑦 → (𝐻‘𝑏)𝑆(𝐻‘𝑦))))
35		breq2 5072	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑎 → (𝑏𝑅𝑦 ↔ 𝑏𝑅𝑎))
36		fveq2 6672	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑎 → (𝐻‘𝑦) = (𝐻‘𝑎))
37	36	breq2d 5080	. . . . . . . . . . . . . 14 ⊢ (𝑦 = 𝑎 → ((𝐻‘𝑏)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
38	35, 37	imbi12d 347	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑎 → ((𝑏𝑅𝑦 → (𝐻‘𝑏)𝑆(𝐻‘𝑦)) ↔ (𝑏𝑅𝑎 → (𝐻‘𝑏)𝑆(𝐻‘𝑎))))
39	34, 38	rspc2va 3636	. . . . . . . . . . . 12 ⊢ (((𝑏 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦))) → (𝑏𝑅𝑎 → (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
40	39	ancoms 461	. . . . . . . . . . 11 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ∧ (𝑏 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴)) → (𝑏𝑅𝑎 → (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
41	40	ancom2s 648	. . . . . . . . . 10 ⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑏𝑅𝑎 → (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
42	7, 41	sylan 582	. . . . . . . . 9 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑏𝑅𝑎 → (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
43		breq2 5072	. . . . . . . . . . . . 13 ⊢ ((𝐻‘𝑎) = (𝐻‘𝑏) → ((𝐻‘𝑏)𝑆(𝐻‘𝑎) ↔ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
44	43	notbid 320	. . . . . . . . . . . 12 ⊢ ((𝐻‘𝑎) = (𝐻‘𝑏) → (¬ (𝐻‘𝑏)𝑆(𝐻‘𝑎) ↔ ¬ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
45	24, 44	syl5ibrcom 249	. . . . . . . . . . 11 ⊢ ((𝑆 Po 𝐵 ∧ (𝐻‘𝑏) ∈ 𝐵) → ((𝐻‘𝑎) = (𝐻‘𝑏) → ¬ (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
46	19, 23, 45	syl2anc 586	. . . . . . . . . 10 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐻‘𝑎) = (𝐻‘𝑏) → ¬ (𝐻‘𝑏)𝑆(𝐻‘𝑎)))
47	46	con2d 136	. . . . . . . . 9 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐻‘𝑏)𝑆(𝐻‘𝑎) → ¬ (𝐻‘𝑎) = (𝐻‘𝑏)))
48	42, 47	syld 47	. . . . . . . 8 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑏𝑅𝑎 → ¬ (𝐻‘𝑎) = (𝐻‘𝑏)))
49	30, 48	jaod 855	. . . . . . 7 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎𝑅𝑏 ∨ 𝑏𝑅𝑎) → ¬ (𝐻‘𝑎) = (𝐻‘𝑏)))
50	6, 49	sylbird 262	. . . . . 6 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (¬ 𝑎 = 𝑏 → ¬ (𝐻‘𝑎) = (𝐻‘𝑏)))
51	50	con4d 115	. . . . 5 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝐻‘𝑎) = (𝐻‘𝑏) → 𝑎 = 𝑏))
52	51	ralrimivva 3193	. . . 4 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ((𝐻‘𝑎) = (𝐻‘𝑏) → 𝑎 = 𝑏))
53		dff13 7015	. . . 4 ⊢ (𝐻:𝐴–1-1→𝐵 ↔ (𝐻:𝐴⟶𝐵 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ((𝐻‘𝑎) = (𝐻‘𝑏) → 𝑎 = 𝑏)))
54	3, 52, 53	sylanbrc 585	. . 3 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻:𝐴–1-1→𝐵)
55		df-f1o 6364	. . 3 ⊢ (𝐻:𝐴–1-1-onto→𝐵 ↔ (𝐻:𝐴–1-1→𝐵 ∧ 𝐻:𝐴–onto→𝐵))
56	54, 1, 55	sylanbrc 585	. 2 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻:𝐴–1-1-onto→𝐵)
57		sotric 5503	. . . . . . 7 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎𝑅𝑏 ↔ ¬ (𝑎 = 𝑏 ∨ 𝑏𝑅𝑎)))
58	57	con2bid 357	. . . . . 6 ⊢ ((𝑅 Or 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎 = 𝑏 ∨ 𝑏𝑅𝑎) ↔ ¬ 𝑎𝑅𝑏))
59	58	ad4ant14 750	. . . . 5 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎 = 𝑏 ∨ 𝑏𝑅𝑎) ↔ ¬ 𝑎𝑅𝑏))
60		fveq2 6672	. . . . . . . . . 10 ⊢ (𝑎 = 𝑏 → (𝐻‘𝑎) = (𝐻‘𝑏))
61	60	breq1d 5078	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → ((𝐻‘𝑎)𝑆(𝐻‘𝑏) ↔ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
62	61	notbid 320	. . . . . . . 8 ⊢ (𝑎 = 𝑏 → (¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏) ↔ ¬ (𝐻‘𝑏)𝑆(𝐻‘𝑏)))
63	24, 62	syl5ibrcom 249	. . . . . . 7 ⊢ ((𝑆 Po 𝐵 ∧ (𝐻‘𝑏) ∈ 𝐵) → (𝑎 = 𝑏 → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
64	19, 23, 63	syl2anc 586	. . . . . 6 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎 = 𝑏 → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
65		simprl 769	. . . . . . . . 9 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑎 ∈ 𝐴)
66	21, 65	ffvelrnd 6854	. . . . . . . 8 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝐻‘𝑎) ∈ 𝐵)
67		po2nr 5489	. . . . . . . . 9 ⊢ ((𝑆 Po 𝐵 ∧ ((𝐻‘𝑏) ∈ 𝐵 ∧ (𝐻‘𝑎) ∈ 𝐵)) → ¬ ((𝐻‘𝑏)𝑆(𝐻‘𝑎) ∧ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
68		imnan 402	. . . . . . . . 9 ⊢ (((𝐻‘𝑏)𝑆(𝐻‘𝑎) → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)) ↔ ¬ ((𝐻‘𝑏)𝑆(𝐻‘𝑎) ∧ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
69	67, 68	sylibr 236	. . . . . . . 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 855	. . . . 5 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑎 = 𝑏 ∨ 𝑏𝑅𝑎) → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
73	59, 72	sylbird 262	. . . 4 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (¬ 𝑎𝑅𝑏 → ¬ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
74	18, 73	impcon4bid 229	. . 3 ⊢ ((((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎𝑅𝑏 ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
75	74	ralrimivva 3193	. 2 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎𝑅𝑏 ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏)))
76		df-isom 6366	. 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎𝑅𝑏 ↔ (𝐻‘𝑎)𝑆(𝐻‘𝑏))))
77	56, 75, 76	sylanbrc 585	1 ⊢ (((𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝐻:𝐴–onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) → 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   = wceq 1537   ∈ wcel 2114  ∀wral 3140   class class class wbr 5068   Po wpo 5474   Or wor 5475  ⟶wf 6353  –1-1→wf1 6354  –onto→wfo 6355  –1-1-onto→wf1o 6356  ‘cfv 6357   Isom wiso 6358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-id 5462  df-po 5476  df-so 5477  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-isom 6366

This theorem is referenced by:  ordtypelem8  8991  cantnf  9158  fin23lem27  9752  iccpnfhmeo  23551  xrhmeo  23552  logccv  25248  xrge0iifiso  31180