hasheuni

Description: The cardinality of a disjoint union, not necessarily finite. cf. hashuni . (Contributed by Thierry Arnoux, 19-Nov-2016) (Revised by Thierry Arnoux, 2-Jan-2017) (Revised by Thierry Arnoux, 20-Jun-2017)

		Ref	Expression
	Assertion	hasheuni	$⊢ (A \in V \land \underset{x \in A}{Disj} x) \to \|⋃ A\| = \underset{x \in A}{\sum^{*}} \|x\|$

Proof

Step	Hyp	Ref	Expression
1		nfdisj1	$⊢ Ⅎ x \underset{x \in A}{Disj} x$
2		nfv	$⊢ Ⅎ x A \in Fin$
3		nfv	$⊢ Ⅎ x A \subseteq Fin$
4	1 2 3	nf3an	$⊢ Ⅎ x (\underset{x \in A}{Disj} x \land A \in Fin \land A \subseteq Fin)$
5		simp2	$⊢ (\underset{x \in A}{Disj} x \land A \in Fin \land A \subseteq Fin) \to A \in Fin$
6		simp3	$⊢ (\underset{x \in A}{Disj} x \land A \in Fin \land A \subseteq Fin) \to A \subseteq Fin$
7		simp1	$⊢ (\underset{x \in A}{Disj} x \land A \in Fin \land A \subseteq Fin) \to \underset{x \in A}{Disj} x$
8	4 5 6 7	hashunif	$⊢ (\underset{x \in A}{Disj} x \land A \in Fin \land A \subseteq Fin) \to \|⋃ A\| = \sum_{x \in A} \|x\|$
9		simpl	$⊢ (A \in Fin \land A \subseteq Fin) \to A \in Fin$
10		dfss3	$⊢ A \subseteq Fin \leftrightarrow \forall x \in A x \in Fin$
11		hashcl	$⊢ x \in Fin \to \|x\| \in ℕ_{0}$
12		nn0re	$⊢ \|x\| \in ℕ_{0} \to \|x\| \in ℝ$
13		nn0ge0	$⊢ \|x\| \in ℕ_{0} \to 0 \leq \|x\|$
14		elrege0	$⊢ \|x\| \in [0, +∞) \leftrightarrow (\|x\| \in ℝ \land 0 \leq \|x\|)$
15	12 13 14	sylanbrc	$⊢ \|x\| \in ℕ_{0} \to \|x\| \in [0, +∞)$
16	11 15	syl	$⊢ x \in Fin \to \|x\| \in [0, +∞)$
17	16	ralimi	$⊢ \forall x \in A x \in Fin \to \forall x \in A \|x\| \in [0, +∞)$
18	10 17	sylbi	$⊢ A \subseteq Fin \to \forall x \in A \|x\| \in [0, +∞)$
19	18	r19.21bi	$⊢ (A \subseteq Fin \land x \in A) \to \|x\| \in [0, +∞)$
20	19	adantll	$⊢ ((A \in Fin \land A \subseteq Fin) \land x \in A) \to \|x\| \in [0, +∞)$
21	9 20	esumpfinval	$⊢ (A \in Fin \land A \subseteq Fin) \to \underset{x \in A}{\sum^{*}} \|x\| = \sum_{x \in A} \|x\|$
22	21	3adant1	$⊢ (\underset{x \in A}{Disj} x \land A \in Fin \land A \subseteq Fin) \to \underset{x \in A}{\sum^{*}} \|x\| = \sum_{x \in A} \|x\|$
23	8 22	eqtr4d	$⊢ (\underset{x \in A}{Disj} x \land A \in Fin \land A \subseteq Fin) \to \|⋃ A\| = \underset{x \in A}{\sum^{*}} \|x\|$
24	23	3adant1l	$⊢ ((A \in V \land \underset{x \in A}{Disj} x) \land A \in Fin \land A \subseteq Fin) \to \|⋃ A\| = \underset{x \in A}{\sum^{*}} \|x\|$
25	24	3expa	$⊢ (((A \in V \land \underset{x \in A}{Disj} x) \land A \in Fin) \land A \subseteq Fin) \to \|⋃ A\| = \underset{x \in A}{\sum^{*}} \|x\|$
26		uniexg	$⊢ A \in V \to ⋃ A \in V$
27	10	notbii	$⊢ \neg A \subseteq Fin \leftrightarrow \neg \forall x \in A x \in Fin$
28		rexnal	$⊢ \exists x \in A \neg x \in Fin \leftrightarrow \neg \forall x \in A x \in Fin$
29	27 28	bitr4i	$⊢ \neg A \subseteq Fin \leftrightarrow \exists x \in A \neg x \in Fin$
30		elssuni	$⊢ x \in A \to x \subseteq ⋃ A$
31		ssfi	$⊢ (⋃ A \in Fin \land x \subseteq ⋃ A) \to x \in Fin$
32	31	expcom	$⊢ x \subseteq ⋃ A \to (⋃ A \in Fin \to x \in Fin)$
33	32	con3d	$⊢ x \subseteq ⋃ A \to (\neg x \in Fin \to \neg ⋃ A \in Fin)$
34	30 33	syl	$⊢ x \in A \to (\neg x \in Fin \to \neg ⋃ A \in Fin)$
35	34	rexlimiv	$⊢ \exists x \in A \neg x \in Fin \to \neg ⋃ A \in Fin$
36	29 35	sylbi	$⊢ \neg A \subseteq Fin \to \neg ⋃ A \in Fin$
37		hashinf	$⊢ (⋃ A \in V \land \neg ⋃ A \in Fin) \to \|⋃ A\| = +∞$
38	26 36 37	syl2an	$⊢ (A \in V \land \neg A \subseteq Fin) \to \|⋃ A\| = +∞$
39		vex	$⊢ x \in V$
40		hashinf	$⊢ (x \in V \land \neg x \in Fin) \to \|x\| = +∞$
41	39 40	mpan	$⊢ \neg x \in Fin \to \|x\| = +∞$
42	41	reximi	$⊢ \exists x \in A \neg x \in Fin \to \exists x \in A \|x\| = +∞$
43	29 42	sylbi	$⊢ \neg A \subseteq Fin \to \exists x \in A \|x\| = +∞$
44		nfv	$⊢ Ⅎ x A \in V$
45		nfre1	$⊢ Ⅎ x \exists x \in A \|x\| = +∞$
46	44 45	nfan	$⊢ Ⅎ x (A \in V \land \exists x \in A \|x\| = +∞)$
47		simpl	$⊢ (A \in V \land \exists x \in A \|x\| = +∞) \to A \in V$
48		hashf2	$⊢ \|.\| : V ⟶ [0, +∞]$
49		ffvelcdm	$⊢ (\|.\| : V ⟶ [0, +∞] \land x \in V) \to \|x\| \in [0, +∞]$
50	48 39 49	mp2an	$⊢ \|x\| \in [0, +∞]$
51	50	a1i	$⊢ ((A \in V \land \exists x \in A \|x\| = +∞) \land x \in A) \to \|x\| \in [0, +∞]$
52		simpr	$⊢ (A \in V \land \exists x \in A \|x\| = +∞) \to \exists x \in A \|x\| = +∞$
53	46 47 51 52	esumpinfval	$⊢ (A \in V \land \exists x \in A \|x\| = +∞) \to \underset{x \in A}{\sum^{*}} \|x\| = +∞$
54	43 53	sylan2	$⊢ (A \in V \land \neg A \subseteq Fin) \to \underset{x \in A}{\sum^{*}} \|x\| = +∞$
55	38 54	eqtr4d	$⊢ (A \in V \land \neg A \subseteq Fin) \to \|⋃ A\| = \underset{x \in A}{\sum^{*}} \|x\|$
56	55	3adant2	$⊢ (A \in V \land A \in Fin \land \neg A \subseteq Fin) \to \|⋃ A\| = \underset{x \in A}{\sum^{*}} \|x\|$
57	56	3adant1r	$⊢ ((A \in V \land \underset{x \in A}{Disj} x) \land A \in Fin \land \neg A \subseteq Fin) \to \|⋃ A\| = \underset{x \in A}{\sum^{*}} \|x\|$
58	57	3expa	$⊢ (((A \in V \land \underset{x \in A}{Disj} x) \land A \in Fin) \land \neg A \subseteq Fin) \to \|⋃ A\| = \underset{x \in A}{\sum^{*}} \|x\|$
59	25 58	pm2.61dan	$⊢ ((A \in V \land \underset{x \in A}{Disj} x) \land A \in Fin) \to \|⋃ A\| = \underset{x \in A}{\sum^{*}} \|x\|$
60		pwfi	$⊢ ⋃ A \in Fin \leftrightarrow 𝒫 ⋃ A \in Fin$
61		pwuni	$⊢ A \subseteq 𝒫 ⋃ A$
62		ssfi	$⊢ (𝒫 ⋃ A \in Fin \land A \subseteq 𝒫 ⋃ A) \to A \in Fin$
63	61 62	mpan2	$⊢ 𝒫 ⋃ A \in Fin \to A \in Fin$
64	60 63	sylbi	$⊢ ⋃ A \in Fin \to A \in Fin$
65	64	con3i	$⊢ \neg A \in Fin \to \neg ⋃ A \in Fin$
66	26 65 37	syl2an	$⊢ (A \in V \land \neg A \in Fin) \to \|⋃ A\| = +∞$
67		nftru	$⊢ Ⅎ x ⊤$
68		unrab	$⊢ \{x \in A \| \|x\| = 0\} \cup \{x \in A \| \neg \|x\| = 0\} = \{x \in A \| (\|x\| = 0 \lor \neg \|x\| = 0)\}$
69		exmid	$⊢ (\|x\| = 0 \lor \neg \|x\| = 0)$
70	69	rgenw	$⊢ \forall x \in A (\|x\| = 0 \lor \neg \|x\| = 0)$
71		rabid2	$⊢ A = \{x \in A \| (\|x\| = 0 \lor \neg \|x\| = 0)\} \leftrightarrow \forall x \in A (\|x\| = 0 \lor \neg \|x\| = 0)$
72	70 71	mpbir	$⊢ A = \{x \in A \| (\|x\| = 0 \lor \neg \|x\| = 0)\}$
73	68 72	eqtr4i	$⊢ \{x \in A \| \|x\| = 0\} \cup \{x \in A \| \neg \|x\| = 0\} = A$
74	73	a1i	$⊢ ⊤ \to \{x \in A \| \|x\| = 0\} \cup \{x \in A \| \neg \|x\| = 0\} = A$
75	67 74	esumeq1d	$⊢ ⊤ \to \underset{x \in \{x \in A \| \|x\| = 0\} \cup \{x \in A \| \neg \|x\| = 0\}}{\sum^{}} \|x\| = \underset{x \in A}{\sum^{}} \|x\|$
76	75	mptru	$⊢ \underset{x \in \{x \in A \| \|x\| = 0\} \cup \{x \in A \| \neg \|x\| = 0\}}{\sum^{}} \|x\| = \underset{x \in A}{\sum^{}} \|x\|$
77		nfrab1	$⊢ \underline{Ⅎ} x \{x \in A \| \|x\| = 0\}$
78		nfrab1	$⊢ \underline{Ⅎ} x \{x \in A \| \neg \|x\| = 0\}$
79		rabexg	$⊢ A \in V \to \{x \in A \| \|x\| = 0\} \in V$
80		rabexg	$⊢ A \in V \to \{x \in A \| \neg \|x\| = 0\} \in V$
81		rabnc	$⊢ \{x \in A \| \|x\| = 0\} \cap \{x \in A \| \neg \|x\| = 0\} = \emptyset$
82	81	a1i	$⊢ A \in V \to \{x \in A \| \|x\| = 0\} \cap \{x \in A \| \neg \|x\| = 0\} = \emptyset$
83	50	a1i	$⊢ (A \in V \land x \in \{x \in A \| \|x\| = 0\}) \to \|x\| \in [0, +∞]$
84	50	a1i	$⊢ (A \in V \land x \in \{x \in A \| \neg \|x\| = 0\}) \to \|x\| \in [0, +∞]$
85	44 77 78 79 80 82 83 84	esumsplit	$⊢ A \in V \to \underset{x \in \{x \in A \| \|x\| = 0\} \cup \{x \in A \| \neg \|x\| = 0\}}{\sum^{}} \|x\| = \underset{x \in \{x \in A \| \|x\| = 0\}}{\sum^{}} \|x\| +_{𝑒} \underset{x \in \{x \in A \| \neg \|x\| = 0\}}{\sum^{*}} \|x\|$
86	76 85	eqtr3id	$⊢ A \in V \to \underset{x \in A}{\sum^{}} \|x\| = \underset{x \in \{x \in A \| \|x\| = 0\}}{\sum^{}} \|x\| +_{𝑒} \underset{x \in \{x \in A \| \neg \|x\| = 0\}}{\sum^{*}} \|x\|$
87	86	adantr	$⊢ (A \in V \land \neg A \in Fin) \to \underset{x \in A}{\sum^{}} \|x\| = \underset{x \in \{x \in A \| \|x\| = 0\}}{\sum^{}} \|x\| +_{𝑒} \underset{x \in \{x \in A \| \neg \|x\| = 0\}}{\sum^{*}} \|x\|$
88		nfv	$⊢ Ⅎ x (A \in V \land \neg A \in Fin)$
89	80	adantr	$⊢ (A \in V \land \neg A \in Fin) \to \{x \in A \| \neg \|x\| = 0\} \in V$
90		simpr	$⊢ (A \in V \land \neg A \in Fin) \to \neg A \in Fin$
91		dfrab3	$⊢ \{x \in A \| \|x\| = 0\} = A \cap \{x \| \|x\| = 0\}$
92		hasheq0	$⊢ x \in V \to (\|x\| = 0 \leftrightarrow x = \emptyset)$
93	39 92	ax-mp	$⊢ \|x\| = 0 \leftrightarrow x = \emptyset$
94	93	abbii	$⊢ \{x \| \|x\| = 0\} = \{x \| x = \emptyset\}$
95		df-sn	$⊢ \{\emptyset\} = \{x \| x = \emptyset\}$
96	94 95	eqtr4i	$⊢ \{x \| \|x\| = 0\} = \{\emptyset\}$
97	96	ineq2i	$⊢ A \cap \{x \| \|x\| = 0\} = A \cap \{\emptyset\}$
98	91 97	eqtri	$⊢ \{x \in A \| \|x\| = 0\} = A \cap \{\emptyset\}$
99		snfi	$⊢ \{\emptyset\} \in Fin$
100		inss2	$⊢ A \cap \{\emptyset\} \subseteq \{\emptyset\}$
101		ssfi	$⊢ (\{\emptyset\} \in Fin \land A \cap \{\emptyset\} \subseteq \{\emptyset\}) \to A \cap \{\emptyset\} \in Fin$
102	99 100 101	mp2an	$⊢ A \cap \{\emptyset\} \in Fin$
103	98 102	eqeltri	$⊢ \{x \in A \| \|x\| = 0\} \in Fin$
104	103	a1i	$⊢ (A \in V \land \neg A \in Fin) \to \{x \in A \| \|x\| = 0\} \in Fin$
105		difinf	$⊢ (\neg A \in Fin \land \{x \in A \| \|x\| = 0\} \in Fin) \to \neg A ∖ \{x \in A \| \|x\| = 0\} \in Fin$
106	90 104 105	syl2anc	$⊢ (A \in V \land \neg A \in Fin) \to \neg A ∖ \{x \in A \| \|x\| = 0\} \in Fin$
107		notrab	$⊢ A ∖ \{x \in A \| \|x\| = 0\} = \{x \in A \| \neg \|x\| = 0\}$
108	107	eleq1i	$⊢ A ∖ \{x \in A \| \|x\| = 0\} \in Fin \leftrightarrow \{x \in A \| \neg \|x\| = 0\} \in Fin$
109	106 108	sylnib	$⊢ (A \in V \land \neg A \in Fin) \to \neg \{x \in A \| \neg \|x\| = 0\} \in Fin$
110	50	a1i	$⊢ ((A \in V \land \neg A \in Fin) \land x \in \{x \in A \| \neg \|x\| = 0\}) \to \|x\| \in [0, +∞]$
111	39	a1i	$⊢ ((A \in V \land \neg A \in Fin) \land x \in \{x \in A \| \neg \|x\| = 0\}) \to x \in V$
112		rabid	$⊢ x \in \{x \in A \| \neg \|x\| = 0\} \leftrightarrow (x \in A \land \neg \|x\| = 0)$
113	112	bilani	$⊢ ((A \in V \land \neg A \in Fin) \land x \in \{x \in A \| \neg \|x\| = 0\}) \to (x \in A \land \neg \|x\| = 0)$
114	113	simprd	$⊢ ((A \in V \land \neg A \in Fin) \land x \in \{x \in A \| \neg \|x\| = 0\}) \to \neg \|x\| = 0$
115	93	biimpri	$⊢ x = \emptyset \to \|x\| = 0$
116	115	necon3bi	$⊢ \neg \|x\| = 0 \to x \neq \emptyset$
117	114 116	syl	$⊢ ((A \in V \land \neg A \in Fin) \land x \in \{x \in A \| \neg \|x\| = 0\}) \to x \neq \emptyset$
118		hashge1	$⊢ (x \in V \land x \neq \emptyset) \to 1 \leq \|x\|$
119	111 117 118	syl2anc	$⊢ ((A \in V \land \neg A \in Fin) \land x \in \{x \in A \| \neg \|x\| = 0\}) \to 1 \leq \|x\|$
120		1xr	$⊢ 1 \in ℝ^{*}$
121	120	a1i	$⊢ (A \in V \land \neg A \in Fin) \to 1 \in ℝ^{*}$
122		0lt1	$⊢ 0 < 1$
123	122	a1i	$⊢ (A \in V \land \neg A \in Fin) \to 0 < 1$
124	88 78 89 109 110 119 121 123	esumpinfsum	$⊢ (A \in V \land \neg A \in Fin) \to \underset{x \in \{x \in A \| \neg \|x\| = 0\}}{\sum^{*}} \|x\| = +∞$
125	124	oveq2d	$⊢ (A \in V \land \neg A \in Fin) \to \underset{x \in \{x \in A \| \|x\| = 0\}}{\sum^{}} \|x\| +_{𝑒} \underset{x \in \{x \in A \| \neg \|x\| = 0\}}{\sum^{}} \|x\| = \underset{x \in \{x \in A \| \|x\| = 0\}}{\sum^{*}} \|x\| +_{𝑒} +∞$
126		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
127	79	adantr	$⊢ (A \in V \land \neg A \in Fin) \to \{x \in A \| \|x\| = 0\} \in V$
128	50	a1i	$⊢ ((A \in V \land \neg A \in Fin) \land x \in \{x \in A \| \|x\| = 0\}) \to \|x\| \in [0, +∞]$
129	128	ralrimiva	$⊢ (A \in V \land \neg A \in Fin) \to \forall x \in \{x \in A \| \|x\| = 0\} \|x\| \in [0, +∞]$
130	77	esumcl	$⊢ (\{x \in A \| \|x\| = 0\} \in V \land \forall x \in \{x \in A \| \|x\| = 0\} \|x\| \in [0, +∞]) \to \underset{x \in \{x \in A \| \|x\| = 0\}}{\sum^{*}} \|x\| \in [0, +∞]$
131	127 129 130	syl2anc	$⊢ (A \in V \land \neg A \in Fin) \to \underset{x \in \{x \in A \| \|x\| = 0\}}{\sum^{*}} \|x\| \in [0, +∞]$
132	126 131	sselid	$⊢ (A \in V \land \neg A \in Fin) \to \underset{x \in \{x \in A \| \|x\| = 0\}}{\sum^{}} \|x\| \in ℝ^{}$
133		xrge0neqmnf	$⊢ \underset{x \in \{x \in A \| \|x\| = 0\}}{\sum^{}} \|x\| \in [0, +∞] \to \underset{x \in \{x \in A \| \|x\| = 0\}}{\sum^{}} \|x\| \neq −∞$
134	131 133	syl	$⊢ (A \in V \land \neg A \in Fin) \to \underset{x \in \{x \in A \| \|x\| = 0\}}{\sum^{*}} \|x\| \neq −∞$
135		xaddpnf1	$⊢ (\underset{x \in \{x \in A \| \|x\| = 0\}}{\sum^{}} \|x\| \in ℝ^{} \land \underset{x \in \{x \in A \| \|x\| = 0\}}{\sum^{}} \|x\| \neq −∞) \to \underset{x \in \{x \in A \| \|x\| = 0\}}{\sum^{}} \|x\| +_{𝑒} +∞ = +∞$
136	132 134 135	syl2anc	$⊢ (A \in V \land \neg A \in Fin) \to \underset{x \in \{x \in A \| \|x\| = 0\}}{\sum^{*}} \|x\| +_{𝑒} +∞ = +∞$
137	87 125 136	3eqtrd	$⊢ (A \in V \land \neg A \in Fin) \to \underset{x \in A}{\sum^{*}} \|x\| = +∞$
138	66 137	eqtr4d	$⊢ (A \in V \land \neg A \in Fin) \to \|⋃ A\| = \underset{x \in A}{\sum^{*}} \|x\|$
139	138	adantlr	$⊢ ((A \in V \land \underset{x \in A}{Disj} x) \land \neg A \in Fin) \to \|⋃ A\| = \underset{x \in A}{\sum^{*}} \|x\|$
140	59 139	pm2.61dan	$⊢ (A \in V \land \underset{x \in A}{Disj} x) \to \|⋃ A\| = \underset{x \in A}{\sum^{*}} \|x\|$

Metamath Proof Explorer

Theorem hasheuni

Proof