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	ffvelrni	$⊢ \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 (\{⟨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)$
69	62 66 68	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$
70		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$
71	69 70	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$
72	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$
73		f1ofn	$⊢ F : dom F \underset{1-1 onto}{⟶} A \to F Fn dom F$
74		fveq2	$⊢ z = F (c) \to x (z) = x (F (c))$
75		fveq2	$⊢ z = F (c) \to y (z) = y (F (c))$
76	74 75	breq12d	$⊢ z = F (c) \to (x (z) S y (z) \leftrightarrow x (F (c)) S y (F (c)))$
77		breq1	$⊢ z = F (c) \to (z R w \leftrightarrow F (c) R w)$
78	77	imbi1d	$⊢ z = F (c) \to ((z R w \to x (w) = y (w)) \leftrightarrow (F (c) R w \to x (w) = y (w)))$
79	78	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)))$
80	76 79	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))))$
81	80	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))))$
82	72 73 81	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))))$
83		f1ofo	$⊢ F : dom F \underset{1-1 onto}{⟶} A \to F : dom F \underset{onto}{⟶} A$
84		forn	$⊢ F : dom F \underset{onto}{⟶} A \to ran F = A$
85	72 83 84	3syl	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to ran F = A$
86	85	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))))$
87	28	adantr	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to G \in V$
88		cnvexg	$⊢ G \in V \to G^{-1} \in V$
89	87 88	syl	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to G^{-1} \in V$
90		vex	$⊢ x \in V$
91	25	adantr	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to F \in V$
92		coexg	$⊢ (x \in V \land F \in V) \to x \circ F \in V$
93	90 91 92	sylancr	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to x \circ F \in V$
94		coexg	$⊢ (G^{-1} \in V \land x \circ F \in V) \to G^{-1} \circ (x \circ F) \in V$
95	89 93 94	syl2anc	$⊢ ((φ \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 91 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		coexg	$⊢ (G^{-1} \in V \land y \circ F \in V) \to G^{-1} \circ (y \circ F) \in V$
100	89 98 99	syl2anc	$⊢ ((φ \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$
101		fveq1	$⊢ a = G^{-1} \circ (x \circ F) \to a (c) = (G^{-1} \circ (x \circ F)) (c)$
102		fveq1	$⊢ b = G^{-1} \circ (y \circ F) \to b (c) = (G^{-1} \circ (y \circ F)) (c)$
103		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))$
104	101 102 103	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))$
105		fveq1	$⊢ a = G^{-1} \circ (x \circ F) \to a (d) = (G^{-1} \circ (x \circ F)) (d)$
106		fveq1	$⊢ b = G^{-1} \circ (y \circ F) \to b (d) = (G^{-1} \circ (y \circ F)) (d)$
107	105 106	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))$
108	107	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)))$
109	108	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)))$
110	104 109	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))))$
111	110	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))))$
112	111 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))))$
113	95 100 112	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))))$
114		eqid	$⊢ (f \in U ⟼ G^{-1} \circ (f \circ F)) = (f \in U ⟼ G^{-1} \circ (f \circ F))$
115		coeq1	$⊢ f = x \to f \circ F = x \circ F$
116	115	coeq2d	$⊢ f = x \to G^{-1} \circ (f \circ F) = G^{-1} \circ (x \circ F)$
117		simprl	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to x \in U$
118	114 116 117 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)$
119		coeq1	$⊢ f = y \to f \circ F = y \circ F$
120	119	coeq2d	$⊢ f = y \to G^{-1} \circ (f \circ F) = G^{-1} \circ (y \circ F)$
121		simprr	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to y \in U$
122	114 120 121 100	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)$
123	118 122	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)))$
124	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)$
125		isocnv	$⊢ G {Isom}_{E, S} (dom G, B) \to G^{-1} {Isom}_{S, E} (B, dom G)$
126	124 125	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)$
127	2	ssrab3	$⊢ U \subseteq B^{A}$
128	127 117	sselid	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to x \in (B^{A})$
129		elmapi	$⊢ x \in (B^{A}) \to x : A ⟶ B$
130	128 129	syl	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to x : A ⟶ B$
131	6	oif	$⊢ F : dom F ⟶ A$
132	131	ffvelrni	$⊢ c \in dom F \to F (c) \in A$
133		ffvelrn	$⊢ (x : A ⟶ B \land F (c) \in A) \to x (F (c)) \in B$
134	130 132 133	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$
135	127 121	sselid	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to y \in (B^{A})$
136		elmapi	$⊢ y \in (B^{A}) \to y : A ⟶ B$
137	135 136	syl	$⊢ ((φ \land (B \in V \land A \in V)) \land (x \in U \land y \in U)) \to y : A ⟶ B$
138		ffvelrn	$⊢ (y : A ⟶ B \land F (c) \in A) \to y (F (c)) \in B$
139	137 132 138	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$
140		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))))$
141	126 134 139 140	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))))$
142		fvex	$⊢ G^{-1} (y (F (c))) \in V$
143	142	epeli	$⊢ G^{-1} (x (F (c))) E G^{-1} (y (F (c))) \leftrightarrow G^{-1} (x (F (c))) \in G^{-1} (y (F (c)))$
144	141 143	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))))$
145	130	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$
146		fco	$⊢ (x : A ⟶ B \land F : dom F ⟶ A) \to (x \circ F) : dom F ⟶ B$
147	145 131 146	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$
148		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))$
149	147 148	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))$
150		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$
151		fvco3	$⊢ (F : dom F ⟶ A \land c \in dom F) \to (x \circ F) (c) = x (F (c))$
152	131 150 151	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))$
153	152	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)))$
154	149 153	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)))$
155	137	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$
156		fco	$⊢ (y : A ⟶ B \land F : dom F ⟶ A) \to (y \circ F) : dom F ⟶ B$
157	155 131 156	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$
158		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))$
159	157 158	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))$
160		fvco3	$⊢ (F : dom F ⟶ A \land c \in dom F) \to (y \circ F) (c) = y (F (c))$
161	131 150 160	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))$
162	161	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)))$
163	159 162	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)))$
164	154 163	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))))$
165	144 164	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))$
166	85	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)))$
167		breq2	$⊢ w = F (d) \to (F (c) R w \leftrightarrow F (c) R F (d))$
168		fveq2	$⊢ w = F (d) \to x (w) = x (F (d))$
169		fveq2	$⊢ w = F (d) \to y (w) = y (F (d))$
170	168 169	eqeq12d	$⊢ w = F (d) \to (x (w) = y (w) \leftrightarrow x (F (d)) = y (F (d)))$
171	167 170	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))))$
172	171	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))))$
173	72 73 172	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))))$
174	166 173	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))))$
175	174	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))))$
176		epel	$⊢ c E d \leftrightarrow c \in d$
177	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)$
178		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))$
179	177 178	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))$
180	176 179	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))$
181	147	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$
182		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$
183	181 182	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))$
184	157	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$
185	184 182	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))$
186	183 185	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)))$
187	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$
188		f1of1	$⊢ G^{-1} : B \underset{1-1 onto}{⟶} dom G \to G^{-1} : B \underset{1-1}{⟶} dom G$
189	187 22 188	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$
190	181 182	ffvelrnd	$⊢ (((φ \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$
191	184 182	ffvelrnd	$⊢ (((φ \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$
192		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))$
193	189 190 191 192	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))$
194		fvco3	$⊢ (F : dom F ⟶ A \land d \in dom F) \to (x \circ F) (d) = x (F (d))$
195	131 182 194	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))$
196		fvco3	$⊢ (F : dom F ⟶ A \land d \in dom F) \to (y \circ F) (d) = y (F (d))$
197	131 182 196	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))$
198	195 197	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)))$
199	186 193 198	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)))$
200	180 199	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))))$
201	200	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))))$
202	201	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))))$
203	175 202	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)))$
204	165 203	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))))$
205	204	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))))$
206	113 123 205	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))$
207	82 86 206	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))$
208	207	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)))$
209	208	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)))$
210	209	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))\}$
211		df-xp	$⊢ U \times U = \{⟨x, y⟩ \| (x \in U \land y \in U)\}$
212	1 211	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)\}$
213		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))\}$
214	212 213	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))\}$
215	211	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)\}$
216		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))\}$
217	215 216	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))\}$
218	210 214 217	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)$
219		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)$
220	218 219	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)$
221	71 220	mpbird	$⊢ (φ \land (B \in V \land A \in V)) \to (T \cap (U \times U)) We U$
222		weinxp	$⊢ T We U \leftrightarrow (T \cap (U \times U)) We U$
223	221 222	sylibr	$⊢ (φ \land (B \in V \land A \in V)) \to T We U$
224	223	ex	$⊢ φ \to ((B \in V \land A \in V) \to T We U)$
225		we0	$⊢ T We \emptyset$
226		elmapex	$⊢ x \in (B^{A}) \to (B \in V \land A \in V)$
227	226	con3i	$⊢ \neg (B \in V \land A \in V) \to \neg x \in (B^{A})$
228	227	pm2.21d	$⊢ \neg (B \in V \land A \in V) \to (x \in (B^{A}) \to \neg {finSupp}_{Z} (x))$
229	228	ralrimiv	$⊢ \neg (B \in V \land A \in V) \to \forall x \in (B^{A}) \neg {finSupp}_{Z} (x)$
230		rabeq0	$⊢ \{x \in (B^{A}) \| {finSupp}_{Z} (x)\} = \emptyset \leftrightarrow \forall x \in (B^{A}) \neg {finSupp}_{Z} (x)$
231	229 230	sylibr	$⊢ \neg (B \in V \land A \in V) \to \{x \in (B^{A}) \| {finSupp}_{Z} (x)\} = \emptyset$
232	2 231	eqtrid	$⊢ \neg (B \in V \land A \in V) \to U = \emptyset$
233		weeq2	$⊢ U = \emptyset \to (T We U \leftrightarrow T We \emptyset)$
234	232 233	syl	$⊢ \neg (B \in V \land A \in V) \to (T We U \leftrightarrow T We \emptyset)$
235	225 234	mpbiri	$⊢ \neg (B \in V \land A \in V) \to T We U$
236	224 235	pm2.61d1	$⊢ φ \to T We U$

Metamath Proof Explorer

Theorem wemapwe

Proof