soisores

Description: Express the condition of isomorphism on two strict orders for a function's restriction. (Contributed by Mario Carneiro, 22-Jan-2015)

		Ref	Expression
	Assertion	soisores	$⊢ ((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B)) \to (({F ↾}_{A}) {Isom}_{R, S} (A, F [A]) \leftrightarrow \forall x \in A \forall y \in A (x R y \to F (x) S F (y)))$

Proof

Step	Hyp	Ref	Expression
1		isorel	$⊢ (({F ↾}_{A}) {Isom}_{R, S} (A, F [A]) \land (x \in A \land y \in A)) \to (x R y \leftrightarrow ({F ↾}_{A}) (x) S ({F ↾}_{A}) (y))$
2		fvres	$⊢ x \in A \to ({F ↾}_{A}) (x) = F (x)$
3		fvres	$⊢ y \in A \to ({F ↾}_{A}) (y) = F (y)$
4	2 3	breqan12d	$⊢ (x \in A \land y \in A) \to (({F ↾}_{A}) (x) S ({F ↾}_{A}) (y) \leftrightarrow F (x) S F (y))$
5	4	adantl	$⊢ (({F ↾}_{A}) {Isom}_{R, S} (A, F [A]) \land (x \in A \land y \in A)) \to (({F ↾}_{A}) (x) S ({F ↾}_{A}) (y) \leftrightarrow F (x) S F (y))$
6	1 5	bitrd	$⊢ (({F ↾}_{A}) {Isom}_{R, S} (A, F [A]) \land (x \in A \land y \in A)) \to (x R y \leftrightarrow F (x) S F (y))$
7	6	biimpd	$⊢ (({F ↾}_{A}) {Isom}_{R, S} (A, F [A]) \land (x \in A \land y \in A)) \to (x R y \to F (x) S F (y))$
8	7	ralrimivva	$⊢ ({F ↾}_{A}) {Isom}_{R, S} (A, F [A]) \to \forall x \in A \forall y \in A (x R y \to F (x) S F (y))$
9		ffn	$⊢ F : B ⟶ C \to F Fn B$
10	9	ad2antrl	$⊢ ((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B)) \to F Fn B$
11		simprr	$⊢ ((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B)) \to A \subseteq B$
12		fnssres	$⊢ (F Fn B \land A \subseteq B) \to ({F ↾}_{A}) Fn A$
13	10 11 12	syl2anc	$⊢ ((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B)) \to ({F ↾}_{A}) Fn A$
14	13	3adant3	$⊢ ((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \to ({F ↾}_{A}) Fn A$
15		df-ima	$⊢ F [A] = ran ({F ↾}_{A})$
16	15	eqcomi	$⊢ ran ({F ↾}_{A}) = F [A]$
17	16	a1i	$⊢ ((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \to ran ({F ↾}_{A}) = F [A]$
18		fvres	$⊢ z \in A \to ({F ↾}_{A}) (z) = F (z)$
19		fvres	$⊢ w \in A \to ({F ↾}_{A}) (w) = F (w)$
20	18 19	eqeqan12d	$⊢ (z \in A \land w \in A) \to (({F ↾}_{A}) (z) = ({F ↾}_{A}) (w) \leftrightarrow F (z) = F (w))$
21	20	adantl	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to (({F ↾}_{A}) (z) = ({F ↾}_{A}) (w) \leftrightarrow F (z) = F (w))$
22		simprl	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to z \in A$
23		simprr	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to w \in A$
24		simpl3	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to \forall x \in A \forall y \in A (x R y \to F (x) S F (y))$
25		breq1	$⊢ x = z \to (x R y \leftrightarrow z R y)$
26		fveq2	$⊢ x = z \to F (x) = F (z)$
27	26	breq1d	$⊢ x = z \to (F (x) S F (y) \leftrightarrow F (z) S F (y))$
28	25 27	imbi12d	$⊢ x = z \to ((x R y \to F (x) S F (y)) \leftrightarrow (z R y \to F (z) S F (y)))$
29		breq2	$⊢ y = w \to (z R y \leftrightarrow z R w)$
30		fveq2	$⊢ y = w \to F (y) = F (w)$
31	30	breq2d	$⊢ y = w \to (F (z) S F (y) \leftrightarrow F (z) S F (w))$
32	29 31	imbi12d	$⊢ y = w \to ((z R y \to F (z) S F (y)) \leftrightarrow (z R w \to F (z) S F (w)))$
33	28 32	rspc2va	$⊢ ((z \in A \land w \in A) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \to (z R w \to F (z) S F (w))$
34	22 23 24 33	syl21anc	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to (z R w \to F (z) S F (w))$
35		breq1	$⊢ x = w \to (x R y \leftrightarrow w R y)$
36		fveq2	$⊢ x = w \to F (x) = F (w)$
37	36	breq1d	$⊢ x = w \to (F (x) S F (y) \leftrightarrow F (w) S F (y))$
38	35 37	imbi12d	$⊢ x = w \to ((x R y \to F (x) S F (y)) \leftrightarrow (w R y \to F (w) S F (y)))$
39		breq2	$⊢ y = z \to (w R y \leftrightarrow w R z)$
40		fveq2	$⊢ y = z \to F (y) = F (z)$
41	40	breq2d	$⊢ y = z \to (F (w) S F (y) \leftrightarrow F (w) S F (z))$
42	39 41	imbi12d	$⊢ y = z \to ((w R y \to F (w) S F (y)) \leftrightarrow (w R z \to F (w) S F (z)))$
43	38 42	rspc2va	$⊢ ((w \in A \land z \in A) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \to (w R z \to F (w) S F (z))$
44	23 22 24 43	syl21anc	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to (w R z \to F (w) S F (z))$
45	34 44	orim12d	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to ((z R w \lor w R z) \to (F (z) S F (w) \lor F (w) S F (z)))$
46	45	con3d	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to (\neg (F (z) S F (w) \lor F (w) S F (z)) \to \neg (z R w \lor w R z))$
47		simpl1r	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to S Or C$
48		simpl2l	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to F : B ⟶ C$
49		simpl2r	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to A \subseteq B$
50	49 22	sseldd	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to z \in B$
51	48 50	ffvelcdmd	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to F (z) \in C$
52	49 23	sseldd	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to w \in B$
53	48 52	ffvelcdmd	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to F (w) \in C$
54		sotrieq	$⊢ (S Or C \land (F (z) \in C \land F (w) \in C)) \to (F (z) = F (w) \leftrightarrow \neg (F (z) S F (w) \lor F (w) S F (z)))$
55	47 51 53 54	syl12anc	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to (F (z) = F (w) \leftrightarrow \neg (F (z) S F (w) \lor F (w) S F (z)))$
56		simpl1l	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to R Or B$
57		sotrieq	$⊢ (R Or B \land (z \in B \land w \in B)) \to (z = w \leftrightarrow \neg (z R w \lor w R z))$
58	56 50 52 57	syl12anc	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to (z = w \leftrightarrow \neg (z R w \lor w R z))$
59	46 55 58	3imtr4d	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to (F (z) = F (w) \to z = w)$
60	21 59	sylbid	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to (({F ↾}_{A}) (z) = ({F ↾}_{A}) (w) \to z = w)$
61	60	ralrimivva	$⊢ ((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \to \forall z \in A \forall w \in A (({F ↾}_{A}) (z) = ({F ↾}_{A}) (w) \to z = w)$
62		dff1o6	$⊢ ({F ↾}_{A}) : A \underset{1-1 onto}{⟶} F [A] \leftrightarrow (({F ↾}_{A}) Fn A \land ran ({F ↾}_{A}) = F [A] \land \forall z \in A \forall w \in A (({F ↾}_{A}) (z) = ({F ↾}_{A}) (w) \to z = w))$
63	14 17 61 62	syl3anbrc	$⊢ ((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \to ({F ↾}_{A}) : A \underset{1-1 onto}{⟶} F [A]$
64		fveq2	$⊢ z = w \to F (z) = F (w)$
65	64	a1i	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to (z = w \to F (z) = F (w))$
66	65 44	orim12d	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to ((z = w \lor w R z) \to (F (z) = F (w) \lor F (w) S F (z)))$
67	66	con3d	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to (\neg (F (z) = F (w) \lor F (w) S F (z)) \to \neg (z = w \lor w R z))$
68		sotric	$⊢ (S Or C \land (F (z) \in C \land F (w) \in C)) \to (F (z) S F (w) \leftrightarrow \neg (F (z) = F (w) \lor F (w) S F (z)))$
69	47 51 53 68	syl12anc	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to (F (z) S F (w) \leftrightarrow \neg (F (z) = F (w) \lor F (w) S F (z)))$
70		sotric	$⊢ (R Or B \land (z \in B \land w \in B)) \to (z R w \leftrightarrow \neg (z = w \lor w R z))$
71	56 50 52 70	syl12anc	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to (z R w \leftrightarrow \neg (z = w \lor w R z))$
72	67 69 71	3imtr4d	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to (F (z) S F (w) \to z R w)$
73	34 72	impbid	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to (z R w \leftrightarrow F (z) S F (w))$
74	18 19	breqan12d	$⊢ (z \in A \land w \in A) \to (({F ↾}_{A}) (z) S ({F ↾}_{A}) (w) \leftrightarrow F (z) S F (w))$
75	74	adantl	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to (({F ↾}_{A}) (z) S ({F ↾}_{A}) (w) \leftrightarrow F (z) S F (w))$
76	73 75	bitr4d	$⊢ (((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \land (z \in A \land w \in A)) \to (z R w \leftrightarrow ({F ↾}_{A}) (z) S ({F ↾}_{A}) (w))$
77	76	ralrimivva	$⊢ ((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \to \forall z \in A \forall w \in A (z R w \leftrightarrow ({F ↾}_{A}) (z) S ({F ↾}_{A}) (w))$
78		df-isom	$⊢ ({F ↾}_{A}) {Isom}_{R, S} (A, F [A]) \leftrightarrow (({F ↾}_{A}) : A \underset{1-1 onto}{⟶} F [A] \land \forall z \in A \forall w \in A (z R w \leftrightarrow ({F ↾}_{A}) (z) S ({F ↾}_{A}) (w)))$
79	63 77 78	sylanbrc	$⊢ ((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B) \land \forall x \in A \forall y \in A (x R y \to F (x) S F (y))) \to ({F ↾}_{A}) {Isom}_{R, S} (A, F [A])$
80	79	3expia	$⊢ ((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B)) \to (\forall x \in A \forall y \in A (x R y \to F (x) S F (y)) \to ({F ↾}_{A}) {Isom}_{R, S} (A, F [A]))$
81	8 80	impbid2	$⊢ ((R Or B \land S Or C) \land (F : B ⟶ C \land A \subseteq B)) \to (({F ↾}_{A}) {Isom}_{R, S} (A, F [A]) \leftrightarrow \forall x \in A \forall y \in A (x R y \to F (x) S F (y)))$

Metamath Proof Explorer

Theorem soisores

Proof