wessf1ornlem

Description: Given a function F on a well-ordered domain A there exists a subset of A such that F restricted to such subset is injective and onto the range of F (without using the axiom of choice). (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	wessf1ornlem.f	$⊢ φ \to F Fn A$
	wessf1ornlem.a	$⊢ φ \to A \in V$
	wessf1ornlem.r	$⊢ φ \to R We A$
	wessf1ornlem.g	$⊢ G = (y \in ran F ⟼ (ι x \in F^{-1} [\{y\}] \| \forall z \in F^{-1} [\{y\}] \neg z R x))$
Assertion	wessf1ornlem	$⊢ φ \to \exists x \in 𝒫 A ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} ran F$

Proof

Step	Hyp	Ref	Expression
1		wessf1ornlem.f	$⊢ φ \to F Fn A$
2		wessf1ornlem.a	$⊢ φ \to A \in V$
3		wessf1ornlem.r	$⊢ φ \to R We A$
4		wessf1ornlem.g	$⊢ G = (y \in ran F ⟼ (ι x \in F^{-1} [\{y\}] \| \forall z \in F^{-1} [\{y\}] \neg z R x))$
5		cnvimass	$⊢ F^{-1} [\{u\}] \subseteq dom F$
6	1	fndmd	$⊢ φ \to dom F = A$
7	6	adantr	$⊢ (φ \land u \in ran F) \to dom F = A$
8	5 7	sseqtrid	$⊢ (φ \land u \in ran F) \to F^{-1} [\{u\}] \subseteq A$
9	3	adantr	$⊢ (φ \land u \in ran F) \to R We A$
10	5 6	sseqtrid	$⊢ φ \to F^{-1} [\{u\}] \subseteq A$
11	2 10	ssexd	$⊢ φ \to F^{-1} [\{u\}] \in V$
12	11	adantr	$⊢ (φ \land u \in ran F) \to F^{-1} [\{u\}] \in V$
13		inisegn0	$⊢ u \in ran F \leftrightarrow F^{-1} [\{u\}] \neq \emptyset$
14	13	bilani	$⊢ (φ \land u \in ran F) \to F^{-1} [\{u\}] \neq \emptyset$
15		wereu	$⊢ (R We A \land (F^{-1} [\{u\}] \in V \land F^{-1} [\{u\}] \subseteq A \land F^{-1} [\{u\}] \neq \emptyset)) \to \exists! v \in F^{-1} [\{u\}] \forall t \in F^{-1} [\{u\}] \neg t R v$
16	9 12 8 14 15	syl13anc	$⊢ (φ \land u \in ran F) \to \exists! v \in F^{-1} [\{u\}] \forall t \in F^{-1} [\{u\}] \neg t R v$
17		riotacl	$⊢ \exists! v \in F^{-1} [\{u\}] \forall t \in F^{-1} [\{u\}] \neg t R v \to (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v) \in F^{-1} [\{u\}]$
18	16 17	syl	$⊢ (φ \land u \in ran F) \to (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v) \in F^{-1} [\{u\}]$
19	8 18	sseldd	$⊢ (φ \land u \in ran F) \to (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v) \in A$
20	19	ralrimiva	$⊢ φ \to \forall u \in ran F (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v) \in A$
21		sneq	$⊢ y = u \to \{y\} = \{u\}$
22	21	imaeq2d	$⊢ y = u \to F^{-1} [\{y\}] = F^{-1} [\{u\}]$
23	22	raleqdv	$⊢ y = u \to (\forall z \in F^{-1} [\{y\}] \neg z R x \leftrightarrow \forall z \in F^{-1} [\{u\}] \neg z R x)$
24	22 23	riotaeqbidv	$⊢ y = u \to (ι x \in F^{-1} [\{y\}] \| \forall z \in F^{-1} [\{y\}] \neg z R x) = (ι x \in F^{-1} [\{u\}] \| \forall z \in F^{-1} [\{u\}] \neg z R x)$
25		breq1	$⊢ z = t \to (z R x \leftrightarrow t R x)$
26	25	notbid	$⊢ z = t \to (\neg z R x \leftrightarrow \neg t R x)$
27	26	cbvralvw	$⊢ \forall z \in F^{-1} [\{u\}] \neg z R x \leftrightarrow \forall t \in F^{-1} [\{u\}] \neg t R x$
28		breq2	$⊢ x = v \to (t R x \leftrightarrow t R v)$
29	28	notbid	$⊢ x = v \to (\neg t R x \leftrightarrow \neg t R v)$
30	29	ralbidv	$⊢ x = v \to (\forall t \in F^{-1} [\{u\}] \neg t R x \leftrightarrow \forall t \in F^{-1} [\{u\}] \neg t R v)$
31	27 30	bitrid	$⊢ x = v \to (\forall z \in F^{-1} [\{u\}] \neg z R x \leftrightarrow \forall t \in F^{-1} [\{u\}] \neg t R v)$
32	31	cbvriotavw	$⊢ (ι x \in F^{-1} [\{u\}] \| \forall z \in F^{-1} [\{u\}] \neg z R x) = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)$
33	24 32	eqtrdi	$⊢ y = u \to (ι x \in F^{-1} [\{y\}] \| \forall z \in F^{-1} [\{y\}] \neg z R x) = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)$
34	33	cbvmptv	$⊢ (y \in ran F ⟼ (ι x \in F^{-1} [\{y\}] \| \forall z \in F^{-1} [\{y\}] \neg z R x)) = (u \in ran F ⟼ (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v))$
35	4 34	eqtri	$⊢ G = (u \in ran F ⟼ (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v))$
36	35	rnmptss	$⊢ \forall u \in ran F (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v) \in A \to ran G \subseteq A$
37	20 36	syl	$⊢ φ \to ran G \subseteq A$
38	2 37	sselpwd	$⊢ φ \to ran G \in 𝒫 A$
39		dffn3	$⊢ F Fn A \leftrightarrow F : A ⟶ ran F$
40	1 39	sylib	$⊢ φ \to F : A ⟶ ran F$
41	40 37	fssresd	$⊢ φ \to ({F ↾}_{ran G}) : ran G ⟶ ran F$
42		fvres	$⊢ w \in ran G \to ({F ↾}_{ran G}) (w) = F (w)$
43	42	eqcomd	$⊢ w \in ran G \to F (w) = ({F ↾}_{ran G}) (w)$
44	43	ad2antrr	$⊢ ((w \in ran G \land t \in ran G) \land ({F ↾}_{ran G}) (w) = ({F ↾}_{ran G}) (t)) \to F (w) = ({F ↾}_{ran G}) (w)$
45		simpr	$⊢ ((w \in ran G \land t \in ran G) \land ({F ↾}_{ran G}) (w) = ({F ↾}_{ran G}) (t)) \to ({F ↾}_{ran G}) (w) = ({F ↾}_{ran G}) (t)$
46		fvres	$⊢ t \in ran G \to ({F ↾}_{ran G}) (t) = F (t)$
47	46	ad2antlr	$⊢ ((w \in ran G \land t \in ran G) \land ({F ↾}_{ran G}) (w) = ({F ↾}_{ran G}) (t)) \to ({F ↾}_{ran G}) (t) = F (t)$
48	44 45 47	3eqtrd	$⊢ ((w \in ran G \land t \in ran G) \land ({F ↾}_{ran G}) (w) = ({F ↾}_{ran G}) (t)) \to F (w) = F (t)$
49	48	3adantl1	$⊢ ((φ \land w \in ran G \land t \in ran G) \land ({F ↾}_{ran G}) (w) = ({F ↾}_{ran G}) (t)) \to F (w) = F (t)$
50		simpl1	$⊢ ((φ \land w \in ran G \land t \in ran G) \land F (w) = F (t)) \to φ$
51		simpl3	$⊢ ((φ \land w \in ran G \land t \in ran G) \land F (w) = F (t)) \to t \in ran G$
52		simpl2	$⊢ ((φ \land w \in ran G \land t \in ran G) \land F (w) = F (t)) \to w \in ran G$
53		id	$⊢ F (w) = F (t) \to F (w) = F (t)$
54	53	eqcomd	$⊢ F (w) = F (t) \to F (t) = F (w)$
55	54	adantl	$⊢ ((φ \land w \in ran G \land t \in ran G) \land F (w) = F (t)) \to F (t) = F (w)$
56		eleq1w	$⊢ b = w \to (b \in ran G \leftrightarrow w \in ran G)$
57	56	3anbi3d	$⊢ b = w \to ((φ \land t \in ran G \land b \in ran G) \leftrightarrow (φ \land t \in ran G \land w \in ran G))$
58		fveq2	$⊢ b = w \to F (b) = F (w)$
59	58	eqeq2d	$⊢ b = w \to (F (t) = F (b) \leftrightarrow F (t) = F (w))$
60	57 59	anbi12d	$⊢ b = w \to (((φ \land t \in ran G \land b \in ran G) \land F (t) = F (b)) \leftrightarrow ((φ \land t \in ran G \land w \in ran G) \land F (t) = F (w)))$
61		breq1	$⊢ b = w \to (b R t \leftrightarrow w R t)$
62	61	notbid	$⊢ b = w \to (\neg b R t \leftrightarrow \neg w R t)$
63	60 62	imbi12d	$⊢ b = w \to ((((φ \land t \in ran G \land b \in ran G) \land F (t) = F (b)) \to \neg b R t) \leftrightarrow (((φ \land t \in ran G \land w \in ran G) \land F (t) = F (w)) \to \neg w R t))$
64		eleq1w	$⊢ a = t \to (a \in ran G \leftrightarrow t \in ran G)$
65	64	3anbi2d	$⊢ a = t \to ((φ \land a \in ran G \land b \in ran G) \leftrightarrow (φ \land t \in ran G \land b \in ran G))$
66		fveqeq2	$⊢ a = t \to (F (a) = F (b) \leftrightarrow F (t) = F (b))$
67	65 66	anbi12d	$⊢ a = t \to (((φ \land a \in ran G \land b \in ran G) \land F (a) = F (b)) \leftrightarrow ((φ \land t \in ran G \land b \in ran G) \land F (t) = F (b)))$
68		breq2	$⊢ a = t \to (b R a \leftrightarrow b R t)$
69	68	notbid	$⊢ a = t \to (\neg b R a \leftrightarrow \neg b R t)$
70	67 69	imbi12d	$⊢ a = t \to ((((φ \land a \in ran G \land b \in ran G) \land F (a) = F (b)) \to \neg b R a) \leftrightarrow (((φ \land t \in ran G \land b \in ran G) \land F (t) = F (b)) \to \neg b R t))$
71		eleq1w	$⊢ t = b \to (t \in ran G \leftrightarrow b \in ran G)$
72	71	3anbi3d	$⊢ t = b \to ((φ \land a \in ran G \land t \in ran G) \leftrightarrow (φ \land a \in ran G \land b \in ran G))$
73		fveq2	$⊢ t = b \to F (t) = F (b)$
74	73	eqeq2d	$⊢ t = b \to (F (a) = F (t) \leftrightarrow F (a) = F (b))$
75	72 74	anbi12d	$⊢ t = b \to (((φ \land a \in ran G \land t \in ran G) \land F (a) = F (t)) \leftrightarrow ((φ \land a \in ran G \land b \in ran G) \land F (a) = F (b)))$
76		breq1	$⊢ t = b \to (t R a \leftrightarrow b R a)$
77	76	notbid	$⊢ t = b \to (\neg t R a \leftrightarrow \neg b R a)$
78	75 77	imbi12d	$⊢ t = b \to ((((φ \land a \in ran G \land t \in ran G) \land F (a) = F (t)) \to \neg t R a) \leftrightarrow (((φ \land a \in ran G \land b \in ran G) \land F (a) = F (b)) \to \neg b R a))$
79		eleq1w	$⊢ w = a \to (w \in ran G \leftrightarrow a \in ran G)$
80	79	3anbi2d	$⊢ w = a \to ((φ \land w \in ran G \land t \in ran G) \leftrightarrow (φ \land a \in ran G \land t \in ran G))$
81		fveqeq2	$⊢ w = a \to (F (w) = F (t) \leftrightarrow F (a) = F (t))$
82	80 81	anbi12d	$⊢ w = a \to (((φ \land w \in ran G \land t \in ran G) \land F (w) = F (t)) \leftrightarrow ((φ \land a \in ran G \land t \in ran G) \land F (a) = F (t)))$
83		breq2	$⊢ w = a \to (t R w \leftrightarrow t R a)$
84	83	notbid	$⊢ w = a \to (\neg t R w \leftrightarrow \neg t R a)$
85	82 84	imbi12d	$⊢ w = a \to ((((φ \land w \in ran G \land t \in ran G) \land F (w) = F (t)) \to \neg t R w) \leftrightarrow (((φ \land a \in ran G \land t \in ran G) \land F (a) = F (t)) \to \neg t R a))$
86	35	elrnmpt	$⊢ w \in V \to (w \in ran G \leftrightarrow \exists u \in ran F w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v))$
87	86	elv	$⊢ w \in ran G \leftrightarrow \exists u \in ran F w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)$
88	87	birani	$⊢ (w \in ran G \land F (w) = F (t)) \to \exists u \in ran F w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)$
89	88	3ad2antl2	$⊢ ((φ \land w \in ran G \land t \in ran G) \land F (w) = F (t)) \to \exists u \in ran F w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)$
90		simp3	$⊢ ((φ \land w \in ran G \land t \in ran G) \land u \in ran F \land w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)) \to w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)$
91	90	eqcomd	$⊢ ((φ \land w \in ran G \land t \in ran G) \land u \in ran F \land w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)) \to (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v) = w$
92		simp11	$⊢ ((φ \land w \in ran G \land t \in ran G) \land u \in ran F \land w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)) \to φ$
93		id	$⊢ w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v) \to w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)$
94		breq2	$⊢ v = w \to (t R v \leftrightarrow t R w)$
95	94	notbid	$⊢ v = w \to (\neg t R v \leftrightarrow \neg t R w)$
96	95	ralbidv	$⊢ v = w \to (\forall t \in F^{-1} [\{u\}] \neg t R v \leftrightarrow \forall t \in F^{-1} [\{u\}] \neg t R w)$
97	96	cbvriotavw	$⊢ (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v) = (ι w \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R w)$
98	93 97	eqtr2di	$⊢ w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v) \to (ι w \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R w) = w$
99	98	3ad2ant3	$⊢ (φ \land u \in ran F \land w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)) \to (ι w \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R w) = w$
100	96	cbvreuvw	$⊢ \exists! v \in F^{-1} [\{u\}] \forall t \in F^{-1} [\{u\}] \neg t R v \leftrightarrow \exists! w \in F^{-1} [\{u\}] \forall t \in F^{-1} [\{u\}] \neg t R w$
101	16 100	sylib	$⊢ (φ \land u \in ran F) \to \exists! w \in F^{-1} [\{u\}] \forall t \in F^{-1} [\{u\}] \neg t R w$
102		riota1	$⊢ \exists! w \in F^{-1} [\{u\}] \forall t \in F^{-1} [\{u\}] \neg t R w \to ((w \in F^{-1} [\{u\}] \land \forall t \in F^{-1} [\{u\}] \neg t R w) \leftrightarrow (ι w \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R w) = w)$
103	101 102	syl	$⊢ (φ \land u \in ran F) \to ((w \in F^{-1} [\{u\}] \land \forall t \in F^{-1} [\{u\}] \neg t R w) \leftrightarrow (ι w \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R w) = w)$
104	103	3adant3	$⊢ (φ \land u \in ran F \land w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)) \to ((w \in F^{-1} [\{u\}] \land \forall t \in F^{-1} [\{u\}] \neg t R w) \leftrightarrow (ι w \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R w) = w)$
105	99 104	mpbird	$⊢ (φ \land u \in ran F \land w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)) \to (w \in F^{-1} [\{u\}] \land \forall t \in F^{-1} [\{u\}] \neg t R w)$
106	105	simpld	$⊢ (φ \land u \in ran F \land w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)) \to w \in F^{-1} [\{u\}]$
107	92 106	syld3an1	$⊢ ((φ \land w \in ran G \land t \in ran G) \land u \in ran F \land w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)) \to w \in F^{-1} [\{u\}]$
108		simp2	$⊢ ((φ \land w \in ran G \land t \in ran G) \land u \in ran F \land w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)) \to u \in ran F$
109	92 108 16	syl2anc	$⊢ ((φ \land w \in ran G \land t \in ran G) \land u \in ran F \land w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)) \to \exists! v \in F^{-1} [\{u\}] \forall t \in F^{-1} [\{u\}] \neg t R v$
110	96	riota2	$⊢ (w \in F^{-1} [\{u\}] \land \exists! v \in F^{-1} [\{u\}] \forall t \in F^{-1} [\{u\}] \neg t R v) \to (\forall t \in F^{-1} [\{u\}] \neg t R w \leftrightarrow (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v) = w)$
111	107 109 110	syl2anc	$⊢ ((φ \land w \in ran G \land t \in ran G) \land u \in ran F \land w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)) \to (\forall t \in F^{-1} [\{u\}] \neg t R w \leftrightarrow (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v) = w)$
112	91 111	mpbird	$⊢ ((φ \land w \in ran G \land t \in ran G) \land u \in ran F \land w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)) \to \forall t \in F^{-1} [\{u\}] \neg t R w$
113	112	3adant1r	$⊢ (((φ \land w \in ran G \land t \in ran G) \land F (w) = F (t)) \land u \in ran F \land w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)) \to \forall t \in F^{-1} [\{u\}] \neg t R w$
114	37	sselda	$⊢ (φ \land t \in ran G) \to t \in A$
115	114	3adant2	$⊢ (φ \land w \in ran G \land t \in ran G) \to t \in A$
116	115	adantr	$⊢ ((φ \land w \in ran G \land t \in ran G) \land F (w) = F (t)) \to t \in A$
117	116	3ad2ant1	$⊢ (((φ \land w \in ran G \land t \in ran G) \land F (w) = F (t)) \land u \in ran F \land w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)) \to t \in A$
118	54	ad2antlr	$⊢ (((φ \land w \in ran G \land t \in ran G) \land F (w) = F (t)) \land u \in ran F) \to F (t) = F (w)$
119	118	3adant3	$⊢ (((φ \land w \in ran G \land t \in ran G) \land F (w) = F (t)) \land u \in ran F \land w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)) \to F (t) = F (w)$
120		fniniseg	$⊢ F Fn A \to (w \in F^{-1} [\{u\}] \leftrightarrow (w \in A \land F (w) = u))$
121	92 1 120	3syl	$⊢ ((φ \land w \in ran G \land t \in ran G) \land u \in ran F \land w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)) \to (w \in F^{-1} [\{u\}] \leftrightarrow (w \in A \land F (w) = u))$
122	107 121	mpbid	$⊢ ((φ \land w \in ran G \land t \in ran G) \land u \in ran F \land w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)) \to (w \in A \land F (w) = u)$
123	122	simprd	$⊢ ((φ \land w \in ran G \land t \in ran G) \land u \in ran F \land w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)) \to F (w) = u$
124	123	3adant1r	$⊢ (((φ \land w \in ran G \land t \in ran G) \land F (w) = F (t)) \land u \in ran F \land w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)) \to F (w) = u$
125	119 124	eqtrd	$⊢ (((φ \land w \in ran G \land t \in ran G) \land F (w) = F (t)) \land u \in ran F \land w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)) \to F (t) = u$
126		fniniseg	$⊢ F Fn A \to (t \in F^{-1} [\{u\}] \leftrightarrow (t \in A \land F (t) = u))$
127	1 126	syl	$⊢ φ \to (t \in F^{-1} [\{u\}] \leftrightarrow (t \in A \land F (t) = u))$
128	127	3ad2ant1	$⊢ (φ \land w \in ran G \land t \in ran G) \to (t \in F^{-1} [\{u\}] \leftrightarrow (t \in A \land F (t) = u))$
129	128	ad2antrr	$⊢ (((φ \land w \in ran G \land t \in ran G) \land F (w) = F (t)) \land u \in ran F) \to (t \in F^{-1} [\{u\}] \leftrightarrow (t \in A \land F (t) = u))$
130	129	3adant3	$⊢ (((φ \land w \in ran G \land t \in ran G) \land F (w) = F (t)) \land u \in ran F \land w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)) \to (t \in F^{-1} [\{u\}] \leftrightarrow (t \in A \land F (t) = u))$
131	117 125 130	mpbir2and	$⊢ (((φ \land w \in ran G \land t \in ran G) \land F (w) = F (t)) \land u \in ran F \land w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)) \to t \in F^{-1} [\{u\}]$
132		rspa	$⊢ (\forall t \in F^{-1} [\{u\}] \neg t R w \land t \in F^{-1} [\{u\}]) \to \neg t R w$
133	113 131 132	syl2anc	$⊢ (((φ \land w \in ran G \land t \in ran G) \land F (w) = F (t)) \land u \in ran F \land w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)) \to \neg t R w$
134	133	rexlimdv3a	$⊢ ((φ \land w \in ran G \land t \in ran G) \land F (w) = F (t)) \to (\exists u \in ran F w = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v) \to \neg t R w)$
135	89 134	mpd	$⊢ ((φ \land w \in ran G \land t \in ran G) \land F (w) = F (t)) \to \neg t R w$
136	85 135	chvarvv	$⊢ ((φ \land a \in ran G \land t \in ran G) \land F (a) = F (t)) \to \neg t R a$
137	78 136	chvarvv	$⊢ ((φ \land a \in ran G \land b \in ran G) \land F (a) = F (b)) \to \neg b R a$
138	70 137	chvarvv	$⊢ ((φ \land t \in ran G \land b \in ran G) \land F (t) = F (b)) \to \neg b R t$
139	63 138	chvarvv	$⊢ ((φ \land t \in ran G \land w \in ran G) \land F (t) = F (w)) \to \neg w R t$
140	50 51 52 55 139	syl31anc	$⊢ ((φ \land w \in ran G \land t \in ran G) \land F (w) = F (t)) \to \neg w R t$
141		weso	$⊢ R We A \to R Or A$
142	3 141	syl	$⊢ φ \to R Or A$
143	142	adantr	$⊢ (φ \land F (w) = F (t)) \to R Or A$
144	143	3ad2antl1	$⊢ ((φ \land w \in ran G \land t \in ran G) \land F (w) = F (t)) \to R Or A$
145	37	sselda	$⊢ (φ \land w \in ran G) \to w \in A$
146	145	3adant3	$⊢ (φ \land w \in ran G \land t \in ran G) \to w \in A$
147	146	adantr	$⊢ ((φ \land w \in ran G \land t \in ran G) \land F (w) = F (t)) \to w \in A$
148		sotrieq2	$⊢ (R Or A \land (w \in A \land t \in A)) \to (w = t \leftrightarrow (\neg w R t \land \neg t R w))$
149	144 147 116 148	syl12anc	$⊢ ((φ \land w \in ran G \land t \in ran G) \land F (w) = F (t)) \to (w = t \leftrightarrow (\neg w R t \land \neg t R w))$
150	140 135 149	mpbir2and	$⊢ ((φ \land w \in ran G \land t \in ran G) \land F (w) = F (t)) \to w = t$
151	49 150	syldan	$⊢ ((φ \land w \in ran G \land t \in ran G) \land ({F ↾}_{ran G}) (w) = ({F ↾}_{ran G}) (t)) \to w = t$
152	151	ex	$⊢ (φ \land w \in ran G \land t \in ran G) \to (({F ↾}_{ran G}) (w) = ({F ↾}_{ran G}) (t) \to w = t)$
153	152	3expb	$⊢ (φ \land (w \in ran G \land t \in ran G)) \to (({F ↾}_{ran G}) (w) = ({F ↾}_{ran G}) (t) \to w = t)$
154	153	ralrimivva	$⊢ φ \to \forall w \in ran G \forall t \in ran G (({F ↾}_{ran G}) (w) = ({F ↾}_{ran G}) (t) \to w = t)$
155		dff13	$⊢ ({F ↾}_{ran G}) : ran G \underset{1-1}{⟶} ran F \leftrightarrow (({F ↾}_{ran G}) : ran G ⟶ ran F \land \forall w \in ran G \forall t \in ran G (({F ↾}_{ran G}) (w) = ({F ↾}_{ran G}) (t) \to w = t))$
156	41 154 155	sylanbrc	$⊢ φ \to ({F ↾}_{ran G}) : ran G \underset{1-1}{⟶} ran F$
157		riotaex	$⊢ (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v) \in V$
158	157	rgenw	$⊢ \forall u \in ran F (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v) \in V$
159	35	fnmpt	$⊢ \forall u \in ran F (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v) \in V \to G Fn ran F$
160	158 159	mp1i	$⊢ φ \to G Fn ran F$
161		dffn3	$⊢ G Fn ran F \leftrightarrow G : ran F ⟶ ran G$
162	160 161	sylib	$⊢ φ \to G : ran F ⟶ ran G$
163	162	ffvelcdmda	$⊢ (φ \land u \in ran F) \to G (u) \in ran G$
164	163	fvresd	$⊢ (φ \land u \in ran F) \to ({F ↾}_{ran G}) (G (u)) = F (G (u))$
165		simpr	$⊢ (φ \land u \in ran F) \to u \in ran F$
166	157	a1i	$⊢ (φ \land u \in ran F) \to (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v) \in V$
167	4 33 165 166	fvmptd3	$⊢ (φ \land u \in ran F) \to G (u) = (ι v \in F^{-1} [\{u\}] \| \forall t \in F^{-1} [\{u\}] \neg t R v)$
168	167 18	eqeltrd	$⊢ (φ \land u \in ran F) \to G (u) \in F^{-1} [\{u\}]$
169		fvex	$⊢ G (u) \in V$
170		eleq1	$⊢ w = G (u) \to (w \in F^{-1} [\{u\}] \leftrightarrow G (u) \in F^{-1} [\{u\}])$
171		eleq1	$⊢ w = G (u) \to (w \in A \leftrightarrow G (u) \in A)$
172		fveqeq2	$⊢ w = G (u) \to (F (w) = u \leftrightarrow F (G (u)) = u)$
173	171 172	anbi12d	$⊢ w = G (u) \to ((w \in A \land F (w) = u) \leftrightarrow (G (u) \in A \land F (G (u)) = u))$
174	170 173	bibi12d	$⊢ w = G (u) \to ((w \in F^{-1} [\{u\}] \leftrightarrow (w \in A \land F (w) = u)) \leftrightarrow (G (u) \in F^{-1} [\{u\}] \leftrightarrow (G (u) \in A \land F (G (u)) = u)))$
175	174	imbi2d	$⊢ w = G (u) \to ((φ \to (w \in F^{-1} [\{u\}] \leftrightarrow (w \in A \land F (w) = u))) \leftrightarrow (φ \to (G (u) \in F^{-1} [\{u\}] \leftrightarrow (G (u) \in A \land F (G (u)) = u))))$
176	1 120	syl	$⊢ φ \to (w \in F^{-1} [\{u\}] \leftrightarrow (w \in A \land F (w) = u))$
177	169 175 176	vtocl	$⊢ φ \to (G (u) \in F^{-1} [\{u\}] \leftrightarrow (G (u) \in A \land F (G (u)) = u))$
178	177	adantr	$⊢ (φ \land u \in ran F) \to (G (u) \in F^{-1} [\{u\}] \leftrightarrow (G (u) \in A \land F (G (u)) = u))$
179	168 178	mpbid	$⊢ (φ \land u \in ran F) \to (G (u) \in A \land F (G (u)) = u)$
180	179	simprd	$⊢ (φ \land u \in ran F) \to F (G (u)) = u$
181	164 180	eqtr2d	$⊢ (φ \land u \in ran F) \to u = ({F ↾}_{ran G}) (G (u))$
182		fveq2	$⊢ w = G (u) \to ({F ↾}_{ran G}) (w) = ({F ↾}_{ran G}) (G (u))$
183	182	rspceeqv	$⊢ (G (u) \in ran G \land u = ({F ↾}_{ran G}) (G (u))) \to \exists w \in ran G u = ({F ↾}_{ran G}) (w)$
184	163 181 183	syl2anc	$⊢ (φ \land u \in ran F) \to \exists w \in ran G u = ({F ↾}_{ran G}) (w)$
185	184	ralrimiva	$⊢ φ \to \forall u \in ran F \exists w \in ran G u = ({F ↾}_{ran G}) (w)$
186		dffo3	$⊢ ({F ↾}_{ran G}) : ran G \underset{onto}{⟶} ran F \leftrightarrow (({F ↾}_{ran G}) : ran G ⟶ ran F \land \forall u \in ran F \exists w \in ran G u = ({F ↾}_{ran G}) (w))$
187	41 185 186	sylanbrc	$⊢ φ \to ({F ↾}_{ran G}) : ran G \underset{onto}{⟶} ran F$
188		df-f1o	$⊢ ({F ↾}_{ran G}) : ran G \underset{1-1 onto}{⟶} ran F \leftrightarrow (({F ↾}_{ran G}) : ran G \underset{1-1}{⟶} ran F \land ({F ↾}_{ran G}) : ran G \underset{onto}{⟶} ran F)$
189	156 187 188	sylanbrc	$⊢ φ \to ({F ↾}_{ran G}) : ran G \underset{1-1 onto}{⟶} ran F$
190		reseq2	$⊢ v = ran G \to {F ↾}_{v} = {F ↾}_{ran G}$
191		id	$⊢ v = ran G \to v = ran G$
192		eqidd	$⊢ v = ran G \to ran F = ran F$
193	190 191 192	f1oeq123d	$⊢ v = ran G \to (({F ↾}_{v}) : v \underset{1-1 onto}{⟶} ran F \leftrightarrow ({F ↾}_{ran G}) : ran G \underset{1-1 onto}{⟶} ran F)$
194	193	rspcev	$⊢ (ran G \in 𝒫 A \land ({F ↾}_{ran G}) : ran G \underset{1-1 onto}{⟶} ran F) \to \exists v \in 𝒫 A ({F ↾}_{v}) : v \underset{1-1 onto}{⟶} ran F$
195	38 189 194	syl2anc	$⊢ φ \to \exists v \in 𝒫 A ({F ↾}_{v}) : v \underset{1-1 onto}{⟶} ran F$
196		reseq2	$⊢ v = x \to {F ↾}_{v} = {F ↾}_{x}$
197		id	$⊢ v = x \to v = x$
198		eqidd	$⊢ v = x \to ran F = ran F$
199	196 197 198	f1oeq123d	$⊢ v = x \to (({F ↾}_{v}) : v \underset{1-1 onto}{⟶} ran F \leftrightarrow ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} ran F)$
200	199	cbvrexvw	$⊢ \exists v \in 𝒫 A ({F ↾}_{v}) : v \underset{1-1 onto}{⟶} ran F \leftrightarrow \exists x \in 𝒫 A ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} ran F$
201	195 200	sylib	$⊢ φ \to \exists x \in 𝒫 A ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} ran F$

Metamath Proof Explorer

Theorem wessf1ornlem

Proof