ixpiunwdom

Description: Describe an onto function from the indexed cartesian product to the indexed union. Together with ixpssmapg this shows that U_ x e. A B and X_ x e. A B have closely linked cardinalities. (Contributed by Mario Carneiro, 27-Aug-2015)

		Ref	Expression
	Assertion	ixpiunwdom	$⊢ (A \in V \land ⋃_{x \in A} B \in W \land \underset{x \in A}{⨉} B \neq \emptyset) \to ⋃_{x \in A} B ≼^{*} (\underset{x \in A}{⨉} B \times A)$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ f \in V$
2	1	elixp	$⊢ f \in \underset{x \in A}{⨉} B \leftrightarrow (f Fn A \land \forall x \in A f (x) \in B)$
3	2	simprbi	$⊢ f \in \underset{x \in A}{⨉} B \to \forall x \in A f (x) \in B$
4		ssiun2	$⊢ x \in A \to B \subseteq ⋃_{x \in A} B$
5	4	sseld	$⊢ x \in A \to (f (x) \in B \to f (x) \in ⋃_{x \in A} B)$
6	5	ralimia	$⊢ \forall x \in A f (x) \in B \to \forall x \in A f (x) \in ⋃_{x \in A} B$
7	3 6	syl	$⊢ f \in \underset{x \in A}{⨉} B \to \forall x \in A f (x) \in ⋃_{x \in A} B$
8		nfv	$⊢ Ⅎ y f (x) \in ⋃_{x \in A} B$
9		nfiu1	$⊢ \underline{Ⅎ} x ⋃_{x \in A} B$
10	9	nfel2	$⊢ Ⅎ x f (y) \in ⋃_{x \in A} B$
11		fveq2	$⊢ x = y \to f (x) = f (y)$
12	11	eleq1d	$⊢ x = y \to (f (x) \in ⋃_{x \in A} B \leftrightarrow f (y) \in ⋃_{x \in A} B)$
13	8 10 12	cbvralw	$⊢ \forall x \in A f (x) \in ⋃_{x \in A} B \leftrightarrow \forall y \in A f (y) \in ⋃_{x \in A} B$
14	7 13	sylib	$⊢ f \in \underset{x \in A}{⨉} B \to \forall y \in A f (y) \in ⋃_{x \in A} B$
15	14	adantl	$⊢ ((A \in V \land ⋃_{x \in A} B \in W \land \underset{x \in A}{⨉} B \neq \emptyset) \land f \in \underset{x \in A}{⨉} B) \to \forall y \in A f (y) \in ⋃_{x \in A} B$
16	15	ralrimiva	$⊢ (A \in V \land ⋃_{x \in A} B \in W \land \underset{x \in A}{⨉} B \neq \emptyset) \to \forall f \in \underset{x \in A}{⨉} B \forall y \in A f (y) \in ⋃_{x \in A} B$
17		eqid	$⊢ (f \in \underset{x \in A}{⨉} B, y \in A ⟼ f (y)) = (f \in \underset{x \in A}{⨉} B, y \in A ⟼ f (y))$
18	17	fmpo	$⊢ \forall f \in \underset{x \in A}{⨉} B \forall y \in A f (y) \in ⋃_{x \in A} B \leftrightarrow (f \in \underset{x \in A}{⨉} B, y \in A ⟼ f (y)) : \underset{x \in A}{⨉} B \times A ⟶ ⋃_{x \in A} B$
19	16 18	sylib	$⊢ (A \in V \land ⋃_{x \in A} B \in W \land \underset{x \in A}{⨉} B \neq \emptyset) \to (f \in \underset{x \in A}{⨉} B, y \in A ⟼ f (y)) : \underset{x \in A}{⨉} B \times A ⟶ ⋃_{x \in A} B$
20		ixpssmap2g	$⊢ ⋃_{x \in A} B \in W \to \underset{x \in A}{⨉} B \subseteq {⋃_{x \in A} B}^{A}$
21	20	3ad2ant2	$⊢ (A \in V \land ⋃_{x \in A} B \in W \land \underset{x \in A}{⨉} B \neq \emptyset) \to \underset{x \in A}{⨉} B \subseteq {⋃_{x \in A} B}^{A}$
22		ovex	$⊢ {⋃_{x \in A} B}^{A} \in V$
23	22	ssex	$⊢ \underset{x \in A}{⨉} B \subseteq {⋃_{x \in A} B}^{A} \to \underset{x \in A}{⨉} B \in V$
24	21 23	syl	$⊢ (A \in V \land ⋃_{x \in A} B \in W \land \underset{x \in A}{⨉} B \neq \emptyset) \to \underset{x \in A}{⨉} B \in V$
25		simp1	$⊢ (A \in V \land ⋃_{x \in A} B \in W \land \underset{x \in A}{⨉} B \neq \emptyset) \to A \in V$
26	24 25	xpexd	$⊢ (A \in V \land ⋃_{x \in A} B \in W \land \underset{x \in A}{⨉} B \neq \emptyset) \to \underset{x \in A}{⨉} B \times A \in V$
27	19 26	fexd	$⊢ (A \in V \land ⋃_{x \in A} B \in W \land \underset{x \in A}{⨉} B \neq \emptyset) \to (f \in \underset{x \in A}{⨉} B, y \in A ⟼ f (y)) \in V$
28	19	ffnd	$⊢ (A \in V \land ⋃_{x \in A} B \in W \land \underset{x \in A}{⨉} B \neq \emptyset) \to (f \in \underset{x \in A}{⨉} B, y \in A ⟼ f (y)) Fn (\underset{x \in A}{⨉} B \times A)$
29		dffn4	$⊢ (f \in \underset{x \in A}{⨉} B, y \in A ⟼ f (y)) Fn (\underset{x \in A}{⨉} B \times A) \leftrightarrow (f \in \underset{x \in A}{⨉} B, y \in A ⟼ f (y)) : \underset{x \in A}{⨉} B \times A \underset{onto}{⟶} ran (f \in \underset{x \in A}{⨉} B, y \in A ⟼ f (y))$
30	28 29	sylib	$⊢ (A \in V \land ⋃_{x \in A} B \in W \land \underset{x \in A}{⨉} B \neq \emptyset) \to (f \in \underset{x \in A}{⨉} B, y \in A ⟼ f (y)) : \underset{x \in A}{⨉} B \times A \underset{onto}{⟶} ran (f \in \underset{x \in A}{⨉} B, y \in A ⟼ f (y))$
31		n0	$⊢ \underset{x \in A}{⨉} B \neq \emptyset \leftrightarrow \exists g g \in \underset{x \in A}{⨉} B$
32		eliun	$⊢ z \in ⋃_{x \in A} B \leftrightarrow \exists x \in A z \in B$
33		nfixp1	$⊢ \underline{Ⅎ} x \underset{x \in A}{⨉} B$
34	33	nfel2	$⊢ Ⅎ x g \in \underset{x \in A}{⨉} B$
35		nfv	$⊢ Ⅎ x \exists y \in A z = f (y)$
36	33 35	nfrex	$⊢ Ⅎ x \exists f \in \underset{x \in A}{⨉} B \exists y \in A z = f (y)$
37		simplrr	$⊢ ((g \in \underset{x \in A}{⨉} B \land (x \in A \land z \in B)) \land k \in A) \to z \in B$
38		iftrue	$⊢ k = x \to if (k = x, z, g (k)) = z$
39		csbeq1a	$⊢ x = k \to B = ⦋ k / x ⦌ B$
40	39	equcoms	$⊢ k = x \to B = ⦋ k / x ⦌ B$
41	40	eqcomd	$⊢ k = x \to ⦋ k / x ⦌ B = B$
42	38 41	eleq12d	$⊢ k = x \to (if (k = x, z, g (k)) \in ⦋ k / x ⦌ B \leftrightarrow z \in B)$
43	37 42	syl5ibrcom	$⊢ ((g \in \underset{x \in A}{⨉} B \land (x \in A \land z \in B)) \land k \in A) \to (k = x \to if (k = x, z, g (k)) \in ⦋ k / x ⦌ B)$
44		vex	$⊢ g \in V$
45	44	elixp	$⊢ g \in \underset{x \in A}{⨉} B \leftrightarrow (g Fn A \land \forall x \in A g (x) \in B)$
46	45	simprbi	$⊢ g \in \underset{x \in A}{⨉} B \to \forall x \in A g (x) \in B$
47	46	adantr	$⊢ (g \in \underset{x \in A}{⨉} B \land (x \in A \land z \in B)) \to \forall x \in A g (x) \in B$
48		nfv	$⊢ Ⅎ k g (x) \in B$
49		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ k / x ⦌ B$
50	49	nfel2	$⊢ Ⅎ x g (k) \in ⦋ k / x ⦌ B$
51		fveq2	$⊢ x = k \to g (x) = g (k)$
52	51 39	eleq12d	$⊢ x = k \to (g (x) \in B \leftrightarrow g (k) \in ⦋ k / x ⦌ B)$
53	48 50 52	cbvralw	$⊢ \forall x \in A g (x) \in B \leftrightarrow \forall k \in A g (k) \in ⦋ k / x ⦌ B$
54	47 53	sylib	$⊢ (g \in \underset{x \in A}{⨉} B \land (x \in A \land z \in B)) \to \forall k \in A g (k) \in ⦋ k / x ⦌ B$
55	54	r19.21bi	$⊢ ((g \in \underset{x \in A}{⨉} B \land (x \in A \land z \in B)) \land k \in A) \to g (k) \in ⦋ k / x ⦌ B$
56		iffalse	$⊢ \neg k = x \to if (k = x, z, g (k)) = g (k)$
57	56	eleq1d	$⊢ \neg k = x \to (if (k = x, z, g (k)) \in ⦋ k / x ⦌ B \leftrightarrow g (k) \in ⦋ k / x ⦌ B)$
58	55 57	syl5ibrcom	$⊢ ((g \in \underset{x \in A}{⨉} B \land (x \in A \land z \in B)) \land k \in A) \to (\neg k = x \to if (k = x, z, g (k)) \in ⦋ k / x ⦌ B)$
59	43 58	pm2.61d	$⊢ ((g \in \underset{x \in A}{⨉} B \land (x \in A \land z \in B)) \land k \in A) \to if (k = x, z, g (k)) \in ⦋ k / x ⦌ B$
60	59	ralrimiva	$⊢ (g \in \underset{x \in A}{⨉} B \land (x \in A \land z \in B)) \to \forall k \in A if (k = x, z, g (k)) \in ⦋ k / x ⦌ B$
61		ixpfn	$⊢ g \in \underset{x \in A}{⨉} B \to g Fn A$
62	61	adantr	$⊢ (g \in \underset{x \in A}{⨉} B \land (x \in A \land z \in B)) \to g Fn A$
63	62	fndmd	$⊢ (g \in \underset{x \in A}{⨉} B \land (x \in A \land z \in B)) \to dom g = A$
64	44	dmex	$⊢ dom g \in V$
65	63 64	eqeltrrdi	$⊢ (g \in \underset{x \in A}{⨉} B \land (x \in A \land z \in B)) \to A \in V$
66		mptelixpg	$⊢ A \in V \to ((k \in A ⟼ if (k = x, z, g (k))) \in \underset{k \in A}{⨉} ⦋ k / x ⦌ B \leftrightarrow \forall k \in A if (k = x, z, g (k)) \in ⦋ k / x ⦌ B)$
67	65 66	syl	$⊢ (g \in \underset{x \in A}{⨉} B \land (x \in A \land z \in B)) \to ((k \in A ⟼ if (k = x, z, g (k))) \in \underset{k \in A}{⨉} ⦋ k / x ⦌ B \leftrightarrow \forall k \in A if (k = x, z, g (k)) \in ⦋ k / x ⦌ B)$
68	60 67	mpbird	$⊢ (g \in \underset{x \in A}{⨉} B \land (x \in A \land z \in B)) \to (k \in A ⟼ if (k = x, z, g (k))) \in \underset{k \in A}{⨉} ⦋ k / x ⦌ B$
69		nfcv	$⊢ \underline{Ⅎ} k B$
70	69 49 39	cbvixp	$⊢ \underset{x \in A}{⨉} B = \underset{k \in A}{⨉} ⦋ k / x ⦌ B$
71	68 70	eleqtrrdi	$⊢ (g \in \underset{x \in A}{⨉} B \land (x \in A \land z \in B)) \to (k \in A ⟼ if (k = x, z, g (k))) \in \underset{x \in A}{⨉} B$
72		simprl	$⊢ (g \in \underset{x \in A}{⨉} B \land (x \in A \land z \in B)) \to x \in A$
73		eqid	$⊢ (k \in A ⟼ if (k = x, z, g (k))) = (k \in A ⟼ if (k = x, z, g (k)))$
74		vex	$⊢ z \in V$
75	38 73 74	fvmpt	$⊢ x \in A \to (k \in A ⟼ if (k = x, z, g (k))) (x) = z$
76	75	ad2antrl	$⊢ (g \in \underset{x \in A}{⨉} B \land (x \in A \land z \in B)) \to (k \in A ⟼ if (k = x, z, g (k))) (x) = z$
77	76	eqcomd	$⊢ (g \in \underset{x \in A}{⨉} B \land (x \in A \land z \in B)) \to z = (k \in A ⟼ if (k = x, z, g (k))) (x)$
78		fveq1	$⊢ f = (k \in A ⟼ if (k = x, z, g (k))) \to f (y) = (k \in A ⟼ if (k = x, z, g (k))) (y)$
79	78	eqeq2d	$⊢ f = (k \in A ⟼ if (k = x, z, g (k))) \to (z = f (y) \leftrightarrow z = (k \in A ⟼ if (k = x, z, g (k))) (y))$
80		fveq2	$⊢ y = x \to (k \in A ⟼ if (k = x, z, g (k))) (y) = (k \in A ⟼ if (k = x, z, g (k))) (x)$
81	80	eqeq2d	$⊢ y = x \to (z = (k \in A ⟼ if (k = x, z, g (k))) (y) \leftrightarrow z = (k \in A ⟼ if (k = x, z, g (k))) (x))$
82	79 81	rspc2ev	$⊢ ((k \in A ⟼ if (k = x, z, g (k))) \in \underset{x \in A}{⨉} B \land x \in A \land z = (k \in A ⟼ if (k = x, z, g (k))) (x)) \to \exists f \in \underset{x \in A}{⨉} B \exists y \in A z = f (y)$
83	71 72 77 82	syl3anc	$⊢ (g \in \underset{x \in A}{⨉} B \land (x \in A \land z \in B)) \to \exists f \in \underset{x \in A}{⨉} B \exists y \in A z = f (y)$
84	83	exp32	$⊢ g \in \underset{x \in A}{⨉} B \to (x \in A \to (z \in B \to \exists f \in \underset{x \in A}{⨉} B \exists y \in A z = f (y)))$
85	34 36 84	rexlimd	$⊢ g \in \underset{x \in A}{⨉} B \to (\exists x \in A z \in B \to \exists f \in \underset{x \in A}{⨉} B \exists y \in A z = f (y))$
86	32 85	syl5bi	$⊢ g \in \underset{x \in A}{⨉} B \to (z \in ⋃_{x \in A} B \to \exists f \in \underset{x \in A}{⨉} B \exists y \in A z = f (y))$
87	86	exlimiv	$⊢ \exists g g \in \underset{x \in A}{⨉} B \to (z \in ⋃_{x \in A} B \to \exists f \in \underset{x \in A}{⨉} B \exists y \in A z = f (y))$
88	31 87	sylbi	$⊢ \underset{x \in A}{⨉} B \neq \emptyset \to (z \in ⋃_{x \in A} B \to \exists f \in \underset{x \in A}{⨉} B \exists y \in A z = f (y))$
89	88	3ad2ant3	$⊢ (A \in V \land ⋃_{x \in A} B \in W \land \underset{x \in A}{⨉} B \neq \emptyset) \to (z \in ⋃_{x \in A} B \to \exists f \in \underset{x \in A}{⨉} B \exists y \in A z = f (y))$
90	89	alrimiv	$⊢ (A \in V \land ⋃_{x \in A} B \in W \land \underset{x \in A}{⨉} B \neq \emptyset) \to \forall z (z \in ⋃_{x \in A} B \to \exists f \in \underset{x \in A}{⨉} B \exists y \in A z = f (y))$
91		ssab	$⊢ ⋃_{x \in A} B \subseteq \{z \| \exists f \in \underset{x \in A}{⨉} B \exists y \in A z = f (y)\} \leftrightarrow \forall z (z \in ⋃_{x \in A} B \to \exists f \in \underset{x \in A}{⨉} B \exists y \in A z = f (y))$
92	90 91	sylibr	$⊢ (A \in V \land ⋃_{x \in A} B \in W \land \underset{x \in A}{⨉} B \neq \emptyset) \to ⋃_{x \in A} B \subseteq \{z \| \exists f \in \underset{x \in A}{⨉} B \exists y \in A z = f (y)\}$
93	17	rnmpo	$⊢ ran (f \in \underset{x \in A}{⨉} B, y \in A ⟼ f (y)) = \{z \| \exists f \in \underset{x \in A}{⨉} B \exists y \in A z = f (y)\}$
94	92 93	sseqtrrdi	$⊢ (A \in V \land ⋃_{x \in A} B \in W \land \underset{x \in A}{⨉} B \neq \emptyset) \to ⋃_{x \in A} B \subseteq ran (f \in \underset{x \in A}{⨉} B, y \in A ⟼ f (y))$
95	19	frnd	$⊢ (A \in V \land ⋃_{x \in A} B \in W \land \underset{x \in A}{⨉} B \neq \emptyset) \to ran (f \in \underset{x \in A}{⨉} B, y \in A ⟼ f (y)) \subseteq ⋃_{x \in A} B$
96	94 95	eqssd	$⊢ (A \in V \land ⋃_{x \in A} B \in W \land \underset{x \in A}{⨉} B \neq \emptyset) \to ⋃_{x \in A} B = ran (f \in \underset{x \in A}{⨉} B, y \in A ⟼ f (y))$
97		foeq3	$⊢ ⋃_{x \in A} B = ran (f \in \underset{x \in A}{⨉} B, y \in A ⟼ f (y)) \to ((f \in \underset{x \in A}{⨉} B, y \in A ⟼ f (y)) : \underset{x \in A}{⨉} B \times A \underset{onto}{⟶} ⋃_{x \in A} B \leftrightarrow (f \in \underset{x \in A}{⨉} B, y \in A ⟼ f (y)) : \underset{x \in A}{⨉} B \times A \underset{onto}{⟶} ran (f \in \underset{x \in A}{⨉} B, y \in A ⟼ f (y)))$
98	96 97	syl	$⊢ (A \in V \land ⋃_{x \in A} B \in W \land \underset{x \in A}{⨉} B \neq \emptyset) \to ((f \in \underset{x \in A}{⨉} B, y \in A ⟼ f (y)) : \underset{x \in A}{⨉} B \times A \underset{onto}{⟶} ⋃_{x \in A} B \leftrightarrow (f \in \underset{x \in A}{⨉} B, y \in A ⟼ f (y)) : \underset{x \in A}{⨉} B \times A \underset{onto}{⟶} ran (f \in \underset{x \in A}{⨉} B, y \in A ⟼ f (y)))$
99	30 98	mpbird	$⊢ (A \in V \land ⋃_{x \in A} B \in W \land \underset{x \in A}{⨉} B \neq \emptyset) \to (f \in \underset{x \in A}{⨉} B, y \in A ⟼ f (y)) : \underset{x \in A}{⨉} B \times A \underset{onto}{⟶} ⋃_{x \in A} B$
100		fowdom	$⊢ ((f \in \underset{x \in A}{⨉} B, y \in A ⟼ f (y)) \in V \land (f \in \underset{x \in A}{⨉} B, y \in A ⟼ f (y)) : \underset{x \in A}{⨉} B \times A \underset{onto}{⟶} ⋃_{x \in A} B) \to ⋃_{x \in A} B ≼^{*} (\underset{x \in A}{⨉} B \times A)$
101	27 99 100	syl2anc	$⊢ (A \in V \land ⋃_{x \in A} B \in W \land \underset{x \in A}{⨉} B \neq \emptyset) \to ⋃_{x \in A} B ≼^{*} (\underset{x \in A}{⨉} B \times A)$

Metamath Proof Explorer

Theorem ixpiunwdom

Proof