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		ffvelrn	$⊢ (F : A ⟶ B \land x \in A) \to F (x) \in B$
53		simpr	$⊢ (F : A ⟶ B \land x \in A) \to x \in A$
54	52 53	jca	$⊢ (F : A ⟶ B \land x \in A) \to (F (x) \in B \land x \in A)$
55		ffvelrn	$⊢ (F : A ⟶ B \land y \in A) \to F (y) \in B$
56		simpr	$⊢ (F : A ⟶ B \land y \in A) \to y \in A$
57	55 56	jca	$⊢ (F : A ⟶ B \land y \in A) \to (F (y) \in B \land y \in A)$
58	54 57	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))$
59	58	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))))$
60		eleq1	$⊢ u = ⟨F (x), x⟩ \to (u \in (B \times A) \leftrightarrow ⟨F (x), x⟩ \in (B \times A))$
61		opelxp	$⊢ ⟨F (x), x⟩ \in (B \times A) \leftrightarrow (F (x) \in B \land x \in A)$
62	60 61	syl6bb	$⊢ u = ⟨F (x), x⟩ \to (u \in (B \times A) \leftrightarrow (F (x) \in B \land x \in A))$
63	62	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)))$
64	29 30	op1std	$⊢ u = ⟨F (x), x⟩ \to 1^{st} (u) = F (x)$
65	64	breq1d	$⊢ u = ⟨F (x), x⟩ \to (1^{st} (u) R 1^{st} (v) \leftrightarrow F (x) R 1^{st} (v))$
66	64	eqeq1d	$⊢ u = ⟨F (x), x⟩ \to (1^{st} (u) = 1^{st} (v) \leftrightarrow F (x) = 1^{st} (v))$
67	29 30	op2ndd	$⊢ u = ⟨F (x), x⟩ \to 2^{nd} (u) = x$
68	67	breq1d	$⊢ u = ⟨F (x), x⟩ \to (2^{nd} (u) S 2^{nd} (v) \leftrightarrow x S 2^{nd} (v))$
69	66 68	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)))$
70	65 69	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))))$
71	63 70	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)))))$
72		eleq1	$⊢ v = ⟨F (y), y⟩ \to (v \in (B \times A) \leftrightarrow ⟨F (y), y⟩ \in (B \times A))$
73		opelxp	$⊢ ⟨F (y), y⟩ \in (B \times A) \leftrightarrow (F (y) \in B \land y \in A)$
74	72 73	syl6bb	$⊢ v = ⟨F (y), y⟩ \to (v \in (B \times A) \leftrightarrow (F (y) \in B \land y \in A))$
75	74	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)))$
76		fvex	$⊢ F (y) \in V$
77		vex	$⊢ y \in V$
78	76 77	op1std	$⊢ v = ⟨F (y), y⟩ \to 1^{st} (v) = F (y)$
79	78	breq2d	$⊢ v = ⟨F (y), y⟩ \to (F (x) R 1^{st} (v) \leftrightarrow F (x) R F (y))$
80	78	eqeq2d	$⊢ v = ⟨F (y), y⟩ \to (F (x) = 1^{st} (v) \leftrightarrow F (x) = F (y))$
81	76 77	op2ndd	$⊢ v = ⟨F (y), y⟩ \to 2^{nd} (v) = y$
82	81	breq2d	$⊢ v = ⟨F (y), y⟩ \to (x S 2^{nd} (v) \leftrightarrow x S y)$
83	80 82	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))$
84	79 83	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)))$
85	75 84	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))))$
86	21 26 71 85 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)))$
87	59 86	syl6rbbr	$⊢ (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		fndm	$⊢ F Fn A \to dom F = A$
116	112 115	syl	$⊢ (φ \land (x \in w \land x \in dom G)) \to dom F = A$
117	114 116	sseqtrid	$⊢ (φ \land (x \in w \land x \in dom G)) \to w \cap dom F \subseteq A$
118	113 117	eqsstrid	$⊢ (φ \land (x \in w \land x \in dom G)) \to dom ({F ↾}_{w}) \subseteq A$
119		simprl	$⊢ (φ \land (x \in w \land x \in dom G)) \to x \in w$
120	109 116	eleqtrrd	$⊢ (φ \land (x \in w \land x \in dom G)) \to x \in dom F$
121	113	elin2	$⊢ x \in dom ({F ↾}_{w}) \leftrightarrow (x \in w \land x \in dom F)$
122	119 120 121	sylanbrc	$⊢ (φ \land (x \in w \land x \in dom G)) \to x \in dom ({F ↾}_{w})$
123		fnfvima	$⊢ (F Fn A \land dom ({F ↾}_{w}) \subseteq A \land x \in dom ({F ↾}_{w})) \to F (x) \in F [dom ({F ↾}_{w})]$
124	112 118 122 123	syl3anc	$⊢ (φ \land (x \in w \land x \in dom G)) \to F (x) \in F [dom ({F ↾}_{w})]$
125		imadmres	$⊢ F [dom ({F ↾}_{w})] = F [w]$
126	124 125	eleqtrdi	$⊢ (φ \land (x \in w \land x \in dom G)) \to F (x) \in F [w]$
127	126 119	opelxpd	$⊢ (φ \land (x \in w \land x \in dom G)) \to ⟨F (x), x⟩ \in (F [w] \times w)$
128	110 127	eqeltrd	$⊢ (φ \land (x \in w \land x \in dom G)) \to G (x) \in (F [w] \times w)$
129	104 128	sylan2b	$⊢ (φ \land x \in dom ({G ↾}_{w})) \to G (x) \in (F [w] \times w)$
130	129	ralrimiva	$⊢ φ \to \forall x \in dom ({G ↾}_{w}) G (x) \in (F [w] \times w)$
131		f1fun	$⊢ G : A \underset{1-1}{⟶} B \times A \to Fun G$
132	2 36 131	3syl	$⊢ φ \to Fun G$
133		resss	$⊢ {G ↾}_{w} \subseteq G$
134		dmss	$⊢ {G ↾}_{w} \subseteq G \to dom ({G ↾}_{w}) \subseteq dom G$
135	133 134	ax-mp	$⊢ dom ({G ↾}_{w}) \subseteq dom G$
136		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))$
137	132 135 136	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))$
138	130 137	mpbird	$⊢ φ \to G [dom ({G ↾}_{w})] \subseteq F [w] \times w$
139	102 138	eqsstrrid	$⊢ φ \to G [w] \subseteq F [w] \times w$
140	101 139	ssexd	$⊢ φ \to G [w] \in V$
141	98 140	eqeltrid	$⊢ φ \to {G^{-1}}^{-1} [w] \in V$
142	141	alrimiv	$⊢ φ \to \forall w {G^{-1}}^{-1} [w] \in V$
143		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)$
144	97 142 143	syl2anc	$⊢ φ \to (Q We ran G \to T We A)$
145	17 144	mpd	$⊢ φ \to T We A$

Metamath Proof Explorer

Theorem fnwelem

Proof