imasaddfnlem

Description: The image structure operation is a function if the original operation is compatible with the function. (Contributed by Mario Carneiro, 23-Feb-2015)

	Ref	Expression
Hypotheses	imasaddf.f	$⊢ φ \to F : V \underset{onto}{⟶} B$
	imasaddf.e	$⊢ (φ \land (a \in V \land b \in V) \land (p \in V \land q \in V)) \to ((F (a) = F (p) \land F (b) = F (q)) \to F (a \underset{˙}{\cdot} b) = F (p \underset{˙}{\cdot} q))$
	imasaddflem.a	$⊢ φ \to \underset{˙}{∙} = ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\}$
Assertion	imasaddfnlem	$⊢ φ \to \underset{˙}{∙} Fn (B \times B)$

Proof

Step	Hyp	Ref	Expression
1		imasaddf.f	$⊢ φ \to F : V \underset{onto}{⟶} B$
2		imasaddf.e	$⊢ (φ \land (a \in V \land b \in V) \land (p \in V \land q \in V)) \to ((F (a) = F (p) \land F (b) = F (q)) \to F (a \underset{˙}{\cdot} b) = F (p \underset{˙}{\cdot} q))$
3		imasaddflem.a	$⊢ φ \to \underset{˙}{∙} = ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\}$
4		opex	$⊢ ⟨F (p), F (q)⟩ \in V$
5		fvex	$⊢ F (p \underset{˙}{\cdot} q) \in V$
6	4 5	relsnop	$⊢ Rel \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\}$
7	6	rgenw	$⊢ \forall q \in V Rel \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\}$
8		reliun	$⊢ Rel ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\} \leftrightarrow \forall q \in V Rel \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\}$
9	7 8	mpbir	$⊢ Rel ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\}$
10	9	rgenw	$⊢ \forall p \in V Rel ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\}$
11		reliun	$⊢ Rel ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\} \leftrightarrow \forall p \in V Rel ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\}$
12	10 11	mpbir	$⊢ Rel ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\}$
13	3	releqd	$⊢ φ \to (Rel \underset{˙}{∙} \leftrightarrow Rel ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\})$
14	12 13	mpbiri	$⊢ φ \to Rel \underset{˙}{∙}$
15		fof	$⊢ F : V \underset{onto}{⟶} B \to F : V ⟶ B$
16	1 15	syl	$⊢ φ \to F : V ⟶ B$
17		ffvelrn	$⊢ (F : V ⟶ B \land p \in V) \to F (p) \in B$
18		ffvelrn	$⊢ (F : V ⟶ B \land q \in V) \to F (q) \in B$
19	17 18	anim12dan	$⊢ (F : V ⟶ B \land (p \in V \land q \in V)) \to (F (p) \in B \land F (q) \in B)$
20	16 19	sylan	$⊢ (φ \land (p \in V \land q \in V)) \to (F (p) \in B \land F (q) \in B)$
21		opelxpi	$⊢ (F (p) \in B \land F (q) \in B) \to ⟨F (p), F (q)⟩ \in (B \times B)$
22	20 21	syl	$⊢ (φ \land (p \in V \land q \in V)) \to ⟨F (p), F (q)⟩ \in (B \times B)$
23		opelxpi	$⊢ (⟨F (p), F (q)⟩ \in (B \times B) \land F (p \underset{˙}{\cdot} q) \in V) \to ⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩ \in ((B \times B) \times V)$
24	22 5 23	sylancl	$⊢ (φ \land (p \in V \land q \in V)) \to ⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩ \in ((B \times B) \times V)$
25	24	snssd	$⊢ (φ \land (p \in V \land q \in V)) \to \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\} \subseteq (B \times B) \times V$
26	25	anassrs	$⊢ ((φ \land p \in V) \land q \in V) \to \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\} \subseteq (B \times B) \times V$
27	26	iunssd	$⊢ (φ \land p \in V) \to ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\} \subseteq (B \times B) \times V$
28	27	iunssd	$⊢ φ \to ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\} \subseteq (B \times B) \times V$
29	3 28	eqsstrd	$⊢ φ \to \underset{˙}{∙} \subseteq (B \times B) \times V$
30		dmss	$⊢ \underset{˙}{∙} \subseteq (B \times B) \times V \to dom \underset{˙}{∙} \subseteq dom ((B \times B) \times V)$
31	29 30	syl	$⊢ φ \to dom \underset{˙}{∙} \subseteq dom ((B \times B) \times V)$
32		vn0	$⊢ V \neq \emptyset$
33		dmxp	$⊢ V \neq \emptyset \to dom ((B \times B) \times V) = B \times B$
34	32 33	ax-mp	$⊢ dom ((B \times B) \times V) = B \times B$
35	31 34	sseqtrdi	$⊢ φ \to dom \underset{˙}{∙} \subseteq B \times B$
36		forn	$⊢ F : V \underset{onto}{⟶} B \to ran F = B$
37	1 36	syl	$⊢ φ \to ran F = B$
38	37	sqxpeqd	$⊢ φ \to ran F \times ran F = B \times B$
39	35 38	sseqtrrd	$⊢ φ \to dom \underset{˙}{∙} \subseteq ran F \times ran F$
40	3	eleq2d	$⊢ φ \to (⟨⟨F (a), F (b)⟩, w⟩ \in \underset{˙}{∙} \leftrightarrow ⟨⟨F (a), F (b)⟩, w⟩ \in ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\})$
41	40	adantr	$⊢ (φ \land (a \in V \land b \in V)) \to (⟨⟨F (a), F (b)⟩, w⟩ \in \underset{˙}{∙} \leftrightarrow ⟨⟨F (a), F (b)⟩, w⟩ \in ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\})$
42		df-br	$⊢ ⟨F (a), F (b)⟩ \underset{˙}{∙} w \leftrightarrow ⟨⟨F (a), F (b)⟩, w⟩ \in \underset{˙}{∙}$
43		eliun	$⊢ ⟨⟨F (a), F (b)⟩, w⟩ \in ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\} \leftrightarrow \exists p \in V ⟨⟨F (a), F (b)⟩, w⟩ \in ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\}$
44		eliun	$⊢ ⟨⟨F (a), F (b)⟩, w⟩ \in ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\} \leftrightarrow \exists q \in V ⟨⟨F (a), F (b)⟩, w⟩ \in \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\}$
45	44	rexbii	$⊢ \exists p \in V ⟨⟨F (a), F (b)⟩, w⟩ \in ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\} \leftrightarrow \exists p \in V \exists q \in V ⟨⟨F (a), F (b)⟩, w⟩ \in \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\}$
46	43 45	bitr2i	$⊢ \exists p \in V \exists q \in V ⟨⟨F (a), F (b)⟩, w⟩ \in \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\} \leftrightarrow ⟨⟨F (a), F (b)⟩, w⟩ \in ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\}$
47	41 42 46	3bitr4g	$⊢ (φ \land (a \in V \land b \in V)) \to (⟨F (a), F (b)⟩ \underset{˙}{∙} w \leftrightarrow \exists p \in V \exists q \in V ⟨⟨F (a), F (b)⟩, w⟩ \in \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\})$
48		opex	$⊢ ⟨⟨F (a), F (b)⟩, w⟩ \in V$
49	48	elsn	$⊢ ⟨⟨F (a), F (b)⟩, w⟩ \in \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\} \leftrightarrow ⟨⟨F (a), F (b)⟩, w⟩ = ⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩$
50		opex	$⊢ ⟨F (a), F (b)⟩ \in V$
51		vex	$⊢ w \in V$
52	50 51	opth	$⊢ ⟨⟨F (a), F (b)⟩, w⟩ = ⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩ \leftrightarrow (⟨F (a), F (b)⟩ = ⟨F (p), F (q)⟩ \land w = F (p \underset{˙}{\cdot} q))$
53		fvex	$⊢ F (a) \in V$
54		fvex	$⊢ F (b) \in V$
55	53 54	opth	$⊢ ⟨F (a), F (b)⟩ = ⟨F (p), F (q)⟩ \leftrightarrow (F (a) = F (p) \land F (b) = F (q))$
56	55 2	syl5bi	$⊢ (φ \land (a \in V \land b \in V) \land (p \in V \land q \in V)) \to (⟨F (a), F (b)⟩ = ⟨F (p), F (q)⟩ \to F (a \underset{˙}{\cdot} b) = F (p \underset{˙}{\cdot} q))$
57		eqeq2	$⊢ F (a \underset{˙}{\cdot} b) = F (p \underset{˙}{\cdot} q) \to (w = F (a \underset{˙}{\cdot} b) \leftrightarrow w = F (p \underset{˙}{\cdot} q))$
58	57	biimprd	$⊢ F (a \underset{˙}{\cdot} b) = F (p \underset{˙}{\cdot} q) \to (w = F (p \underset{˙}{\cdot} q) \to w = F (a \underset{˙}{\cdot} b))$
59	56 58	syl6	$⊢ (φ \land (a \in V \land b \in V) \land (p \in V \land q \in V)) \to (⟨F (a), F (b)⟩ = ⟨F (p), F (q)⟩ \to (w = F (p \underset{˙}{\cdot} q) \to w = F (a \underset{˙}{\cdot} b)))$
60	59	impd	$⊢ (φ \land (a \in V \land b \in V) \land (p \in V \land q \in V)) \to ((⟨F (a), F (b)⟩ = ⟨F (p), F (q)⟩ \land w = F (p \underset{˙}{\cdot} q)) \to w = F (a \underset{˙}{\cdot} b))$
61	52 60	syl5bi	$⊢ (φ \land (a \in V \land b \in V) \land (p \in V \land q \in V)) \to (⟨⟨F (a), F (b)⟩, w⟩ = ⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩ \to w = F (a \underset{˙}{\cdot} b))$
62	49 61	syl5bi	$⊢ (φ \land (a \in V \land b \in V) \land (p \in V \land q \in V)) \to (⟨⟨F (a), F (b)⟩, w⟩ \in \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\} \to w = F (a \underset{˙}{\cdot} b))$
63	62	3expa	$⊢ ((φ \land (a \in V \land b \in V)) \land (p \in V \land q \in V)) \to (⟨⟨F (a), F (b)⟩, w⟩ \in \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\} \to w = F (a \underset{˙}{\cdot} b))$
64	63	rexlimdvva	$⊢ (φ \land (a \in V \land b \in V)) \to (\exists p \in V \exists q \in V ⟨⟨F (a), F (b)⟩, w⟩ \in \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\} \to w = F (a \underset{˙}{\cdot} b))$
65	47 64	sylbid	$⊢ (φ \land (a \in V \land b \in V)) \to (⟨F (a), F (b)⟩ \underset{˙}{∙} w \to w = F (a \underset{˙}{\cdot} b))$
66	65	alrimiv	$⊢ (φ \land (a \in V \land b \in V)) \to \forall w (⟨F (a), F (b)⟩ \underset{˙}{∙} w \to w = F (a \underset{˙}{\cdot} b))$
67		mo2icl	$⊢ \forall w (⟨F (a), F (b)⟩ \underset{˙}{∙} w \to w = F (a \underset{˙}{\cdot} b)) \to \exists^{*} w ⟨F (a), F (b)⟩ \underset{˙}{∙} w$
68	66 67	syl	$⊢ (φ \land (a \in V \land b \in V)) \to \exists^{*} w ⟨F (a), F (b)⟩ \underset{˙}{∙} w$
69	68	ralrimivva	$⊢ φ \to \forall a \in V \forall b \in V \exists^{*} w ⟨F (a), F (b)⟩ \underset{˙}{∙} w$
70		fofn	$⊢ F : V \underset{onto}{⟶} B \to F Fn V$
71	1 70	syl	$⊢ φ \to F Fn V$
72		opeq2	$⊢ z = F (b) \to ⟨F (a), z⟩ = ⟨F (a), F (b)⟩$
73	72	breq1d	$⊢ z = F (b) \to (⟨F (a), z⟩ \underset{˙}{∙} w \leftrightarrow ⟨F (a), F (b)⟩ \underset{˙}{∙} w)$
74	73	mobidv	$⊢ z = F (b) \to (\exists^{} w ⟨F (a), z⟩ \underset{˙}{∙} w \leftrightarrow \exists^{} w ⟨F (a), F (b)⟩ \underset{˙}{∙} w)$
75	74	ralrn	$⊢ F Fn V \to (\forall z \in ran F \exists^{} w ⟨F (a), z⟩ \underset{˙}{∙} w \leftrightarrow \forall b \in V \exists^{} w ⟨F (a), F (b)⟩ \underset{˙}{∙} w)$
76	71 75	syl	$⊢ φ \to (\forall z \in ran F \exists^{} w ⟨F (a), z⟩ \underset{˙}{∙} w \leftrightarrow \forall b \in V \exists^{} w ⟨F (a), F (b)⟩ \underset{˙}{∙} w)$
77	76	ralbidv	$⊢ φ \to (\forall a \in V \forall z \in ran F \exists^{} w ⟨F (a), z⟩ \underset{˙}{∙} w \leftrightarrow \forall a \in V \forall b \in V \exists^{} w ⟨F (a), F (b)⟩ \underset{˙}{∙} w)$
78	69 77	mpbird	$⊢ φ \to \forall a \in V \forall z \in ran F \exists^{*} w ⟨F (a), z⟩ \underset{˙}{∙} w$
79		opeq1	$⊢ y = F (a) \to ⟨y, z⟩ = ⟨F (a), z⟩$
80	79	breq1d	$⊢ y = F (a) \to (⟨y, z⟩ \underset{˙}{∙} w \leftrightarrow ⟨F (a), z⟩ \underset{˙}{∙} w)$
81	80	mobidv	$⊢ y = F (a) \to (\exists^{} w ⟨y, z⟩ \underset{˙}{∙} w \leftrightarrow \exists^{} w ⟨F (a), z⟩ \underset{˙}{∙} w)$
82	81	ralbidv	$⊢ y = F (a) \to (\forall z \in ran F \exists^{} w ⟨y, z⟩ \underset{˙}{∙} w \leftrightarrow \forall z \in ran F \exists^{} w ⟨F (a), z⟩ \underset{˙}{∙} w)$
83	82	ralrn	$⊢ F Fn V \to (\forall y \in ran F \forall z \in ran F \exists^{} w ⟨y, z⟩ \underset{˙}{∙} w \leftrightarrow \forall a \in V \forall z \in ran F \exists^{} w ⟨F (a), z⟩ \underset{˙}{∙} w)$
84	71 83	syl	$⊢ φ \to (\forall y \in ran F \forall z \in ran F \exists^{} w ⟨y, z⟩ \underset{˙}{∙} w \leftrightarrow \forall a \in V \forall z \in ran F \exists^{} w ⟨F (a), z⟩ \underset{˙}{∙} w)$
85	78 84	mpbird	$⊢ φ \to \forall y \in ran F \forall z \in ran F \exists^{*} w ⟨y, z⟩ \underset{˙}{∙} w$
86		breq1	$⊢ x = ⟨y, z⟩ \to (x \underset{˙}{∙} w \leftrightarrow ⟨y, z⟩ \underset{˙}{∙} w)$
87	86	mobidv	$⊢ x = ⟨y, z⟩ \to (\exists^{} w x \underset{˙}{∙} w \leftrightarrow \exists^{} w ⟨y, z⟩ \underset{˙}{∙} w)$
88	87	ralxp	$⊢ \forall x \in (ran F \times ran F) \exists^{} w x \underset{˙}{∙} w \leftrightarrow \forall y \in ran F \forall z \in ran F \exists^{} w ⟨y, z⟩ \underset{˙}{∙} w$
89	85 88	sylibr	$⊢ φ \to \forall x \in (ran F \times ran F) \exists^{*} w x \underset{˙}{∙} w$
90		ssralv	$⊢ dom \underset{˙}{∙} \subseteq ran F \times ran F \to (\forall x \in (ran F \times ran F) \exists^{} w x \underset{˙}{∙} w \to \forall x \in dom \underset{˙}{∙} \exists^{} w x \underset{˙}{∙} w)$
91	39 89 90	sylc	$⊢ φ \to \forall x \in dom \underset{˙}{∙} \exists^{*} w x \underset{˙}{∙} w$
92		dffun7	$⊢ Fun \underset{˙}{∙} \leftrightarrow (Rel \underset{˙}{∙} \land \forall x \in dom \underset{˙}{∙} \exists^{*} w x \underset{˙}{∙} w)$
93	14 91 92	sylanbrc	$⊢ φ \to Fun \underset{˙}{∙}$
94		eqimss2	$⊢ \underset{˙}{∙} = ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\} \to ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\} \subseteq \underset{˙}{∙}$
95	3 94	syl	$⊢ φ \to ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\} \subseteq \underset{˙}{∙}$
96		iunss	$⊢ ⋃_{p \in V} ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\} \subseteq \underset{˙}{∙} \leftrightarrow \forall p \in V ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\} \subseteq \underset{˙}{∙}$
97	95 96	sylib	$⊢ φ \to \forall p \in V ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\} \subseteq \underset{˙}{∙}$
98		iunss	$⊢ ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\} \subseteq \underset{˙}{∙} \leftrightarrow \forall q \in V \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\} \subseteq \underset{˙}{∙}$
99		opex	$⊢ ⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩ \in V$
100	99	snss	$⊢ ⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩ \in \underset{˙}{∙} \leftrightarrow \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\} \subseteq \underset{˙}{∙}$
101	4 5	opeldm	$⊢ ⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩ \in \underset{˙}{∙} \to ⟨F (p), F (q)⟩ \in dom \underset{˙}{∙}$
102	100 101	sylbir	$⊢ \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\} \subseteq \underset{˙}{∙} \to ⟨F (p), F (q)⟩ \in dom \underset{˙}{∙}$
103	102	ralimi	$⊢ \forall q \in V \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\} \subseteq \underset{˙}{∙} \to \forall q \in V ⟨F (p), F (q)⟩ \in dom \underset{˙}{∙}$
104	98 103	sylbi	$⊢ ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\} \subseteq \underset{˙}{∙} \to \forall q \in V ⟨F (p), F (q)⟩ \in dom \underset{˙}{∙}$
105	104	ralimi	$⊢ \forall p \in V ⋃_{q \in V} \{⟨⟨F (p), F (q)⟩, F (p \underset{˙}{\cdot} q)⟩\} \subseteq \underset{˙}{∙} \to \forall p \in V \forall q \in V ⟨F (p), F (q)⟩ \in dom \underset{˙}{∙}$
106	97 105	syl	$⊢ φ \to \forall p \in V \forall q \in V ⟨F (p), F (q)⟩ \in dom \underset{˙}{∙}$
107		opeq2	$⊢ z = F (q) \to ⟨F (p), z⟩ = ⟨F (p), F (q)⟩$
108	107	eleq1d	$⊢ z = F (q) \to (⟨F (p), z⟩ \in dom \underset{˙}{∙} \leftrightarrow ⟨F (p), F (q)⟩ \in dom \underset{˙}{∙})$
109	108	ralrn	$⊢ F Fn V \to (\forall z \in ran F ⟨F (p), z⟩ \in dom \underset{˙}{∙} \leftrightarrow \forall q \in V ⟨F (p), F (q)⟩ \in dom \underset{˙}{∙})$
110	71 109	syl	$⊢ φ \to (\forall z \in ran F ⟨F (p), z⟩ \in dom \underset{˙}{∙} \leftrightarrow \forall q \in V ⟨F (p), F (q)⟩ \in dom \underset{˙}{∙})$
111	110	ralbidv	$⊢ φ \to (\forall p \in V \forall z \in ran F ⟨F (p), z⟩ \in dom \underset{˙}{∙} \leftrightarrow \forall p \in V \forall q \in V ⟨F (p), F (q)⟩ \in dom \underset{˙}{∙})$
112	106 111	mpbird	$⊢ φ \to \forall p \in V \forall z \in ran F ⟨F (p), z⟩ \in dom \underset{˙}{∙}$
113		opeq1	$⊢ y = F (p) \to ⟨y, z⟩ = ⟨F (p), z⟩$
114	113	eleq1d	$⊢ y = F (p) \to (⟨y, z⟩ \in dom \underset{˙}{∙} \leftrightarrow ⟨F (p), z⟩ \in dom \underset{˙}{∙})$
115	114	ralbidv	$⊢ y = F (p) \to (\forall z \in ran F ⟨y, z⟩ \in dom \underset{˙}{∙} \leftrightarrow \forall z \in ran F ⟨F (p), z⟩ \in dom \underset{˙}{∙})$
116	115	ralrn	$⊢ F Fn V \to (\forall y \in ran F \forall z \in ran F ⟨y, z⟩ \in dom \underset{˙}{∙} \leftrightarrow \forall p \in V \forall z \in ran F ⟨F (p), z⟩ \in dom \underset{˙}{∙})$
117	71 116	syl	$⊢ φ \to (\forall y \in ran F \forall z \in ran F ⟨y, z⟩ \in dom \underset{˙}{∙} \leftrightarrow \forall p \in V \forall z \in ran F ⟨F (p), z⟩ \in dom \underset{˙}{∙})$
118	112 117	mpbird	$⊢ φ \to \forall y \in ran F \forall z \in ran F ⟨y, z⟩ \in dom \underset{˙}{∙}$
119		eleq1	$⊢ x = ⟨y, z⟩ \to (x \in dom \underset{˙}{∙} \leftrightarrow ⟨y, z⟩ \in dom \underset{˙}{∙})$
120	119	ralxp	$⊢ \forall x \in (ran F \times ran F) x \in dom \underset{˙}{∙} \leftrightarrow \forall y \in ran F \forall z \in ran F ⟨y, z⟩ \in dom \underset{˙}{∙}$
121	118 120	sylibr	$⊢ φ \to \forall x \in (ran F \times ran F) x \in dom \underset{˙}{∙}$
122		dfss3	$⊢ ran F \times ran F \subseteq dom \underset{˙}{∙} \leftrightarrow \forall x \in (ran F \times ran F) x \in dom \underset{˙}{∙}$
123	121 122	sylibr	$⊢ φ \to ran F \times ran F \subseteq dom \underset{˙}{∙}$
124	38 123	eqsstrrd	$⊢ φ \to B \times B \subseteq dom \underset{˙}{∙}$
125	35 124	eqssd	$⊢ φ \to dom \underset{˙}{∙} = B \times B$
126		df-fn	$⊢ \underset{˙}{∙} Fn (B \times B) \leftrightarrow (Fun \underset{˙}{∙} \land dom \underset{˙}{∙} = B \times B)$
127	93 125 126	sylanbrc	$⊢ φ \to \underset{˙}{∙} Fn (B \times B)$

Metamath Proof Explorer

Theorem imasaddfnlem

Proof