wemapwe

Description: Construct lexicographic order on a function space based on a reverse well-ordering of the indices and a well-ordering of the values. (Contributed by Mario Carneiro, 29-May-2015) (Revised by AV, 3-Jul-2019)

	Ref	Expression
Hypotheses	wemapwe.t	$⊢ T = \{⟨x, y⟩ \| \exists z \in A (x (z) S y (z) \land \forall w \in A (z R w \to x (w) = y (w)))\}$
	wemapwe.u	$⊢ U = \{x \in (B^{A}) \| {finSupp}_{Z} (x)\}$
	wemapwe.2	$⊢ φ \to R We A$
	wemapwe.3	$⊢ φ \to S We B$
	wemapwe.4	$⊢ φ \to B \neq \emptyset$
	wemapwe.5	$⊢ F = OrdIso (R, A)$
	wemapwe.6	$⊢ G = OrdIso (S, B)$
	wemapwe.7	$⊢ Z = G (\emptyset)$
Assertion	wemapwe	$⊢ φ \to T We U$

Proof

Step	Hyp	Ref	Expression
1		wemapwe.t	$⊢ T = \{⟨x, y⟩ \| \exists z \in A (x (z) S y (z) \land \forall w \in A (z R w \to x (w) = y (w)))\}$
2		wemapwe.u	$⊢ U = \{x \in (B^{A}) \| {finSupp}_{Z} (x)\}$
3		wemapwe.2	$⊢ φ \to R We A$
4		wemapwe.3	$⊢ φ \to S We B$
5		wemapwe.4	$⊢ φ \to B \neq \emptyset$
6		wemapwe.5	$⊢ F = OrdIso (R, A)$
7		wemapwe.6	$⊢ G = OrdIso (S, B)$
8		wemapwe.7	$⊢ Z = G (\emptyset)$
9		eqid	$⊢ \{x \in ({dom G}^{dom F}) \| {finSupp}_{G^{-1} (Z)} (x)\} = \{x \in ({dom G}^{dom F}) \| {finSupp}_{G^{-1} (Z)} (x)\}$
10		eqid	$⊢ G^{-1} (Z) = G^{-1} (Z)$
11		simprr	$⊢ (φ \land (B \in V \land A \in V)) \to A \in V$
12	3	adantr	$⊢ (φ \land (B \in V \land A \in V)) \to R We A$
13	6	oiiso	$⊢ (A \in V \land R We A) \to F {Isom}_{E, R} (dom F, A)$
14	11 12 13	syl2anc	$⊢ (φ \land (B \in V \land A \in V)) \to F {Isom}_{E, R} (dom F, A)$
15		isof1o	$⊢ F {Isom}_{E, R} (dom F, A) \to F : dom F \underset{1-1 onto}{⟶} A$
16	14 15	syl	$⊢ (φ \land (B \in V \land A \in V)) \to F : dom F \underset{1-1 onto}{⟶} A$
17		simprl	$⊢ (φ \land (B \in V \land A \in V)) \to B \in V$
18	4	adantr	$⊢ (φ \land (B \in V \land A \in V)) \to S We B$
19	7	oiiso	$⊢ (B \in V \land S We B) \to G {Isom}_{E, S} (dom G, B)$
20	17 18 19	syl2anc	$⊢ (φ \land (B \in V \land A \in V)) \to G {Isom}_{E, S} (dom G, B)$
21		isof1o	$⊢ G {Isom}_{E, S} (dom G, B) \to G : dom G \underset{1-1 onto}{⟶} B$
22		f1ocnv	$⊢ G : dom G \underset{1-1 onto}{⟶} B \to G^{-1} : B \underset{1-1 onto}{⟶} dom G$
23	20 21 22	3syl	$⊢ (φ \land (B \in V \land A \in V)) \to G^{-1} : B \underset{1-1 onto}{⟶} dom G$
24	6	oiexg	$⊢ A \in V \to F \in V$
25	24	ad2antll	$⊢ (φ \land (B \in V \land A \in V)) \to F \in V$
26	25	dmexd	$⊢ (φ \land (B \in V \land A \in V)) \to dom F \in V$
27	7	oiexg	$⊢ B \in V \to G \in V$
28	27	ad2antrl	$⊢ (φ \land (B \in V \land A \in V)) \to G \in V$
29	28	dmexd	$⊢ (φ \land (B \in V \land A \in V)) \to dom G \in V$
30	20 21	syl	$⊢ (φ \land (B \in V \land A \in V)) \to G : dom G \underset{1-1 onto}{⟶} B$
31		f1ofo	$⊢ G : dom G \underset{1-1 onto}{⟶} B \to G : dom G \underset{onto}{⟶} B$
32		forn	$⊢ G : dom G \underset{onto}{⟶} B \to ran G = B$
33	30 31 32	3syl	$⊢ (φ \land (B \in V \land A \in V)) \to ran G = B$
34	5	adantr	$⊢ (φ \land (B \in V \land A \in V)) \to B \neq \emptyset$
35	33 34	eqnetrd	$⊢ (φ \land (B \in V \land A \in V)) \to ran G \neq \emptyset$
36		dm0rn0	$⊢ dom G = \emptyset \leftrightarrow ran G = \emptyset$
37	36	necon3bii	$⊢ dom G \neq \emptyset \leftrightarrow ran G \neq \emptyset$
38	35 37	sylibr	$⊢ (φ \land (B \in V \land A \in V)) \to dom G \neq \emptyset$
39	7	oicl	$⊢ Ord dom G$
40		ord0eln0	$⊢ Ord dom G \to (\emptyset \in dom G \leftrightarrow dom G \neq \emptyset)$
41	39 40	ax-mp	$⊢ \emptyset \in dom G \leftrightarrow dom G \neq \emptyset$
42	38 41	sylibr	$⊢ (φ \land (B \in V \land A \in V)) \to \emptyset \in dom G$
43	7	oif	$⊢ G : dom G ⟶ B$
44	43	ffvelcdmi	$⊢ \emptyset \in dom G \to G (\emptyset) \in B$
45	42 44	syl	$⊢ (φ \land (B \in V \land A \in V)) \to G (\emptyset) \in B$
46	8 45	eqeltrid	$⊢ (φ \land (B \in V \land A \in V)) \to Z \in B$
47	2 9 10 16 23 11 17 26 29 46	mapfien	$⊢ (φ \land (B \in V \land A \in V)) \to (f \in U ⟼ G^{-1} \circ (f \circ F)) : U \underset{1-1 onto}{⟶} \{x \in ({dom G}^{dom F}) \| {finSupp}_{G^{-1} (Z)} (x)\}$
48		eqid	$⊢ \{x \in ({dom G}^{dom F}) \| {finSupp}_{\emptyset} (x)\} = \{x \in ({dom G}^{dom F}) \| {finSupp}_{\emptyset} (x)\}$
49	7	oion	$⊢ B \in V \to dom G \in On$
50	49	ad2antrl	$⊢ (φ \land (B \in V \land A \in V)) \to dom G \in On$
51	6	oion	$⊢ A \in V \to dom F \in On$
52	51	ad2antll	$⊢ (φ \land (B \in V \land A \in V)) \to dom F \in On$
53	48 50 52	cantnfdm	$⊢ (φ \land (B \in V \land A \in V)) \to dom (dom G CNF dom F) = \{x \in ({dom G}^{dom F}) \| {finSupp}_{\emptyset} (x)\}$
54	8	fveq2i	$⊢ G^{-1} (Z) = G^{-1} (G (\emptyset))$
55		f1ocnvfv1	$⊢ (G : dom G \underset{1-1 onto}{⟶} B \land \emptyset \in dom G) \to G^{-1} (G (\emptyset)) = \emptyset$
56	30 42 55	syl2anc	$⊢ (φ \land (B \in V \land A \in V)) \to G^{-1} (G (\emptyset)) = \emptyset$
57	54 56	eqtrid	$⊢ (φ \land (B \in V \land A \in V)) \to G^{-1} (Z) = \emptyset$
58	57	breq2d	$⊢ (φ \land (B \in V \land A \in V)) \to ({finSupp}_{G^{-1} (Z)} (x) \leftrightarrow {finSupp}_{\emptyset} (x))$
59	58	rabbidv	$⊢ (φ \land (B \in V \land A \in V)) \to \{x \in ({dom G}^{dom F}) \| {finSupp}_{G^{-1} (Z)} (x)\} = \{x \in ({dom G}^{dom F}) \| {finSupp}_{\emptyset} (x)\}$
60	53 59	eqtr4d	$⊢ (φ \land (B \in V \land A \in V)) \to dom (dom G CNF dom F) = \{x \in ({dom G}^{dom F}) \| {finSupp}_{G^{-1} (Z)} (x)\}$
61	60	f1oeq3d	$⊢ (φ \land (B \in V \land A \in V)) \to ((f \in U ⟼ G^{-1} \circ (f \circ F)) : U \underset{1-1 onto}{⟶} dom (dom G CNF dom F) \leftrightarrow (f \in U ⟼ G^{-1} \circ (f \circ F)) : U \underset{1-1 onto}{⟶} \{x \in ({dom G}^{dom F}) \| {finSupp}_{G^{-1} (Z)} (x)\})$
62	47 61	mpbird	$⊢ (φ \land (B \in V \land A \in V)) \to (f \in U ⟼ G^{-1} \circ (f \circ F)) : U \underset{1-1 onto}{⟶} dom (dom G CNF dom F)$
63		eqid	$⊢ dom (dom G CNF dom F) = dom (dom G CNF dom F)$
64		eqid	$⊢ \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} = \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\}$
65	63 50 52 64	oemapwe	$⊢ (φ \land (B \in V \land A \in V)) \to (\{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} We dom (dom G CNF dom F) \land dom OrdIso (\{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\}, dom (dom G CNF dom F)) = dom G ↑_{𝑜} dom F)$
66	65	simpld	$⊢ (φ \land (B \in V \land A \in V)) \to \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} We dom (dom G CNF dom F)$
67		eqid	$⊢ \{⟨x, y⟩ \| (f \in U ⟼ G^{-1} \circ (f \circ F)) (x) \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} (f \in U ⟼ G^{-1} \circ (f \circ F)) (y)\} = \{⟨x, y⟩ \| (f \in U ⟼ G^{-1} \circ (f \circ F)) (x) \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} (f \in U ⟼ G^{-1} \circ (f \circ F)) (y)\}$
68	67	f1owe	$⊢ (f \in U ⟼ G^{-1} \circ (f \circ F)) : U \underset{1-1 onto}{⟶} dom (dom G CNF dom F) \to (\{⟨x, y⟩ \| (f \in U ⟼ G^{-1} \circ (f \circ F)) (x) \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} (f \in U ⟼ G^{-1} \circ (f \circ F)) (y)\} We U \leftrightarrow \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} We dom (dom G CNF dom F))$
69	68	biimprd	$⊢ (f \in U ⟼ G^{-1} \circ (f \circ F)) : U \underset{1-1 onto}{⟶} dom (dom G CNF dom F) \to (\{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} We dom (dom G CNF dom F) \to \{⟨x, y⟩ \| (f \in U ⟼ G^{-1} \circ (f \circ F)) (x) \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} (f \in U ⟼ G^{-1} \circ (f \circ F)) (y)\} We U)$
70	62 66 69	sylc	$⊢ (φ \land (B \in V \land A \in V)) \to \{⟨x, y⟩ \| (f \in U ⟼ G^{-1} \circ (f \circ F)) (x) \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} (f \in U ⟼ G^{-1} \circ (f \circ F)) (y)\} We U$
71		weinxp	$⊢ \{⟨x, y⟩ \| (f \in U ⟼ G^{-1} \circ (f \circ F)) (x) \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} (f \in U ⟼ G^{-1} \circ (f \circ F)) (y)\} We U \leftrightarrow (\{⟨x, y⟩ \| (f \in U ⟼ G^{-1} \circ (f \circ F)) (x) \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} (f \in U ⟼ G^{-1} \circ (f \circ F)) (y)\} \cap (U \times U)) We U$
72	70 71	sylib	$⊢ (φ \land (B \in V \land A \in V)) \to (\{⟨x, y⟩ \| (f \in U ⟼ G^{-1} \circ (f \circ F)) (x) \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} (f \in U ⟼ G^{-1} \circ (f \circ F)) (y)\} \cap (U \times U)) We U$
73	16	adantr	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to F : dom F \underset{1-1 onto}{⟶} A$
74		f1ofn	$⊢ F : dom F \underset{1-1 onto}{⟶} A \to F Fn dom F$
75		fveq2	$⊢ z = F (c) \to x (z) = x (F (c))$
76		fveq2	$⊢ z = F (c) \to y (z) = y (F (c))$
77	75 76	breq12d	$⊢ z = F (c) \to (x (z) S y (z) \leftrightarrow x (F (c)) S y (F (c)))$
78		breq1	$⊢ z = F (c) \to (z R w \leftrightarrow F (c) R w)$
79	78	imbi1d	$⊢ z = F (c) \to ((z R w \to x (w) = y (w)) \leftrightarrow (F (c) R w \to x (w) = y (w)))$
80	79	ralbidv	$⊢ z = F (c) \to (\forall w \in A (z R w \to x (w) = y (w)) \leftrightarrow \forall w \in A (F (c) R w \to x (w) = y (w)))$
81	77 80	anbi12d	$⊢ z = F (c) \to ((x (z) S y (z) \land \forall w \in A (z R w \to x (w) = y (w))) \leftrightarrow (x (F (c)) S y (F (c)) \land \forall w \in A (F (c) R w \to x (w) = y (w))))$
82	81	rexrn	$⊢ F Fn dom F \to (\exists z \in ran F (x (z) S y (z) \land \forall w \in A (z R w \to x (w) = y (w))) \leftrightarrow \exists c \in dom F (x (F (c)) S y (F (c)) \land \forall w \in A (F (c) R w \to x (w) = y (w))))$
83	73 74 82	3syl	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to (\exists z \in ran F (x (z) S y (z) \land \forall w \in A (z R w \to x (w) = y (w))) \leftrightarrow \exists c \in dom F (x (F (c)) S y (F (c)) \land \forall w \in A (F (c) R w \to x (w) = y (w))))$
84		f1ofo	$⊢ F : dom F \underset{1-1 onto}{⟶} A \to F : dom F \underset{onto}{⟶} A$
85		forn	$⊢ F : dom F \underset{onto}{⟶} A \to ran F = A$
86	73 84 85	3syl	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to ran F = A$
87	86	rexeqdv	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to (\exists z \in ran F (x (z) S y (z) \land \forall w \in A (z R w \to x (w) = y (w))) \leftrightarrow \exists z \in A (x (z) S y (z) \land \forall w \in A (z R w \to x (w) = y (w))))$
88	28	adantr	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to G \in V$
89		cnvexg	$⊢ G \in V \to G^{-1} \in V$
90	88 89	syl	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to G^{-1} \in V$
91		vex	$⊢ x \in V$
92	25	adantr	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to F \in V$
93		coexg	$⊢ (x \in V \land F \in V) \to x \circ F \in V$
94	91 92 93	sylancr	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to x \circ F \in V$
95	90 94	coexd	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to G^{-1} \circ (x \circ F) \in V$
96		vex	$⊢ y \in V$
97		coexg	$⊢ (y \in V \land F \in V) \to y \circ F \in V$
98	96 92 97	sylancr	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to y \circ F \in V$
99	90 98	coexd	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to G^{-1} \circ (y \circ F) \in V$
100		fveq1	$⊢ a = G^{-1} \circ (x \circ F) \to a (c) = (G^{-1} \circ (x \circ F)) (c)$
101		fveq1	$⊢ b = G^{-1} \circ (y \circ F) \to b (c) = (G^{-1} \circ (y \circ F)) (c)$
102		eleq12	$⊢ (a (c) = (G^{-1} \circ (x \circ F)) (c) \land b (c) = (G^{-1} \circ (y \circ F)) (c)) \to (a (c) \in b (c) \leftrightarrow (G^{-1} \circ (x \circ F)) (c) \in (G^{-1} \circ (y \circ F)) (c))$
103	100 101 102	syl2an	$⊢ (a = G^{-1} \circ (x \circ F) \land b = G^{-1} \circ (y \circ F)) \to (a (c) \in b (c) \leftrightarrow (G^{-1} \circ (x \circ F)) (c) \in (G^{-1} \circ (y \circ F)) (c))$
104		fveq1	$⊢ a = G^{-1} \circ (x \circ F) \to a (d) = (G^{-1} \circ (x \circ F)) (d)$
105		fveq1	$⊢ b = G^{-1} \circ (y \circ F) \to b (d) = (G^{-1} \circ (y \circ F)) (d)$
106	104 105	eqeqan12d	$⊢ (a = G^{-1} \circ (x \circ F) \land b = G^{-1} \circ (y \circ F)) \to (a (d) = b (d) \leftrightarrow (G^{-1} \circ (x \circ F)) (d) = (G^{-1} \circ (y \circ F)) (d))$
107	106	imbi2d	$⊢ (a = G^{-1} \circ (x \circ F) \land b = G^{-1} \circ (y \circ F)) \to ((c \in d \to a (d) = b (d)) \leftrightarrow (c \in d \to (G^{-1} \circ (x \circ F)) (d) = (G^{-1} \circ (y \circ F)) (d)))$
108	107	ralbidv	$⊢ (a = G^{-1} \circ (x \circ F) \land b = G^{-1} \circ (y \circ F)) \to (\forall d \in dom F (c \in d \to a (d) = b (d)) \leftrightarrow \forall d \in dom F (c \in d \to (G^{-1} \circ (x \circ F)) (d) = (G^{-1} \circ (y \circ F)) (d)))$
109	103 108	anbi12d	$⊢ (a = G^{-1} \circ (x \circ F) \land b = G^{-1} \circ (y \circ F)) \to ((a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d))) \leftrightarrow ((G^{-1} \circ (x \circ F)) (c) \in (G^{-1} \circ (y \circ F)) (c) \land \forall d \in dom F (c \in d \to (G^{-1} \circ (x \circ F)) (d) = (G^{-1} \circ (y \circ F)) (d))))$
110	109	rexbidv	$⊢ (a = G^{-1} \circ (x \circ F) \land b = G^{-1} \circ (y \circ F)) \to (\exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d))) \leftrightarrow \exists c \in dom F ((G^{-1} \circ (x \circ F)) (c) \in (G^{-1} \circ (y \circ F)) (c) \land \forall d \in dom F (c \in d \to (G^{-1} \circ (x \circ F)) (d) = (G^{-1} \circ (y \circ F)) (d))))$
111	110 64	brabga	$⊢ (G^{-1} \circ (x \circ F) \in V \land G^{-1} \circ (y \circ F) \in V) \to ((G^{-1} \circ (x \circ F)) \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} (G^{-1} \circ (y \circ F)) \leftrightarrow \exists c \in dom F ((G^{-1} \circ (x \circ F)) (c) \in (G^{-1} \circ (y \circ F)) (c) \land \forall d \in dom F (c \in d \to (G^{-1} \circ (x \circ F)) (d) = (G^{-1} \circ (y \circ F)) (d))))$
112	95 99 111	syl2anc	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to ((G^{-1} \circ (x \circ F)) \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} (G^{-1} \circ (y \circ F)) \leftrightarrow \exists c \in dom F ((G^{-1} \circ (x \circ F)) (c) \in (G^{-1} \circ (y \circ F)) (c) \land \forall d \in dom F (c \in d \to (G^{-1} \circ (x \circ F)) (d) = (G^{-1} \circ (y \circ F)) (d))))$
113		eqid	$⊢ (f \in U ⟼ G^{-1} \circ (f \circ F)) = (f \in U ⟼ G^{-1} \circ (f \circ F))$
114		coeq1	$⊢ f = x \to f \circ F = x \circ F$
115	114	coeq2d	$⊢ f = x \to G^{-1} \circ (f \circ F) = G^{-1} \circ (x \circ F)$
116		simprl	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to x \in U$
117	113 115 116 95	fvmptd3	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to (f \in U ⟼ G^{-1} \circ (f \circ F)) (x) = G^{-1} \circ (x \circ F)$
118		coeq1	$⊢ f = y \to f \circ F = y \circ F$
119	118	coeq2d	$⊢ f = y \to G^{-1} \circ (f \circ F) = G^{-1} \circ (y \circ F)$
120		simprr	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to y \in U$
121	113 119 120 99	fvmptd3	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to (f \in U ⟼ G^{-1} \circ (f \circ F)) (y) = G^{-1} \circ (y \circ F)$
122	117 121	breq12d	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to ((f \in U ⟼ G^{-1} \circ (f \circ F)) (x) \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} (f \in U ⟼ G^{-1} \circ (f \circ F)) (y) \leftrightarrow (G^{-1} \circ (x \circ F)) \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} (G^{-1} \circ (y \circ F)))$
123	20	ad2antrr	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land c \in dom F) \to G {Isom}_{E, S} (dom G, B)$
124		isocnv	$⊢ G {Isom}_{E, S} (dom G, B) \to G^{-1} {Isom}_{S, E} (B, dom G)$
125	123 124	syl	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land c \in dom F) \to G^{-1} {Isom}_{S, E} (B, dom G)$
126	2	ssrab3	$⊢ U \subseteq B^{A}$
127	126 116	sselid	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to x \in (B^{A})$
128		elmapi	$⊢ x \in (B^{A}) \to x : A ⟶ B$
129	127 128	syl	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to x : A ⟶ B$
130	6	oif	$⊢ F : dom F ⟶ A$
131	130	ffvelcdmi	$⊢ c \in dom F \to F (c) \in A$
132		ffvelcdm	$⊢ (x : A ⟶ B \land F (c) \in A) \to x (F (c)) \in B$
133	129 131 132	syl2an	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land c \in dom F) \to x (F (c)) \in B$
134	126 120	sselid	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to y \in (B^{A})$
135		elmapi	$⊢ y \in (B^{A}) \to y : A ⟶ B$
136	134 135	syl	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to y : A ⟶ B$
137		ffvelcdm	$⊢ (y : A ⟶ B \land F (c) \in A) \to y (F (c)) \in B$
138	136 131 137	syl2an	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land c \in dom F) \to y (F (c)) \in B$
139		isorel	$⊢ (G^{-1} {Isom}_{S, E} (B, dom G) \land (x (F (c)) \in B \land y (F (c)) \in B)) \to (x (F (c)) S y (F (c)) \leftrightarrow G^{-1} (x (F (c))) E G^{-1} (y (F (c))))$
140	125 133 138 139	syl12anc	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land c \in dom F) \to (x (F (c)) S y (F (c)) \leftrightarrow G^{-1} (x (F (c))) E G^{-1} (y (F (c))))$
141		fvex	$⊢ G^{-1} (y (F (c))) \in V$
142	141	epeli	$⊢ G^{-1} (x (F (c))) E G^{-1} (y (F (c))) \leftrightarrow G^{-1} (x (F (c))) \in G^{-1} (y (F (c)))$
143	140 142	bitrdi	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land c \in dom F) \to (x (F (c)) S y (F (c)) \leftrightarrow G^{-1} (x (F (c))) \in G^{-1} (y (F (c))))$
144	129	adantr	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land c \in dom F) \to x : A ⟶ B$
145		fco	$⊢ (x : A ⟶ B \land F : dom F ⟶ A) \to (x \circ F) : dom F ⟶ B$
146	144 130 145	sylancl	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land c \in dom F) \to (x \circ F) : dom F ⟶ B$
147		fvco3	$⊢ ((x \circ F) : dom F ⟶ B \land c \in dom F) \to (G^{-1} \circ (x \circ F)) (c) = G^{-1} ((x \circ F) (c))$
148	146 147	sylancom	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land c \in dom F) \to (G^{-1} \circ (x \circ F)) (c) = G^{-1} ((x \circ F) (c))$
149		simpr	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land c \in dom F) \to c \in dom F$
150		fvco3	$⊢ (F : dom F ⟶ A \land c \in dom F) \to (x \circ F) (c) = x (F (c))$
151	130 149 150	sylancr	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land c \in dom F) \to (x \circ F) (c) = x (F (c))$
152	151	fveq2d	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land c \in dom F) \to G^{-1} ((x \circ F) (c)) = G^{-1} (x (F (c)))$
153	148 152	eqtrd	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land c \in dom F) \to (G^{-1} \circ (x \circ F)) (c) = G^{-1} (x (F (c)))$
154	136	adantr	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land c \in dom F) \to y : A ⟶ B$
155		fco	$⊢ (y : A ⟶ B \land F : dom F ⟶ A) \to (y \circ F) : dom F ⟶ B$
156	154 130 155	sylancl	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land c \in dom F) \to (y \circ F) : dom F ⟶ B$
157		fvco3	$⊢ ((y \circ F) : dom F ⟶ B \land c \in dom F) \to (G^{-1} \circ (y \circ F)) (c) = G^{-1} ((y \circ F) (c))$
158	156 157	sylancom	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land c \in dom F) \to (G^{-1} \circ (y \circ F)) (c) = G^{-1} ((y \circ F) (c))$
159		fvco3	$⊢ (F : dom F ⟶ A \land c \in dom F) \to (y \circ F) (c) = y (F (c))$
160	130 149 159	sylancr	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land c \in dom F) \to (y \circ F) (c) = y (F (c))$
161	160	fveq2d	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land c \in dom F) \to G^{-1} ((y \circ F) (c)) = G^{-1} (y (F (c)))$
162	158 161	eqtrd	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land c \in dom F) \to (G^{-1} \circ (y \circ F)) (c) = G^{-1} (y (F (c)))$
163	153 162	eleq12d	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land c \in dom F) \to ((G^{-1} \circ (x \circ F)) (c) \in (G^{-1} \circ (y \circ F)) (c) \leftrightarrow G^{-1} (x (F (c))) \in G^{-1} (y (F (c))))$
164	143 163	bitr4d	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land c \in dom F) \to (x (F (c)) S y (F (c)) \leftrightarrow (G^{-1} \circ (x \circ F)) (c) \in (G^{-1} \circ (y \circ F)) (c))$
165	86	raleqdv	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to (\forall w \in ran F (F (c) R w \to x (w) = y (w)) \leftrightarrow \forall w \in A (F (c) R w \to x (w) = y (w)))$
166		breq2	$⊢ w = F (d) \to (F (c) R w \leftrightarrow F (c) R F (d))$
167		fveq2	$⊢ w = F (d) \to x (w) = x (F (d))$
168		fveq2	$⊢ w = F (d) \to y (w) = y (F (d))$
169	167 168	eqeq12d	$⊢ w = F (d) \to (x (w) = y (w) \leftrightarrow x (F (d)) = y (F (d)))$
170	166 169	imbi12d	$⊢ w = F (d) \to ((F (c) R w \to x (w) = y (w)) \leftrightarrow (F (c) R F (d) \to x (F (d)) = y (F (d))))$
171	170	ralrn	$⊢ F Fn dom F \to (\forall w \in ran F (F (c) R w \to x (w) = y (w)) \leftrightarrow \forall d \in dom F (F (c) R F (d) \to x (F (d)) = y (F (d))))$
172	73 74 171	3syl	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to (\forall w \in ran F (F (c) R w \to x (w) = y (w)) \leftrightarrow \forall d \in dom F (F (c) R F (d) \to x (F (d)) = y (F (d))))$
173	165 172	bitr3d	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to (\forall w \in A (F (c) R w \to x (w) = y (w)) \leftrightarrow \forall d \in dom F (F (c) R F (d) \to x (F (d)) = y (F (d))))$
174	173	adantr	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land c \in dom F) \to (\forall w \in A (F (c) R w \to x (w) = y (w)) \leftrightarrow \forall d \in dom F (F (c) R F (d) \to x (F (d)) = y (F (d))))$
175		epel	$⊢ c E d \leftrightarrow c \in d$
176	14	ad2antrr	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land (c \in dom F \land d \in dom F)) \to F {Isom}_{E, R} (dom F, A)$
177		isorel	$⊢ (F {Isom}_{E, R} (dom F, A) \land (c \in dom F \land d \in dom F)) \to (c E d \leftrightarrow F (c) R F (d))$
178	176 177	sylancom	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land (c \in dom F \land d \in dom F)) \to (c E d \leftrightarrow F (c) R F (d))$
179	175 178	bitr3id	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land (c \in dom F \land d \in dom F)) \to (c \in d \leftrightarrow F (c) R F (d))$
180	146	adantrr	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land (c \in dom F \land d \in dom F)) \to (x \circ F) : dom F ⟶ B$
181		simprr	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land (c \in dom F \land d \in dom F)) \to d \in dom F$
182	180 181	fvco3d	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land (c \in dom F \land d \in dom F)) \to (G^{-1} \circ (x \circ F)) (d) = G^{-1} ((x \circ F) (d))$
183	156	adantrr	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land (c \in dom F \land d \in dom F)) \to (y \circ F) : dom F ⟶ B$
184	183 181	fvco3d	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land (c \in dom F \land d \in dom F)) \to (G^{-1} \circ (y \circ F)) (d) = G^{-1} ((y \circ F) (d))$
185	182 184	eqeq12d	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land (c \in dom F \land d \in dom F)) \to ((G^{-1} \circ (x \circ F)) (d) = (G^{-1} \circ (y \circ F)) (d) \leftrightarrow G^{-1} ((x \circ F) (d)) = G^{-1} ((y \circ F) (d)))$
186	30	ad2antrr	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land (c \in dom F \land d \in dom F)) \to G : dom G \underset{1-1 onto}{⟶} B$
187		f1of1	$⊢ G^{-1} : B \underset{1-1 onto}{⟶} dom G \to G^{-1} : B \underset{1-1}{⟶} dom G$
188	186 22 187	3syl	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land (c \in dom F \land d \in dom F)) \to G^{-1} : B \underset{1-1}{⟶} dom G$
189	180 181	ffvelcdmd	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land (c \in dom F \land d \in dom F)) \to (x \circ F) (d) \in B$
190	183 181	ffvelcdmd	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land (c \in dom F \land d \in dom F)) \to (y \circ F) (d) \in B$
191		f1fveq	$⊢ (G^{-1} : B \underset{1-1}{⟶} dom G \land ((x \circ F) (d) \in B \land (y \circ F) (d) \in B)) \to (G^{-1} ((x \circ F) (d)) = G^{-1} ((y \circ F) (d)) \leftrightarrow (x \circ F) (d) = (y \circ F) (d))$
192	188 189 190 191	syl12anc	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land (c \in dom F \land d \in dom F)) \to (G^{-1} ((x \circ F) (d)) = G^{-1} ((y \circ F) (d)) \leftrightarrow (x \circ F) (d) = (y \circ F) (d))$
193		fvco3	$⊢ (F : dom F ⟶ A \land d \in dom F) \to (x \circ F) (d) = x (F (d))$
194	130 181 193	sylancr	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land (c \in dom F \land d \in dom F)) \to (x \circ F) (d) = x (F (d))$
195		fvco3	$⊢ (F : dom F ⟶ A \land d \in dom F) \to (y \circ F) (d) = y (F (d))$
196	130 181 195	sylancr	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land (c \in dom F \land d \in dom F)) \to (y \circ F) (d) = y (F (d))$
197	194 196	eqeq12d	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land (c \in dom F \land d \in dom F)) \to ((x \circ F) (d) = (y \circ F) (d) \leftrightarrow x (F (d)) = y (F (d)))$
198	185 192 197	3bitrd	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land (c \in dom F \land d \in dom F)) \to ((G^{-1} \circ (x \circ F)) (d) = (G^{-1} \circ (y \circ F)) (d) \leftrightarrow x (F (d)) = y (F (d)))$
199	179 198	imbi12d	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land (c \in dom F \land d \in dom F)) \to ((c \in d \to (G^{-1} \circ (x \circ F)) (d) = (G^{-1} \circ (y \circ F)) (d)) \leftrightarrow (F (c) R F (d) \to x (F (d)) = y (F (d))))$
200	199	anassrs	$⊢ ((((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land c \in dom F) \land d \in dom F) \to ((c \in d \to (G^{-1} \circ (x \circ F)) (d) = (G^{-1} \circ (y \circ F)) (d)) \leftrightarrow (F (c) R F (d) \to x (F (d)) = y (F (d))))$
201	200	ralbidva	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land c \in dom F) \to (\forall d \in dom F (c \in d \to (G^{-1} \circ (x \circ F)) (d) = (G^{-1} \circ (y \circ F)) (d)) \leftrightarrow \forall d \in dom F (F (c) R F (d) \to x (F (d)) = y (F (d))))$
202	174 201	bitr4d	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land c \in dom F) \to (\forall w \in A (F (c) R w \to x (w) = y (w)) \leftrightarrow \forall d \in dom F (c \in d \to (G^{-1} \circ (x \circ F)) (d) = (G^{-1} \circ (y \circ F)) (d)))$
203	164 202	anbi12d	$⊢ (((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \land c \in dom F) \to ((x (F (c)) S y (F (c)) \land \forall w \in A (F (c) R w \to x (w) = y (w))) \leftrightarrow ((G^{-1} \circ (x \circ F)) (c) \in (G^{-1} \circ (y \circ F)) (c) \land \forall d \in dom F (c \in d \to (G^{-1} \circ (x \circ F)) (d) = (G^{-1} \circ (y \circ F)) (d))))$
204	203	rexbidva	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to (\exists c \in dom F (x (F (c)) S y (F (c)) \land \forall w \in A (F (c) R w \to x (w) = y (w))) \leftrightarrow \exists c \in dom F ((G^{-1} \circ (x \circ F)) (c) \in (G^{-1} \circ (y \circ F)) (c) \land \forall d \in dom F (c \in d \to (G^{-1} \circ (x \circ F)) (d) = (G^{-1} \circ (y \circ F)) (d))))$
205	112 122 204	3bitr4rd	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to (\exists c \in dom F (x (F (c)) S y (F (c)) \land \forall w \in A (F (c) R w \to x (w) = y (w))) \leftrightarrow (f \in U ⟼ G^{-1} \circ (f \circ F)) (x) \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} (f \in U ⟼ G^{-1} \circ (f \circ F)) (y))$
206	83 87 205	3bitr3d	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to (\exists z \in A (x (z) S y (z) \land \forall w \in A (z R w \to x (w) = y (w))) \leftrightarrow (f \in U ⟼ G^{-1} \circ (f \circ F)) (x) \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} (f \in U ⟼ G^{-1} \circ (f \circ F)) (y))$
207	206	ex	$⊢ (φ \land (B \in V \land A \in V)) \to ((x \in U \land y \in U) \to (\exists z \in A (x (z) S y (z) \land \forall w \in A (z R w \to x (w) = y (w))) \leftrightarrow (f \in U ⟼ G^{-1} \circ (f \circ F)) (x) \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} (f \in U ⟼ G^{-1} \circ (f \circ F)) (y)))$
208	207	pm5.32rd	$⊢ (φ \land (B \in V \land A \in V)) \to ((\exists z \in A (x (z) S y (z) \land \forall w \in A (z R w \to x (w) = y (w))) \land (x \in U \land y \in U)) \leftrightarrow ((f \in U ⟼ G^{-1} \circ (f \circ F)) (x) \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} (f \in U ⟼ G^{-1} \circ (f \circ F)) (y) \land (x \in U \land y \in U)))$
209	208	opabbidv	$⊢ (φ \land (B \in V \land A \in V)) \to \{⟨x, y⟩ \| (\exists z \in A (x (z) S y (z) \land \forall w \in A (z R w \to x (w) = y (w))) \land (x \in U \land y \in U))\} = \{⟨x, y⟩ \| ((f \in U ⟼ G^{-1} \circ (f \circ F)) (x) \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} (f \in U ⟼ G^{-1} \circ (f \circ F)) (y) \land (x \in U \land y \in U))\}$
210		df-xp	$⊢ U \times U = \{⟨x, y⟩ \| (x \in U \land y \in U)\}$
211	1 210	ineq12i	$⊢ T \cap (U \times U) = \{⟨x, y⟩ \| \exists z \in A (x (z) S y (z) \land \forall w \in A (z R w \to x (w) = y (w)))\} \cap \{⟨x, y⟩ \| (x \in U \land y \in U)\}$
212		inopab	$⊢ \{⟨x, y⟩ \| \exists z \in A (x (z) S y (z) \land \forall w \in A (z R w \to x (w) = y (w)))\} \cap \{⟨x, y⟩ \| (x \in U \land y \in U)\} = \{⟨x, y⟩ \| (\exists z \in A (x (z) S y (z) \land \forall w \in A (z R w \to x (w) = y (w))) \land (x \in U \land y \in U))\}$
213	211 212	eqtri	$⊢ T \cap (U \times U) = \{⟨x, y⟩ \| (\exists z \in A (x (z) S y (z) \land \forall w \in A (z R w \to x (w) = y (w))) \land (x \in U \land y \in U))\}$
214	210	ineq2i	$⊢ \{⟨x, y⟩ \| (f \in U ⟼ G^{-1} \circ (f \circ F)) (x) \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} (f \in U ⟼ G^{-1} \circ (f \circ F)) (y)\} \cap (U \times U) = \{⟨x, y⟩ \| (f \in U ⟼ G^{-1} \circ (f \circ F)) (x) \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} (f \in U ⟼ G^{-1} \circ (f \circ F)) (y)\} \cap \{⟨x, y⟩ \| (x \in U \land y \in U)\}$
215		inopab	$⊢ \{⟨x, y⟩ \| (f \in U ⟼ G^{-1} \circ (f \circ F)) (x) \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} (f \in U ⟼ G^{-1} \circ (f \circ F)) (y)\} \cap \{⟨x, y⟩ \| (x \in U \land y \in U)\} = \{⟨x, y⟩ \| ((f \in U ⟼ G^{-1} \circ (f \circ F)) (x) \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} (f \in U ⟼ G^{-1} \circ (f \circ F)) (y) \land (x \in U \land y \in U))\}$
216	214 215	eqtri	$⊢ \{⟨x, y⟩ \| (f \in U ⟼ G^{-1} \circ (f \circ F)) (x) \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} (f \in U ⟼ G^{-1} \circ (f \circ F)) (y)\} \cap (U \times U) = \{⟨x, y⟩ \| ((f \in U ⟼ G^{-1} \circ (f \circ F)) (x) \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} (f \in U ⟼ G^{-1} \circ (f \circ F)) (y) \land (x \in U \land y \in U))\}$
217	209 213 216	3eqtr4g	$⊢ (φ \land (B \in V \land A \in V)) \to T \cap (U \times U) = \{⟨x, y⟩ \| (f \in U ⟼ G^{-1} \circ (f \circ F)) (x) \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} (f \in U ⟼ G^{-1} \circ (f \circ F)) (y)\} \cap (U \times U)$
218		weeq1	$⊢ T \cap (U \times U) = \{⟨x, y⟩ \| (f \in U ⟼ G^{-1} \circ (f \circ F)) (x) \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} (f \in U ⟼ G^{-1} \circ (f \circ F)) (y)\} \cap (U \times U) \to ((T \cap (U \times U)) We U \leftrightarrow (\{⟨x, y⟩ \| (f \in U ⟼ G^{-1} \circ (f \circ F)) (x) \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} (f \in U ⟼ G^{-1} \circ (f \circ F)) (y)\} \cap (U \times U)) We U)$
219	217 218	syl	$⊢ (φ \land (B \in V \land A \in V)) \to ((T \cap (U \times U)) We U \leftrightarrow (\{⟨x, y⟩ \| (f \in U ⟼ G^{-1} \circ (f \circ F)) (x) \{⟨a, b⟩ \| \exists c \in dom F (a (c) \in b (c) \land \forall d \in dom F (c \in d \to a (d) = b (d)))\} (f \in U ⟼ G^{-1} \circ (f \circ F)) (y)\} \cap (U \times U)) We U)$
220	72 219	mpbird	$⊢ (φ \land (B \in V \land A \in V)) \to (T \cap (U \times U)) We U$
221		weinxp	$⊢ T We U \leftrightarrow (T \cap (U \times U)) We U$
222	220 221	sylibr	$⊢ (φ \land (B \in V \land A \in V)) \to T We U$
223	222	ex	$⊢ φ \to ((B \in V \land A \in V) \to T We U)$
224		we0	$⊢ T We \emptyset$
225		elmapex	$⊢ x \in (B^{A}) \to (B \in V \land A \in V)$
226	225	con3i	$⊢ \neg (B \in V \land A \in V) \to \neg x \in (B^{A})$
227	226	pm2.21d	$⊢ \neg (B \in V \land A \in V) \to (x \in (B^{A}) \to \neg {finSupp}_{Z} (x))$
228	227	ralrimiv	$⊢ \neg (B \in V \land A \in V) \to \forall x \in (B^{A}) \neg {finSupp}_{Z} (x)$
229		rabeq0	$⊢ \{x \in (B^{A}) \| {finSupp}_{Z} (x)\} = \emptyset \leftrightarrow \forall x \in (B^{A}) \neg {finSupp}_{Z} (x)$
230	228 229	sylibr	$⊢ \neg (B \in V \land A \in V) \to \{x \in (B^{A}) \| {finSupp}_{Z} (x)\} = \emptyset$
231	2 230	eqtrid	$⊢ \neg (B \in V \land A \in V) \to U = \emptyset$
232		weeq2	$⊢ U = \emptyset \to (T We U \leftrightarrow T We \emptyset)$
233	231 232	syl	$⊢ \neg (B \in V \land A \in V) \to (T We U \leftrightarrow T We \emptyset)$
234	224 233	mpbiri	$⊢ \neg (B \in V \land A \in V) \to T We U$
235	223 234	pm2.61d1	$⊢ φ \to T We U$

Metamath Proof Explorer

Theorem wemapwe

Proof