imasleval

Description: The value of the image structure's ordering when the order is compatible with the mapping function. (Contributed by Mario Carneiro, 24-Feb-2015)

	Ref	Expression
Hypotheses	imasless.u	$⊢ φ \to U = F “_{𝑠} R$
	imasless.v	$⊢ φ \to V = {Base}_{R}$
	imasless.f	$⊢ φ \to F : V \underset{onto}{⟶} B$
	imasless.r	$⊢ φ \to R \in Z$
	imasless.l	$⊢ \underset{˙}{\leq} = \leq_{U}$
	imasleval.n	$⊢ N = \leq_{R}$
	imasleval.e	$⊢ (φ \land (a \in V \land b \in V) \land (c \in V \land d \in V)) \to ((F (a) = F (c) \land F (b) = F (d)) \to (a N b \leftrightarrow c N d))$
Assertion	imasleval	$⊢ (φ \land X \in V \land Y \in V) \to (F (X) \underset{˙}{\leq} F (Y) \leftrightarrow X N Y)$

Proof

Step	Hyp	Ref	Expression
1		imasless.u	$⊢ φ \to U = F “_{𝑠} R$
2		imasless.v	$⊢ φ \to V = {Base}_{R}$
3		imasless.f	$⊢ φ \to F : V \underset{onto}{⟶} B$
4		imasless.r	$⊢ φ \to R \in Z$
5		imasless.l	$⊢ \underset{˙}{\leq} = \leq_{U}$
6		imasleval.n	$⊢ N = \leq_{R}$
7		imasleval.e	$⊢ (φ \land (a \in V \land b \in V) \land (c \in V \land d \in V)) \to ((F (a) = F (c) \land F (b) = F (d)) \to (a N b \leftrightarrow c N d))$
8		fveq2	$⊢ c = X \to F (c) = F (X)$
9	8	breq1d	$⊢ c = X \to (F (c) \underset{˙}{\leq} F (d) \leftrightarrow F (X) \underset{˙}{\leq} F (d))$
10		breq1	$⊢ c = X \to (c N d \leftrightarrow X N d)$
11	9 10	bibi12d	$⊢ c = X \to ((F (c) \underset{˙}{\leq} F (d) \leftrightarrow c N d) \leftrightarrow (F (X) \underset{˙}{\leq} F (d) \leftrightarrow X N d))$
12	11	imbi2d	$⊢ c = X \to ((φ \to (F (c) \underset{˙}{\leq} F (d) \leftrightarrow c N d)) \leftrightarrow (φ \to (F (X) \underset{˙}{\leq} F (d) \leftrightarrow X N d)))$
13		fveq2	$⊢ d = Y \to F (d) = F (Y)$
14	13	breq2d	$⊢ d = Y \to (F (X) \underset{˙}{\leq} F (d) \leftrightarrow F (X) \underset{˙}{\leq} F (Y))$
15		breq2	$⊢ d = Y \to (X N d \leftrightarrow X N Y)$
16	14 15	bibi12d	$⊢ d = Y \to ((F (X) \underset{˙}{\leq} F (d) \leftrightarrow X N d) \leftrightarrow (F (X) \underset{˙}{\leq} F (Y) \leftrightarrow X N Y))$
17	16	imbi2d	$⊢ d = Y \to ((φ \to (F (X) \underset{˙}{\leq} F (d) \leftrightarrow X N d)) \leftrightarrow (φ \to (F (X) \underset{˙}{\leq} F (Y) \leftrightarrow X N Y)))$
18		fofn	$⊢ F : V \underset{onto}{⟶} B \to F Fn V$
19	3 18	syl	$⊢ φ \to F Fn V$
20	19	adantr	$⊢ (φ \land (c \in V \land d \in V)) \to F Fn V$
21	20	fndmd	$⊢ (φ \land (c \in V \land d \in V)) \to dom F = V$
22	21	rexeqdv	$⊢ (φ \land (c \in V \land d \in V)) \to (\exists a \in dom F (a F F (c) \land a (F \circ N) F (d)) \leftrightarrow \exists a \in V (a F F (c) \land a (F \circ N) F (d)))$
23		fnbrfvb	$⊢ (F Fn V \land a \in V) \to (F (a) = F (c) \leftrightarrow a F F (c))$
24	20 23	sylan	$⊢ ((φ \land (c \in V \land d \in V)) \land a \in V) \to (F (a) = F (c) \leftrightarrow a F F (c))$
25	24	anbi1d	$⊢ ((φ \land (c \in V \land d \in V)) \land a \in V) \to ((F (a) = F (c) \land a (F \circ N) F (d)) \leftrightarrow (a F F (c) \land a (F \circ N) F (d)))$
26		ancom	$⊢ (a N b \land b F F (d)) \leftrightarrow (b F F (d) \land a N b)$
27		vex	$⊢ b \in V$
28		fvex	$⊢ F (d) \in V$
29	27 28	breldm	$⊢ b F F (d) \to b \in dom F$
30	29	adantr	$⊢ (b F F (d) \land a N b) \to b \in dom F$
31	30	pm4.71ri	$⊢ (b F F (d) \land a N b) \leftrightarrow (b \in dom F \land (b F F (d) \land a N b))$
32	26 31	bitri	$⊢ (a N b \land b F F (d)) \leftrightarrow (b \in dom F \land (b F F (d) \land a N b))$
33	32	exbii	$⊢ \exists b (a N b \land b F F (d)) \leftrightarrow \exists b (b \in dom F \land (b F F (d) \land a N b))$
34		vex	$⊢ a \in V$
35	34 28	brco	$⊢ a (F \circ N) F (d) \leftrightarrow \exists b (a N b \land b F F (d))$
36		df-rex	$⊢ \exists b \in dom F (b F F (d) \land a N b) \leftrightarrow \exists b (b \in dom F \land (b F F (d) \land a N b))$
37	33 35 36	3bitr4i	$⊢ a (F \circ N) F (d) \leftrightarrow \exists b \in dom F (b F F (d) \land a N b)$
38	20	ad2antrr	$⊢ (((φ \land (c \in V \land d \in V)) \land a \in V) \land F (a) = F (c)) \to F Fn V$
39		fnbrfvb	$⊢ (F Fn V \land b \in V) \to (F (b) = F (d) \leftrightarrow b F F (d))$
40	38 39	sylan	$⊢ ((((φ \land (c \in V \land d \in V)) \land a \in V) \land F (a) = F (c)) \land b \in V) \to (F (b) = F (d) \leftrightarrow b F F (d))$
41	40	anbi1d	$⊢ ((((φ \land (c \in V \land d \in V)) \land a \in V) \land F (a) = F (c)) \land b \in V) \to ((F (b) = F (d) \land a N b) \leftrightarrow (b F F (d) \land a N b))$
42	7	3expa	$⊢ ((φ \land (a \in V \land b \in V)) \land (c \in V \land d \in V)) \to ((F (a) = F (c) \land F (b) = F (d)) \to (a N b \leftrightarrow c N d))$
43	42	an32s	$⊢ ((φ \land (c \in V \land d \in V)) \land (a \in V \land b \in V)) \to ((F (a) = F (c) \land F (b) = F (d)) \to (a N b \leftrightarrow c N d))$
44	43	anassrs	$⊢ (((φ \land (c \in V \land d \in V)) \land a \in V) \land b \in V) \to ((F (a) = F (c) \land F (b) = F (d)) \to (a N b \leftrightarrow c N d))$
45	44	impl	$⊢ (((((φ \land (c \in V \land d \in V)) \land a \in V) \land b \in V) \land F (a) = F (c)) \land F (b) = F (d)) \to (a N b \leftrightarrow c N d)$
46	45	pm5.32da	$⊢ ((((φ \land (c \in V \land d \in V)) \land a \in V) \land b \in V) \land F (a) = F (c)) \to ((F (b) = F (d) \land a N b) \leftrightarrow (F (b) = F (d) \land c N d))$
47	46	an32s	$⊢ ((((φ \land (c \in V \land d \in V)) \land a \in V) \land F (a) = F (c)) \land b \in V) \to ((F (b) = F (d) \land a N b) \leftrightarrow (F (b) = F (d) \land c N d))$
48	41 47	bitr3d	$⊢ ((((φ \land (c \in V \land d \in V)) \land a \in V) \land F (a) = F (c)) \land b \in V) \to ((b F F (d) \land a N b) \leftrightarrow (F (b) = F (d) \land c N d))$
49	48	rexbidva	$⊢ (((φ \land (c \in V \land d \in V)) \land a \in V) \land F (a) = F (c)) \to (\exists b \in V (b F F (d) \land a N b) \leftrightarrow \exists b \in V (F (b) = F (d) \land c N d))$
50		r19.41v	$⊢ \exists b \in V (F (b) = F (d) \land c N d) \leftrightarrow (\exists b \in V F (b) = F (d) \land c N d)$
51	49 50	bitrdi	$⊢ (((φ \land (c \in V \land d \in V)) \land a \in V) \land F (a) = F (c)) \to (\exists b \in V (b F F (d) \land a N b) \leftrightarrow (\exists b \in V F (b) = F (d) \land c N d))$
52	21	rexeqdv	$⊢ (φ \land (c \in V \land d \in V)) \to (\exists b \in dom F (b F F (d) \land a N b) \leftrightarrow \exists b \in V (b F F (d) \land a N b))$
53	52	ad2antrr	$⊢ (((φ \land (c \in V \land d \in V)) \land a \in V) \land F (a) = F (c)) \to (\exists b \in dom F (b F F (d) \land a N b) \leftrightarrow \exists b \in V (b F F (d) \land a N b))$
54		simprr	$⊢ (φ \land (c \in V \land d \in V)) \to d \in V$
55		eqid	$⊢ F (d) = F (d)$
56		fveqeq2	$⊢ b = d \to (F (b) = F (d) \leftrightarrow F (d) = F (d))$
57	56	rspcev	$⊢ (d \in V \land F (d) = F (d)) \to \exists b \in V F (b) = F (d)$
58	54 55 57	sylancl	$⊢ (φ \land (c \in V \land d \in V)) \to \exists b \in V F (b) = F (d)$
59	58	biantrurd	$⊢ (φ \land (c \in V \land d \in V)) \to (c N d \leftrightarrow (\exists b \in V F (b) = F (d) \land c N d))$
60	59	ad2antrr	$⊢ (((φ \land (c \in V \land d \in V)) \land a \in V) \land F (a) = F (c)) \to (c N d \leftrightarrow (\exists b \in V F (b) = F (d) \land c N d))$
61	51 53 60	3bitr4d	$⊢ (((φ \land (c \in V \land d \in V)) \land a \in V) \land F (a) = F (c)) \to (\exists b \in dom F (b F F (d) \land a N b) \leftrightarrow c N d)$
62	37 61	syl5bb	$⊢ (((φ \land (c \in V \land d \in V)) \land a \in V) \land F (a) = F (c)) \to (a (F \circ N) F (d) \leftrightarrow c N d)$
63	62	pm5.32da	$⊢ ((φ \land (c \in V \land d \in V)) \land a \in V) \to ((F (a) = F (c) \land a (F \circ N) F (d)) \leftrightarrow (F (a) = F (c) \land c N d))$
64	25 63	bitr3d	$⊢ ((φ \land (c \in V \land d \in V)) \land a \in V) \to ((a F F (c) \land a (F \circ N) F (d)) \leftrightarrow (F (a) = F (c) \land c N d))$
65	64	rexbidva	$⊢ (φ \land (c \in V \land d \in V)) \to (\exists a \in V (a F F (c) \land a (F \circ N) F (d)) \leftrightarrow \exists a \in V (F (a) = F (c) \land c N d))$
66	22 65	bitrd	$⊢ (φ \land (c \in V \land d \in V)) \to (\exists a \in dom F (a F F (c) \land a (F \circ N) F (d)) \leftrightarrow \exists a \in V (F (a) = F (c) \land c N d))$
67		fvex	$⊢ F (c) \in V$
68	67 34	brcnv	$⊢ F (c) F^{-1} a \leftrightarrow a F F (c)$
69	68	anbi1i	$⊢ (F (c) F^{-1} a \land a (F \circ N) F (d)) \leftrightarrow (a F F (c) \land a (F \circ N) F (d))$
70	34 67	breldm	$⊢ a F F (c) \to a \in dom F$
71	70	adantr	$⊢ (a F F (c) \land a (F \circ N) F (d)) \to a \in dom F$
72	71	pm4.71ri	$⊢ (a F F (c) \land a (F \circ N) F (d)) \leftrightarrow (a \in dom F \land (a F F (c) \land a (F \circ N) F (d)))$
73	69 72	bitri	$⊢ (F (c) F^{-1} a \land a (F \circ N) F (d)) \leftrightarrow (a \in dom F \land (a F F (c) \land a (F \circ N) F (d)))$
74	73	exbii	$⊢ \exists a (F (c) F^{-1} a \land a (F \circ N) F (d)) \leftrightarrow \exists a (a \in dom F \land (a F F (c) \land a (F \circ N) F (d)))$
75	67 28	brco	$⊢ F (c) ((F \circ N) \circ F^{-1}) F (d) \leftrightarrow \exists a (F (c) F^{-1} a \land a (F \circ N) F (d))$
76		df-rex	$⊢ \exists a \in dom F (a F F (c) \land a (F \circ N) F (d)) \leftrightarrow \exists a (a \in dom F \land (a F F (c) \land a (F \circ N) F (d)))$
77	74 75 76	3bitr4ri	$⊢ \exists a \in dom F (a F F (c) \land a (F \circ N) F (d)) \leftrightarrow F (c) ((F \circ N) \circ F^{-1}) F (d)$
78		r19.41v	$⊢ \exists a \in V (F (a) = F (c) \land c N d) \leftrightarrow (\exists a \in V F (a) = F (c) \land c N d)$
79	66 77 78	3bitr3g	$⊢ (φ \land (c \in V \land d \in V)) \to (F (c) ((F \circ N) \circ F^{-1}) F (d) \leftrightarrow (\exists a \in V F (a) = F (c) \land c N d))$
80	1 2 3 4 6 5	imasle	$⊢ φ \to \underset{˙}{\leq} = (F \circ N) \circ F^{-1}$
81	80	adantr	$⊢ (φ \land (c \in V \land d \in V)) \to \underset{˙}{\leq} = (F \circ N) \circ F^{-1}$
82	81	breqd	$⊢ (φ \land (c \in V \land d \in V)) \to (F (c) \underset{˙}{\leq} F (d) \leftrightarrow F (c) ((F \circ N) \circ F^{-1}) F (d))$
83		simprl	$⊢ (φ \land (c \in V \land d \in V)) \to c \in V$
84		eqid	$⊢ F (c) = F (c)$
85		fveqeq2	$⊢ a = c \to (F (a) = F (c) \leftrightarrow F (c) = F (c))$
86	85	rspcev	$⊢ (c \in V \land F (c) = F (c)) \to \exists a \in V F (a) = F (c)$
87	83 84 86	sylancl	$⊢ (φ \land (c \in V \land d \in V)) \to \exists a \in V F (a) = F (c)$
88	87	biantrurd	$⊢ (φ \land (c \in V \land d \in V)) \to (c N d \leftrightarrow (\exists a \in V F (a) = F (c) \land c N d))$
89	79 82 88	3bitr4d	$⊢ (φ \land (c \in V \land d \in V)) \to (F (c) \underset{˙}{\leq} F (d) \leftrightarrow c N d)$
90	89	expcom	$⊢ (c \in V \land d \in V) \to (φ \to (F (c) \underset{˙}{\leq} F (d) \leftrightarrow c N d))$
91	12 17 90	vtocl2ga	$⊢ (X \in V \land Y \in V) \to (φ \to (F (X) \underset{˙}{\leq} F (Y) \leftrightarrow X N Y))$
92	91	com12	$⊢ φ \to ((X \in V \land Y \in V) \to (F (X) \underset{˙}{\leq} F (Y) \leftrightarrow X N Y))$
93	92	3impib	$⊢ (φ \land X \in V \land Y \in V) \to (F (X) \underset{˙}{\leq} F (Y) \leftrightarrow X N Y)$

Metamath Proof Explorer

Theorem imasleval

Proof