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

Metamath Proof Explorer

Theorem wessf1ornlem

Proof