fnwelem

	Ref	Expression
Hypotheses	fnwe.1	$⊢ T = \{⟨x, y⟩ \| ((x \in A \land y \in A) \land (F (x) R F (y) \lor (F (x) = F (y) \land x S y)))\}$
	fnwe.2	$⊢ φ \to F : A ⟶ B$
	fnwe.3	$⊢ φ \to R We B$
	fnwe.4	$⊢ φ \to S We A$
	fnwe.5	$⊢ φ \to F [w] \in V$
	fnwelem.6	$⊢ Q = \{⟨u, v⟩ \| ((u \in (B \times A) \land v \in (B \times A)) \land (1^{st} (u) R 1^{st} (v) \lor (1^{st} (u) = 1^{st} (v) \land 2^{nd} (u) S 2^{nd} (v))))\}$
	fnwelem.7	$⊢ G = (z \in A ⟼ ⟨F (z), z⟩)$
Assertion	fnwelem	$⊢ φ \to T We A$

Proof

Step	Hyp	Ref	Expression
1		fnwe.1	$⊢ T = \{⟨x, y⟩ \| ((x \in A \land y \in A) \land (F (x) R F (y) \lor (F (x) = F (y) \land x S y)))\}$
2		fnwe.2	$⊢ φ \to F : A ⟶ B$
3		fnwe.3	$⊢ φ \to R We B$
4		fnwe.4	$⊢ φ \to S We A$
5		fnwe.5	$⊢ φ \to F [w] \in V$
6		fnwelem.6	$⊢ Q = \{⟨u, v⟩ \| ((u \in (B \times A) \land v \in (B \times A)) \land (1^{st} (u) R 1^{st} (v) \lor (1^{st} (u) = 1^{st} (v) \land 2^{nd} (u) S 2^{nd} (v))))\}$
7		fnwelem.7	$⊢ G = (z \in A ⟼ ⟨F (z), z⟩)$
8		ffvelrn	$⊢ (F : A ⟶ B \land z \in A) \to F (z) \in B$
9		simpr	$⊢ (F : A ⟶ B \land z \in A) \to z \in A$
10	8 9	opelxpd	$⊢ (F : A ⟶ B \land z \in A) \to ⟨F (z), z⟩ \in (B \times A)$
11	10 7	fmptd	$⊢ F : A ⟶ B \to G : A ⟶ B \times A$
12		frn	$⊢ G : A ⟶ B \times A \to ran G \subseteq B \times A$
13	2 11 12	3syl	$⊢ φ \to ran G \subseteq B \times A$
14	6	wexp	$⊢ (R We B \land S We A) \to Q We (B \times A)$
15	3 4 14	syl2anc	$⊢ φ \to Q We (B \times A)$
16		wess	$⊢ ran G \subseteq B \times A \to (Q We (B \times A) \to Q We ran G)$
17	13 15 16	sylc	$⊢ φ \to Q We ran G$
18		fveq2	$⊢ z = x \to F (z) = F (x)$
19		id	$⊢ z = x \to z = x$
20	18 19	opeq12d	$⊢ z = x \to ⟨F (z), z⟩ = ⟨F (x), x⟩$
21		opex	$⊢ ⟨F (x), x⟩ \in V$
22	20 7 21	fvmpt	$⊢ x \in A \to G (x) = ⟨F (x), x⟩$
23		fveq2	$⊢ z = y \to F (z) = F (y)$
24		id	$⊢ z = y \to z = y$
25	23 24	opeq12d	$⊢ z = y \to ⟨F (z), z⟩ = ⟨F (y), y⟩$
26		opex	$⊢ ⟨F (y), y⟩ \in V$
27	25 7 26	fvmpt	$⊢ y \in A \to G (y) = ⟨F (y), y⟩$
28	22 27	eqeqan12d	$⊢ (x \in A \land y \in A) \to (G (x) = G (y) \leftrightarrow ⟨F (x), x⟩ = ⟨F (y), y⟩)$
29		fvex	$⊢ F (x) \in V$
30		vex	$⊢ x \in V$
31	29 30	opth	$⊢ ⟨F (x), x⟩ = ⟨F (y), y⟩ \leftrightarrow (F (x) = F (y) \land x = y)$
32	31	simprbi	$⊢ ⟨F (x), x⟩ = ⟨F (y), y⟩ \to x = y$
33	28 32	syl6bi	$⊢ (x \in A \land y \in A) \to (G (x) = G (y) \to x = y)$
34	33	rgen2	$⊢ \forall x \in A \forall y \in A (G (x) = G (y) \to x = y)$
35		dff13	$⊢ G : A \underset{1-1}{⟶} B \times A \leftrightarrow (G : A ⟶ B \times A \land \forall x \in A \forall y \in A (G (x) = G (y) \to x = y))$
36	11 34 35	sylanblrc	$⊢ F : A ⟶ B \to G : A \underset{1-1}{⟶} B \times A$
37		f1f1orn	$⊢ G : A \underset{1-1}{⟶} B \times A \to G : A \underset{1-1 onto}{⟶} ran G$
38		f1ocnv	$⊢ G : A \underset{1-1 onto}{⟶} ran G \to G^{-1} : ran G \underset{1-1 onto}{⟶} A$
39	2 36 37 38	4syl	$⊢ φ \to G^{-1} : ran G \underset{1-1 onto}{⟶} A$
40		eqid	$⊢ \{⟨x, y⟩ \| ((x \in A \land y \in A) \land {G^{-1}}^{-1} (x) Q {G^{-1}}^{-1} (y))\} = \{⟨x, y⟩ \| ((x \in A \land y \in A) \land {G^{-1}}^{-1} (x) Q {G^{-1}}^{-1} (y))\}$
41	40	f1oiso2	$⊢ G^{-1} : ran G \underset{1-1 onto}{⟶} A \to G^{-1} {Isom}_{Q, \{⟨x, y⟩ \| ((x \in A \land y \in A) \land {G^{-1}}^{-1} (x) Q {G^{-1}}^{-1} (y))\}} (ran G, A)$
42		frel	$⊢ G : A ⟶ B \times A \to Rel G$
43		dfrel2	$⊢ Rel G \leftrightarrow {G^{-1}}^{-1} = G$
44	42 43	sylib	$⊢ G : A ⟶ B \times A \to {G^{-1}}^{-1} = G$
45	44	fveq1d	$⊢ G : A ⟶ B \times A \to {G^{-1}}^{-1} (x) = G (x)$
46	44	fveq1d	$⊢ G : A ⟶ B \times A \to {G^{-1}}^{-1} (y) = G (y)$
47	45 46	breq12d	$⊢ G : A ⟶ B \times A \to ({G^{-1}}^{-1} (x) Q {G^{-1}}^{-1} (y) \leftrightarrow G (x) Q G (y))$
48	11 47	syl	$⊢ F : A ⟶ B \to ({G^{-1}}^{-1} (x) Q {G^{-1}}^{-1} (y) \leftrightarrow G (x) Q G (y))$
49	48	adantr	$⊢ (F : A ⟶ B \land (x \in A \land y \in A)) \to ({G^{-1}}^{-1} (x) Q {G^{-1}}^{-1} (y) \leftrightarrow G (x) Q G (y))$
50	22 27	breqan12d	$⊢ (x \in A \land y \in A) \to (G (x) Q G (y) \leftrightarrow ⟨F (x), x⟩ Q ⟨F (y), y⟩)$
51	50	adantl	$⊢ (F : A ⟶ B \land (x \in A \land y \in A)) \to (G (x) Q G (y) \leftrightarrow ⟨F (x), x⟩ Q ⟨F (y), y⟩)$
52		eleq1	$⊢ u = ⟨F (x), x⟩ \to (u \in (B \times A) \leftrightarrow ⟨F (x), x⟩ \in (B \times A))$
53		opelxp	$⊢ ⟨F (x), x⟩ \in (B \times A) \leftrightarrow (F (x) \in B \land x \in A)$
54	52 53	bitrdi	$⊢ u = ⟨F (x), x⟩ \to (u \in (B \times A) \leftrightarrow (F (x) \in B \land x \in A))$
55	54	anbi1d	$⊢ u = ⟨F (x), x⟩ \to ((u \in (B \times A) \land v \in (B \times A)) \leftrightarrow ((F (x) \in B \land x \in A) \land v \in (B \times A)))$
56	29 30	op1std	$⊢ u = ⟨F (x), x⟩ \to 1^{st} (u) = F (x)$
57	56	breq1d	$⊢ u = ⟨F (x), x⟩ \to (1^{st} (u) R 1^{st} (v) \leftrightarrow F (x) R 1^{st} (v))$
58	56	eqeq1d	$⊢ u = ⟨F (x), x⟩ \to (1^{st} (u) = 1^{st} (v) \leftrightarrow F (x) = 1^{st} (v))$
59	29 30	op2ndd	$⊢ u = ⟨F (x), x⟩ \to 2^{nd} (u) = x$
60	59	breq1d	$⊢ u = ⟨F (x), x⟩ \to (2^{nd} (u) S 2^{nd} (v) \leftrightarrow x S 2^{nd} (v))$
61	58 60	anbi12d	$⊢ u = ⟨F (x), x⟩ \to ((1^{st} (u) = 1^{st} (v) \land 2^{nd} (u) S 2^{nd} (v)) \leftrightarrow (F (x) = 1^{st} (v) \land x S 2^{nd} (v)))$
62	57 61	orbi12d	$⊢ u = ⟨F (x), x⟩ \to ((1^{st} (u) R 1^{st} (v) \lor (1^{st} (u) = 1^{st} (v) \land 2^{nd} (u) S 2^{nd} (v))) \leftrightarrow (F (x) R 1^{st} (v) \lor (F (x) = 1^{st} (v) \land x S 2^{nd} (v))))$
63	55 62	anbi12d	$⊢ u = ⟨F (x), x⟩ \to (((u \in (B \times A) \land v \in (B \times A)) \land (1^{st} (u) R 1^{st} (v) \lor (1^{st} (u) = 1^{st} (v) \land 2^{nd} (u) S 2^{nd} (v)))) \leftrightarrow (((F (x) \in B \land x \in A) \land v \in (B \times A)) \land (F (x) R 1^{st} (v) \lor (F (x) = 1^{st} (v) \land x S 2^{nd} (v)))))$
64		eleq1	$⊢ v = ⟨F (y), y⟩ \to (v \in (B \times A) \leftrightarrow ⟨F (y), y⟩ \in (B \times A))$
65		opelxp	$⊢ ⟨F (y), y⟩ \in (B \times A) \leftrightarrow (F (y) \in B \land y \in A)$
66	64 65	bitrdi	$⊢ v = ⟨F (y), y⟩ \to (v \in (B \times A) \leftrightarrow (F (y) \in B \land y \in A))$
67	66	anbi2d	$⊢ v = ⟨F (y), y⟩ \to (((F (x) \in B \land x \in A) \land v \in (B \times A)) \leftrightarrow ((F (x) \in B \land x \in A) \land (F (y) \in B \land y \in A)))$
68		fvex	$⊢ F (y) \in V$
69		vex	$⊢ y \in V$
70	68 69	op1std	$⊢ v = ⟨F (y), y⟩ \to 1^{st} (v) = F (y)$
71	70	breq2d	$⊢ v = ⟨F (y), y⟩ \to (F (x) R 1^{st} (v) \leftrightarrow F (x) R F (y))$
72	70	eqeq2d	$⊢ v = ⟨F (y), y⟩ \to (F (x) = 1^{st} (v) \leftrightarrow F (x) = F (y))$
73	68 69	op2ndd	$⊢ v = ⟨F (y), y⟩ \to 2^{nd} (v) = y$
74	73	breq2d	$⊢ v = ⟨F (y), y⟩ \to (x S 2^{nd} (v) \leftrightarrow x S y)$
75	72 74	anbi12d	$⊢ v = ⟨F (y), y⟩ \to ((F (x) = 1^{st} (v) \land x S 2^{nd} (v)) \leftrightarrow (F (x) = F (y) \land x S y))$
76	71 75	orbi12d	$⊢ v = ⟨F (y), y⟩ \to ((F (x) R 1^{st} (v) \lor (F (x) = 1^{st} (v) \land x S 2^{nd} (v))) \leftrightarrow (F (x) R F (y) \lor (F (x) = F (y) \land x S y)))$
77	67 76	anbi12d	$⊢ v = ⟨F (y), y⟩ \to ((((F (x) \in B \land x \in A) \land v \in (B \times A)) \land (F (x) R 1^{st} (v) \lor (F (x) = 1^{st} (v) \land x S 2^{nd} (v)))) \leftrightarrow (((F (x) \in B \land x \in A) \land (F (y) \in B \land y \in A)) \land (F (x) R F (y) \lor (F (x) = F (y) \land x S y))))$
78	21 26 63 77 6	brab	$⊢ ⟨F (x), x⟩ Q ⟨F (y), y⟩ \leftrightarrow (((F (x) \in B \land x \in A) \land (F (y) \in B \land y \in A)) \land (F (x) R F (y) \lor (F (x) = F (y) \land x S y)))$
79		ffvelrn	$⊢ (F : A ⟶ B \land x \in A) \to F (x) \in B$
80		simpr	$⊢ (F : A ⟶ B \land x \in A) \to x \in A$
81	79 80	jca	$⊢ (F : A ⟶ B \land x \in A) \to (F (x) \in B \land x \in A)$
82		ffvelrn	$⊢ (F : A ⟶ B \land y \in A) \to F (y) \in B$
83		simpr	$⊢ (F : A ⟶ B \land y \in A) \to y \in A$
84	82 83	jca	$⊢ (F : A ⟶ B \land y \in A) \to (F (y) \in B \land y \in A)$
85	81 84	anim12dan	$⊢ (F : A ⟶ B \land (x \in A \land y \in A)) \to ((F (x) \in B \land x \in A) \land (F (y) \in B \land y \in A))$
86	85	biantrurd	$⊢ (F : A ⟶ B \land (x \in A \land y \in A)) \to ((F (x) R F (y) \lor (F (x) = F (y) \land x S y)) \leftrightarrow (((F (x) \in B \land x \in A) \land (F (y) \in B \land y \in A)) \land (F (x) R F (y) \lor (F (x) = F (y) \land x S y))))$
87	78 86	bitr4id	$⊢ (F : A ⟶ B \land (x \in A \land y \in A)) \to (⟨F (x), x⟩ Q ⟨F (y), y⟩ \leftrightarrow (F (x) R F (y) \lor (F (x) = F (y) \land x S y)))$
88	49 51 87	3bitrrd	$⊢ (F : A ⟶ B \land (x \in A \land y \in A)) \to ((F (x) R F (y) \lor (F (x) = F (y) \land x S y)) \leftrightarrow {G^{-1}}^{-1} (x) Q {G^{-1}}^{-1} (y))$
89	88	pm5.32da	$⊢ F : A ⟶ B \to (((x \in A \land y \in A) \land (F (x) R F (y) \lor (F (x) = F (y) \land x S y))) \leftrightarrow ((x \in A \land y \in A) \land {G^{-1}}^{-1} (x) Q {G^{-1}}^{-1} (y)))$
90	89	opabbidv	$⊢ F : A ⟶ B \to \{⟨x, y⟩ \| ((x \in A \land y \in A) \land (F (x) R F (y) \lor (F (x) = F (y) \land x S y)))\} = \{⟨x, y⟩ \| ((x \in A \land y \in A) \land {G^{-1}}^{-1} (x) Q {G^{-1}}^{-1} (y))\}$
91	1 90	syl5eq	$⊢ F : A ⟶ B \to T = \{⟨x, y⟩ \| ((x \in A \land y \in A) \land {G^{-1}}^{-1} (x) Q {G^{-1}}^{-1} (y))\}$
92		isoeq3	$⊢ T = \{⟨x, y⟩ \| ((x \in A \land y \in A) \land {G^{-1}}^{-1} (x) Q {G^{-1}}^{-1} (y))\} \to (G^{-1} {Isom}_{Q, T} (ran G, A) \leftrightarrow G^{-1} {Isom}_{Q, \{⟨x, y⟩ \| ((x \in A \land y \in A) \land {G^{-1}}^{-1} (x) Q {G^{-1}}^{-1} (y))\}} (ran G, A))$
93	91 92	syl	$⊢ F : A ⟶ B \to (G^{-1} {Isom}_{Q, T} (ran G, A) \leftrightarrow G^{-1} {Isom}_{Q, \{⟨x, y⟩ \| ((x \in A \land y \in A) \land {G^{-1}}^{-1} (x) Q {G^{-1}}^{-1} (y))\}} (ran G, A))$
94	41 93	syl5ibr	$⊢ F : A ⟶ B \to (G^{-1} : ran G \underset{1-1 onto}{⟶} A \to G^{-1} {Isom}_{Q, T} (ran G, A))$
95	2 39 94	sylc	$⊢ φ \to G^{-1} {Isom}_{Q, T} (ran G, A)$
96		isocnv	$⊢ G^{-1} {Isom}_{Q, T} (ran G, A) \to {G^{-1}}^{-1} {Isom}_{T, Q} (A, ran G)$
97	95 96	syl	$⊢ φ \to {G^{-1}}^{-1} {Isom}_{T, Q} (A, ran G)$
98		imacnvcnv	$⊢ {G^{-1}}^{-1} [w] = G [w]$
99		vex	$⊢ w \in V$
100		xpexg	$⊢ (F [w] \in V \land w \in V) \to F [w] \times w \in V$
101	5 99 100	sylancl	$⊢ φ \to F [w] \times w \in V$
102		imadmres	$⊢ G [dom ({G ↾}_{w})] = G [w]$
103		dmres	$⊢ dom ({G ↾}_{w}) = w \cap dom G$
104	103	elin2	$⊢ x \in dom ({G ↾}_{w}) \leftrightarrow (x \in w \land x \in dom G)$
105		simprr	$⊢ (φ \land (x \in w \land x \in dom G)) \to x \in dom G$
106		f1dm	$⊢ G : A \underset{1-1}{⟶} B \times A \to dom G = A$
107	2 36 106	3syl	$⊢ φ \to dom G = A$
108	107	adantr	$⊢ (φ \land (x \in w \land x \in dom G)) \to dom G = A$
109	105 108	eleqtrd	$⊢ (φ \land (x \in w \land x \in dom G)) \to x \in A$
110	109 22	syl	$⊢ (φ \land (x \in w \land x \in dom G)) \to G (x) = ⟨F (x), x⟩$
111	2	ffnd	$⊢ φ \to F Fn A$
112	111	adantr	$⊢ (φ \land (x \in w \land x \in dom G)) \to F Fn A$
113		dmres	$⊢ dom ({F ↾}_{w}) = w \cap dom F$
114		inss2	$⊢ w \cap dom F \subseteq dom F$
115	112	fndmd	$⊢ (φ \land (x \in w \land x \in dom G)) \to dom F = A$
116	114 115	sseqtrid	$⊢ (φ \land (x \in w \land x \in dom G)) \to w \cap dom F \subseteq A$
117	113 116	eqsstrid	$⊢ (φ \land (x \in w \land x \in dom G)) \to dom ({F ↾}_{w}) \subseteq A$
118		simprl	$⊢ (φ \land (x \in w \land x \in dom G)) \to x \in w$
119	109 115	eleqtrrd	$⊢ (φ \land (x \in w \land x \in dom G)) \to x \in dom F$
120	113	elin2	$⊢ x \in dom ({F ↾}_{w}) \leftrightarrow (x \in w \land x \in dom F)$
121	118 119 120	sylanbrc	$⊢ (φ \land (x \in w \land x \in dom G)) \to x \in dom ({F ↾}_{w})$
122		fnfvima	$⊢ (F Fn A \land dom ({F ↾}_{w}) \subseteq A \land x \in dom ({F ↾}_{w})) \to F (x) \in F [dom ({F ↾}_{w})]$
123	112 117 121 122	syl3anc	$⊢ (φ \land (x \in w \land x \in dom G)) \to F (x) \in F [dom ({F ↾}_{w})]$
124		imadmres	$⊢ F [dom ({F ↾}_{w})] = F [w]$
125	123 124	eleqtrdi	$⊢ (φ \land (x \in w \land x \in dom G)) \to F (x) \in F [w]$
126	125 118	opelxpd	$⊢ (φ \land (x \in w \land x \in dom G)) \to ⟨F (x), x⟩ \in (F [w] \times w)$
127	110 126	eqeltrd	$⊢ (φ \land (x \in w \land x \in dom G)) \to G (x) \in (F [w] \times w)$
128	104 127	sylan2b	$⊢ (φ \land x \in dom ({G ↾}_{w})) \to G (x) \in (F [w] \times w)$
129	128	ralrimiva	$⊢ φ \to \forall x \in dom ({G ↾}_{w}) G (x) \in (F [w] \times w)$
130		f1fun	$⊢ G : A \underset{1-1}{⟶} B \times A \to Fun G$
131	2 36 130	3syl	$⊢ φ \to Fun G$
132		resss	$⊢ {G ↾}_{w} \subseteq G$
133		dmss	$⊢ {G ↾}_{w} \subseteq G \to dom ({G ↾}_{w}) \subseteq dom G$
134	132 133	ax-mp	$⊢ dom ({G ↾}_{w}) \subseteq dom G$
135		funimass4	$⊢ (Fun G \land dom ({G ↾}_{w}) \subseteq dom G) \to (G [dom ({G ↾}_{w})] \subseteq F [w] \times w \leftrightarrow \forall x \in dom ({G ↾}_{w}) G (x) \in (F [w] \times w))$
136	131 134 135	sylancl	$⊢ φ \to (G [dom ({G ↾}_{w})] \subseteq F [w] \times w \leftrightarrow \forall x \in dom ({G ↾}_{w}) G (x) \in (F [w] \times w))$
137	129 136	mpbird	$⊢ φ \to G [dom ({G ↾}_{w})] \subseteq F [w] \times w$
138	102 137	eqsstrrid	$⊢ φ \to G [w] \subseteq F [w] \times w$
139	101 138	ssexd	$⊢ φ \to G [w] \in V$
140	98 139	eqeltrid	$⊢ φ \to {G^{-1}}^{-1} [w] \in V$
141	140	alrimiv	$⊢ φ \to \forall w {G^{-1}}^{-1} [w] \in V$
142		isowe2	$⊢ ({G^{-1}}^{-1} {Isom}_{T, Q} (A, ran G) \land \forall w {G^{-1}}^{-1} [w] \in V) \to (Q We ran G \to T We A)$
143	97 141 142	syl2anc	$⊢ φ \to (Q We ran G \to T We A)$
144	17 143	mpd	$⊢ φ \to T We A$

Metamath Proof Explorer

Theorem fnwelem

Proof