fpwrelmapffslem

Description: Lemma for fpwrelmapffs . For this theorem, the sets A and B could be infinite, but the relation R itself is finite. (Contributed by Thierry Arnoux, 1-Sep-2017) (Revised by Thierry Arnoux, 1-Sep-2019)

	Ref	Expression
Hypotheses	fpwrelmapffslem.1	$⊢ A \in V$
	fpwrelmapffslem.2	$⊢ B \in V$
	fpwrelmapffslem.3	$⊢ φ \to F : A ⟶ 𝒫 B$
	fpwrelmapffslem.4	$⊢ φ \to R = \{⟨x, y⟩ \| (x \in A \land y \in F (x))\}$
Assertion	fpwrelmapffslem	$⊢ φ \to (R \in Fin \leftrightarrow (ran F \subseteq Fin \land F supp \emptyset \in Fin))$

Proof

Step	Hyp	Ref	Expression
1		fpwrelmapffslem.1	$⊢ A \in V$
2		fpwrelmapffslem.2	$⊢ B \in V$
3		fpwrelmapffslem.3	$⊢ φ \to F : A ⟶ 𝒫 B$
4		fpwrelmapffslem.4	$⊢ φ \to R = \{⟨x, y⟩ \| (x \in A \land y \in F (x))\}$
5		relopab	$⊢ Rel \{⟨x, y⟩ \| (x \in A \land y \in F (x))\}$
6		releq	$⊢ R = \{⟨x, y⟩ \| (x \in A \land y \in F (x))\} \to (Rel R \leftrightarrow Rel \{⟨x, y⟩ \| (x \in A \land y \in F (x))\})$
7	5 6	mpbiri	$⊢ R = \{⟨x, y⟩ \| (x \in A \land y \in F (x))\} \to Rel R$
8		relfi	$⊢ Rel R \to (R \in Fin \leftrightarrow (dom R \in Fin \land ran R \in Fin))$
9	4 7 8	3syl	$⊢ φ \to (R \in Fin \leftrightarrow (dom R \in Fin \land ran R \in Fin))$
10		rexcom4	$⊢ \exists x \in A \exists z (w \in z \land z = F (x)) \leftrightarrow \exists z \exists x \in A (w \in z \land z = F (x))$
11		ancom	$⊢ (z = F (x) \land w \in z) \leftrightarrow (w \in z \land z = F (x))$
12	11	exbii	$⊢ \exists z (z = F (x) \land w \in z) \leftrightarrow \exists z (w \in z \land z = F (x))$
13		fvex	$⊢ F (x) \in V$
14		eleq2	$⊢ z = F (x) \to (w \in z \leftrightarrow w \in F (x))$
15	13 14	ceqsexv	$⊢ \exists z (z = F (x) \land w \in z) \leftrightarrow w \in F (x)$
16	12 15	bitr3i	$⊢ \exists z (w \in z \land z = F (x)) \leftrightarrow w \in F (x)$
17	16	rexbii	$⊢ \exists x \in A \exists z (w \in z \land z = F (x)) \leftrightarrow \exists x \in A w \in F (x)$
18		r19.42v	$⊢ \exists x \in A (w \in z \land z = F (x)) \leftrightarrow (w \in z \land \exists x \in A z = F (x))$
19	18	exbii	$⊢ \exists z \exists x \in A (w \in z \land z = F (x)) \leftrightarrow \exists z (w \in z \land \exists x \in A z = F (x))$
20	10 17 19	3bitr3ri	$⊢ \exists z (w \in z \land \exists x \in A z = F (x)) \leftrightarrow \exists x \in A w \in F (x)$
21		df-rex	$⊢ \exists x \in A w \in F (x) \leftrightarrow \exists x (x \in A \land w \in F (x))$
22	20 21	bitr2i	$⊢ \exists x (x \in A \land w \in F (x)) \leftrightarrow \exists z (w \in z \land \exists x \in A z = F (x))$
23	22	a1i	$⊢ φ \to (\exists x (x \in A \land w \in F (x)) \leftrightarrow \exists z (w \in z \land \exists x \in A z = F (x)))$
24		vex	$⊢ w \in V$
25		eleq1w	$⊢ y = w \to (y \in F (x) \leftrightarrow w \in F (x))$
26	25	anbi2d	$⊢ y = w \to ((x \in A \land y \in F (x)) \leftrightarrow (x \in A \land w \in F (x)))$
27	26	exbidv	$⊢ y = w \to (\exists x (x \in A \land y \in F (x)) \leftrightarrow \exists x (x \in A \land w \in F (x)))$
28	24 27	elab	$⊢ w \in \{y \| \exists x (x \in A \land y \in F (x))\} \leftrightarrow \exists x (x \in A \land w \in F (x))$
29		eluniab	$⊢ w \in ⋃ \{z \| \exists x \in A z = F (x)\} \leftrightarrow \exists z (w \in z \land \exists x \in A z = F (x))$
30	23 28 29	3bitr4g	$⊢ φ \to (w \in \{y \| \exists x (x \in A \land y \in F (x))\} \leftrightarrow w \in ⋃ \{z \| \exists x \in A z = F (x)\})$
31	30	eqrdv	$⊢ φ \to \{y \| \exists x (x \in A \land y \in F (x))\} = ⋃ \{z \| \exists x \in A z = F (x)\}$
32	31	eleq1d	$⊢ φ \to (\{y \| \exists x (x \in A \land y \in F (x))\} \in Fin \leftrightarrow ⋃ \{z \| \exists x \in A z = F (x)\} \in Fin)$
33	32	adantr	$⊢ (φ \land dom R \in Fin) \to (\{y \| \exists x (x \in A \land y \in F (x))\} \in Fin \leftrightarrow ⋃ \{z \| \exists x \in A z = F (x)\} \in Fin)$
34		ffn	$⊢ F : A ⟶ 𝒫 B \to F Fn A$
35		fnrnfv	$⊢ F Fn A \to ran F = \{z \| \exists x \in A z = F (x)\}$
36	3 34 35	3syl	$⊢ φ \to ran F = \{z \| \exists x \in A z = F (x)\}$
37	36	adantr	$⊢ (φ \land dom R \in Fin) \to ran F = \{z \| \exists x \in A z = F (x)\}$
38		0ex	$⊢ \emptyset \in V$
39	38	a1i	$⊢ (φ \land dom R \in Fin) \to \emptyset \in V$
40		fex	$⊢ (F : A ⟶ 𝒫 B \land A \in V) \to F \in V$
41	3 1 40	sylancl	$⊢ φ \to F \in V$
42	41	adantr	$⊢ (φ \land dom R \in Fin) \to F \in V$
43	3	ffund	$⊢ φ \to Fun F$
44	43	adantr	$⊢ (φ \land dom R \in Fin) \to Fun F$
45		opabdm	$⊢ R = \{⟨x, y⟩ \| (x \in A \land y \in F (x))\} \to dom R = \{x \| \exists y (x \in A \land y \in F (x))\}$
46	4 45	syl	$⊢ φ \to dom R = \{x \| \exists y (x \in A \land y \in F (x))\}$
47	1 40	mpan2	$⊢ F : A ⟶ 𝒫 B \to F \in V$
48		suppimacnv	$⊢ (F \in V \land \emptyset \in V) \to F supp \emptyset = F^{-1} [V ∖ \{\emptyset\}]$
49	38 48	mpan2	$⊢ F \in V \to F supp \emptyset = F^{-1} [V ∖ \{\emptyset\}]$
50	3 47 49	3syl	$⊢ φ \to F supp \emptyset = F^{-1} [V ∖ \{\emptyset\}]$
51	3	feqmptd	$⊢ φ \to F = (x \in A ⟼ F (x))$
52	51	cnveqd	$⊢ φ \to F^{-1} = {(x \in A ⟼ F (x))}^{-1}$
53	52	imaeq1d	$⊢ φ \to F^{-1} [V ∖ \{\emptyset\}] = {(x \in A ⟼ F (x))}^{-1} [V ∖ \{\emptyset\}]$
54	50 53	eqtrd	$⊢ φ \to F supp \emptyset = {(x \in A ⟼ F (x))}^{-1} [V ∖ \{\emptyset\}]$
55		eqid	$⊢ (x \in A ⟼ F (x)) = (x \in A ⟼ F (x))$
56	55	mptpreima	$⊢ {(x \in A ⟼ F (x))}^{-1} [V ∖ \{\emptyset\}] = \{x \in A \| F (x) \in (V ∖ \{\emptyset\})\}$
57	54 56	eqtrdi	$⊢ φ \to F supp \emptyset = \{x \in A \| F (x) \in (V ∖ \{\emptyset\})\}$
58		suppvalfn	$⊢ (F Fn A \land A \in V \land \emptyset \in V) \to F supp \emptyset = \{x \in A \| F (x) \neq \emptyset\}$
59	1 38 58	mp3an23	$⊢ F Fn A \to F supp \emptyset = \{x \in A \| F (x) \neq \emptyset\}$
60	3 34 59	3syl	$⊢ φ \to F supp \emptyset = \{x \in A \| F (x) \neq \emptyset\}$
61		n0	$⊢ F (x) \neq \emptyset \leftrightarrow \exists y y \in F (x)$
62	61	rabbii	$⊢ \{x \in A \| F (x) \neq \emptyset\} = \{x \in A \| \exists y y \in F (x)\}$
63	62	a1i	$⊢ φ \to \{x \in A \| F (x) \neq \emptyset\} = \{x \in A \| \exists y y \in F (x)\}$
64	60 57 63	3eqtr3d	$⊢ φ \to \{x \in A \| F (x) \in (V ∖ \{\emptyset\})\} = \{x \in A \| \exists y y \in F (x)\}$
65		df-rab	$⊢ \{x \in A \| \exists y y \in F (x)\} = \{x \| (x \in A \land \exists y y \in F (x))\}$
66		19.42v	$⊢ \exists y (x \in A \land y \in F (x)) \leftrightarrow (x \in A \land \exists y y \in F (x))$
67	66	abbii	$⊢ \{x \| \exists y (x \in A \land y \in F (x))\} = \{x \| (x \in A \land \exists y y \in F (x))\}$
68	65 67	eqtr4i	$⊢ \{x \in A \| \exists y y \in F (x)\} = \{x \| \exists y (x \in A \land y \in F (x))\}$
69	68	a1i	$⊢ φ \to \{x \in A \| \exists y y \in F (x)\} = \{x \| \exists y (x \in A \land y \in F (x))\}$
70	57 64 69	3eqtrd	$⊢ φ \to F supp \emptyset = \{x \| \exists y (x \in A \land y \in F (x))\}$
71	46 70	eqtr4d	$⊢ φ \to dom R = F supp \emptyset$
72	71	eleq1d	$⊢ φ \to (dom R \in Fin \leftrightarrow F supp \emptyset \in Fin)$
73	72	biimpa	$⊢ (φ \land dom R \in Fin) \to F supp \emptyset \in Fin$
74	39 42 44 73	ffsrn	$⊢ (φ \land dom R \in Fin) \to ran F \in Fin$
75	37 74	eqeltrrd	$⊢ (φ \land dom R \in Fin) \to \{z \| \exists x \in A z = F (x)\} \in Fin$
76		unifi	$⊢ (\{z \| \exists x \in A z = F (x)\} \in Fin \land \{z \| \exists x \in A z = F (x)\} \subseteq Fin) \to ⋃ \{z \| \exists x \in A z = F (x)\} \in Fin$
77	76	ex	$⊢ \{z \| \exists x \in A z = F (x)\} \in Fin \to (\{z \| \exists x \in A z = F (x)\} \subseteq Fin \to ⋃ \{z \| \exists x \in A z = F (x)\} \in Fin)$
78	75 77	syl	$⊢ (φ \land dom R \in Fin) \to (\{z \| \exists x \in A z = F (x)\} \subseteq Fin \to ⋃ \{z \| \exists x \in A z = F (x)\} \in Fin)$
79		unifi3	$⊢ ⋃ \{z \| \exists x \in A z = F (x)\} \in Fin \to \{z \| \exists x \in A z = F (x)\} \subseteq Fin$
80	78 79	impbid1	$⊢ (φ \land dom R \in Fin) \to (\{z \| \exists x \in A z = F (x)\} \subseteq Fin \leftrightarrow ⋃ \{z \| \exists x \in A z = F (x)\} \in Fin)$
81	33 80	bitr4d	$⊢ (φ \land dom R \in Fin) \to (\{y \| \exists x (x \in A \land y \in F (x))\} \in Fin \leftrightarrow \{z \| \exists x \in A z = F (x)\} \subseteq Fin)$
82		opabrn	$⊢ R = \{⟨x, y⟩ \| (x \in A \land y \in F (x))\} \to ran R = \{y \| \exists x (x \in A \land y \in F (x))\}$
83	4 82	syl	$⊢ φ \to ran R = \{y \| \exists x (x \in A \land y \in F (x))\}$
84	83	eleq1d	$⊢ φ \to (ran R \in Fin \leftrightarrow \{y \| \exists x (x \in A \land y \in F (x))\} \in Fin)$
85	84	adantr	$⊢ (φ \land dom R \in Fin) \to (ran R \in Fin \leftrightarrow \{y \| \exists x (x \in A \land y \in F (x))\} \in Fin)$
86	37	sseq1d	$⊢ (φ \land dom R \in Fin) \to (ran F \subseteq Fin \leftrightarrow \{z \| \exists x \in A z = F (x)\} \subseteq Fin)$
87	81 85 86	3bitr4d	$⊢ (φ \land dom R \in Fin) \to (ran R \in Fin \leftrightarrow ran F \subseteq Fin)$
88	87	pm5.32da	$⊢ φ \to ((dom R \in Fin \land ran R \in Fin) \leftrightarrow (dom R \in Fin \land ran F \subseteq Fin))$
89	72	anbi1d	$⊢ φ \to ((dom R \in Fin \land ran F \subseteq Fin) \leftrightarrow (F supp \emptyset \in Fin \land ran F \subseteq Fin))$
90	88 89	bitrd	$⊢ φ \to ((dom R \in Fin \land ran R \in Fin) \leftrightarrow (F supp \emptyset \in Fin \land ran F \subseteq Fin))$
91		ancom	$⊢ (F supp \emptyset \in Fin \land ran F \subseteq Fin) \leftrightarrow (ran F \subseteq Fin \land F supp \emptyset \in Fin)$
92	91	a1i	$⊢ φ \to ((F supp \emptyset \in Fin \land ran F \subseteq Fin) \leftrightarrow (ran F \subseteq Fin \land F supp \emptyset \in Fin))$
93	9 90 92	3bitrd	$⊢ φ \to (R \in Fin \leftrightarrow (ran F \subseteq Fin \land F supp \emptyset \in Fin))$

Metamath Proof Explorer

Theorem fpwrelmapffslem

Proof