soisoi

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

		Ref	Expression
	Assertion	soisoi	$⊢ ((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \to H {Isom}_{R, S} (A, B)$

Proof

Step	Hyp	Ref	Expression
1		simprl	$⊢ ((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \to H : A \underset{onto}{⟶} B$
2		fof	$⊢ H : A \underset{onto}{⟶} B \to H : A ⟶ B$
3	1 2	syl	$⊢ ((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \to H : A ⟶ B$
4		sotrieq	$⊢ (R Or A \land (a \in A \land b \in A)) \to (a = b \leftrightarrow \neg (a R b \lor b R a))$
5	4	con2bid	$⊢ (R Or A \land (a \in A \land b \in A)) \to ((a R b \lor b R a) \leftrightarrow \neg a = b)$
6	5	ad4ant14	$⊢ (((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \land (a \in A \land b \in A)) \to ((a R b \lor b R a) \leftrightarrow \neg a = b)$
7		simprr	$⊢ ((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \to \forall x \in A \forall y \in A (x R y \to H (x) S H (y))$
8		breq1	$⊢ x = a \to (x R y \leftrightarrow a R y)$
9		fveq2	$⊢ x = a \to H (x) = H (a)$
10	9	breq1d	$⊢ x = a \to (H (x) S H (y) \leftrightarrow H (a) S H (y))$
11	8 10	imbi12d	$⊢ x = a \to ((x R y \to H (x) S H (y)) \leftrightarrow (a R y \to H (a) S H (y)))$
12		breq2	$⊢ y = b \to (a R y \leftrightarrow a R b)$
13		fveq2	$⊢ y = b \to H (y) = H (b)$
14	13	breq2d	$⊢ y = b \to (H (a) S H (y) \leftrightarrow H (a) S H (b))$
15	12 14	imbi12d	$⊢ y = b \to ((a R y \to H (a) S H (y)) \leftrightarrow (a R b \to H (a) S H (b)))$
16	11 15	rspc2va	$⊢ ((a \in A \land b \in A) \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y))) \to (a R b \to H (a) S H (b))$
17	16	ancoms	$⊢ (\forall x \in A \forall y \in A (x R y \to H (x) S H (y)) \land (a \in A \land b \in A)) \to (a R b \to H (a) S H (b))$
18	7 17	sylan	$⊢ (((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \land (a \in A \land b \in A)) \to (a R b \to H (a) S H (b))$
19		simpllr	$⊢ (((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \land (a \in A \land b \in A)) \to S Po B$
20		simplrl	$⊢ (((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \land (a \in A \land b \in A)) \to H : A \underset{onto}{⟶} B$
21	20 2	syl	$⊢ (((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \land (a \in A \land b \in A)) \to H : A ⟶ B$
22		simprr	$⊢ (((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \land (a \in A \land b \in A)) \to b \in A$
23	21 22	ffvelrnd	$⊢ (((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \land (a \in A \land b \in A)) \to H (b) \in B$
24		poirr	$⊢ (S Po B \land H (b) \in B) \to \neg H (b) S H (b)$
25		breq1	$⊢ H (a) = H (b) \to (H (a) S H (b) \leftrightarrow H (b) S H (b))$
26	25	notbid	$⊢ H (a) = H (b) \to (\neg H (a) S H (b) \leftrightarrow \neg H (b) S H (b))$
27	24 26	syl5ibrcom	$⊢ (S Po B \land H (b) \in B) \to (H (a) = H (b) \to \neg H (a) S H (b))$
28	19 23 27	syl2anc	$⊢ (((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \land (a \in A \land b \in A)) \to (H (a) = H (b) \to \neg H (a) S H (b))$
29	28	con2d	$⊢ (((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \land (a \in A \land b \in A)) \to (H (a) S H (b) \to \neg H (a) = H (b))$
30	18 29	syld	$⊢ (((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \land (a \in A \land b \in A)) \to (a R b \to \neg H (a) = H (b))$
31		breq1	$⊢ x = b \to (x R y \leftrightarrow b R y)$
32		fveq2	$⊢ x = b \to H (x) = H (b)$
33	32	breq1d	$⊢ x = b \to (H (x) S H (y) \leftrightarrow H (b) S H (y))$
34	31 33	imbi12d	$⊢ x = b \to ((x R y \to H (x) S H (y)) \leftrightarrow (b R y \to H (b) S H (y)))$
35		breq2	$⊢ y = a \to (b R y \leftrightarrow b R a)$
36		fveq2	$⊢ y = a \to H (y) = H (a)$
37	36	breq2d	$⊢ y = a \to (H (b) S H (y) \leftrightarrow H (b) S H (a))$
38	35 37	imbi12d	$⊢ y = a \to ((b R y \to H (b) S H (y)) \leftrightarrow (b R a \to H (b) S H (a)))$
39	34 38	rspc2va	$⊢ ((b \in A \land a \in A) \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y))) \to (b R a \to H (b) S H (a))$
40	39	ancoms	$⊢ (\forall x \in A \forall y \in A (x R y \to H (x) S H (y)) \land (b \in A \land a \in A)) \to (b R a \to H (b) S H (a))$
41	40	ancom2s	$⊢ (\forall x \in A \forall y \in A (x R y \to H (x) S H (y)) \land (a \in A \land b \in A)) \to (b R a \to H (b) S H (a))$
42	7 41	sylan	$⊢ (((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \land (a \in A \land b \in A)) \to (b R a \to H (b) S H (a))$
43		breq2	$⊢ H (a) = H (b) \to (H (b) S H (a) \leftrightarrow H (b) S H (b))$
44	43	notbid	$⊢ H (a) = H (b) \to (\neg H (b) S H (a) \leftrightarrow \neg H (b) S H (b))$
45	24 44	syl5ibrcom	$⊢ (S Po B \land H (b) \in B) \to (H (a) = H (b) \to \neg H (b) S H (a))$
46	19 23 45	syl2anc	$⊢ (((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \land (a \in A \land b \in A)) \to (H (a) = H (b) \to \neg H (b) S H (a))$
47	46	con2d	$⊢ (((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \land (a \in A \land b \in A)) \to (H (b) S H (a) \to \neg H (a) = H (b))$
48	42 47	syld	$⊢ (((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \land (a \in A \land b \in A)) \to (b R a \to \neg H (a) = H (b))$
49	30 48	jaod	$⊢ (((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \land (a \in A \land b \in A)) \to ((a R b \lor b R a) \to \neg H (a) = H (b))$
50	6 49	sylbird	$⊢ (((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \land (a \in A \land b \in A)) \to (\neg a = b \to \neg H (a) = H (b))$
51	50	con4d	$⊢ (((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \land (a \in A \land b \in A)) \to (H (a) = H (b) \to a = b)$
52	51	ralrimivva	$⊢ ((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \to \forall a \in A \forall b \in A (H (a) = H (b) \to a = b)$
53		dff13	$⊢ H : A \underset{1-1}{⟶} B \leftrightarrow (H : A ⟶ B \land \forall a \in A \forall b \in A (H (a) = H (b) \to a = b))$
54	3 52 53	sylanbrc	$⊢ ((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \to H : A \underset{1-1}{⟶} B$
55		df-f1o	$⊢ H : A \underset{1-1 onto}{⟶} B \leftrightarrow (H : A \underset{1-1}{⟶} B \land H : A \underset{onto}{⟶} B)$
56	54 1 55	sylanbrc	$⊢ ((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \to H : A \underset{1-1 onto}{⟶} B$
57		sotric	$⊢ (R Or A \land (a \in A \land b \in A)) \to (a R b \leftrightarrow \neg (a = b \lor b R a))$
58	57	con2bid	$⊢ (R Or A \land (a \in A \land b \in A)) \to ((a = b \lor b R a) \leftrightarrow \neg a R b)$
59	58	ad4ant14	$⊢ (((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \land (a \in A \land b \in A)) \to ((a = b \lor b R a) \leftrightarrow \neg a R b)$
60		fveq2	$⊢ a = b \to H (a) = H (b)$
61	60	breq1d	$⊢ a = b \to (H (a) S H (b) \leftrightarrow H (b) S H (b))$
62	61	notbid	$⊢ a = b \to (\neg H (a) S H (b) \leftrightarrow \neg H (b) S H (b))$
63	24 62	syl5ibrcom	$⊢ (S Po B \land H (b) \in B) \to (a = b \to \neg H (a) S H (b))$
64	19 23 63	syl2anc	$⊢ (((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \land (a \in A \land b \in A)) \to (a = b \to \neg H (a) S H (b))$
65		simprl	$⊢ (((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \land (a \in A \land b \in A)) \to a \in A$
66	21 65	ffvelrnd	$⊢ (((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \land (a \in A \land b \in A)) \to H (a) \in B$
67		po2nr	$⊢ (S Po B \land (H (b) \in B \land H (a) \in B)) \to \neg (H (b) S H (a) \land H (a) S H (b))$
68		imnan	$⊢ (H (b) S H (a) \to \neg H (a) S H (b)) \leftrightarrow \neg (H (b) S H (a) \land H (a) S H (b))$
69	67 68	sylibr	$⊢ (S Po B \land (H (b) \in B \land H (a) \in B)) \to (H (b) S H (a) \to \neg H (a) S H (b))$
70	19 23 66 69	syl12anc	$⊢ (((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \land (a \in A \land b \in A)) \to (H (b) S H (a) \to \neg H (a) S H (b))$
71	42 70	syld	$⊢ (((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \land (a \in A \land b \in A)) \to (b R a \to \neg H (a) S H (b))$
72	64 71	jaod	$⊢ (((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \land (a \in A \land b \in A)) \to ((a = b \lor b R a) \to \neg H (a) S H (b))$
73	59 72	sylbird	$⊢ (((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \land (a \in A \land b \in A)) \to (\neg a R b \to \neg H (a) S H (b))$
74	18 73	impcon4bid	$⊢ (((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \land (a \in A \land b \in A)) \to (a R b \leftrightarrow H (a) S H (b))$
75	74	ralrimivva	$⊢ ((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \to \forall a \in A \forall b \in A (a R b \leftrightarrow H (a) S H (b))$
76		df-isom	$⊢ H {Isom}_{R, S} (A, B) \leftrightarrow (H : A \underset{1-1 onto}{⟶} B \land \forall a \in A \forall b \in A (a R b \leftrightarrow H (a) S H (b)))$
77	56 75 76	sylanbrc	$⊢ ((R Or A \land S Po B) \land (H : A \underset{onto}{⟶} B \land \forall x \in A \forall y \in A (x R y \to H (x) S H (y)))) \to H {Isom}_{R, S} (A, B)$

Metamath Proof Explorer

Theorem soisoi

Proof