iunfo

Description: Existence of an onto function from a disjoint union to a union. (Contributed by Mario Carneiro, 24-Jun-2013) (Revised by Mario Carneiro, 18-Jan-2014)

		Ref	Expression
	Hypothesis	iunfo.1	$⊢ T = ⋃_{x \in A} (\{x\} \times B)$
	Assertion	iunfo	$⊢ ({2^{nd} ↾}_{T}) : T \underset{onto}{⟶} ⋃_{x \in A} B$

Proof

Step	Hyp	Ref	Expression
1		iunfo.1	$⊢ T = ⋃_{x \in A} (\{x\} \times B)$
2		fo2nd	$⊢ 2^{nd} : V \underset{onto}{⟶} V$
3		fof	$⊢ 2^{nd} : V \underset{onto}{⟶} V \to 2^{nd} : V ⟶ V$
4		ffn	$⊢ 2^{nd} : V ⟶ V \to 2^{nd} Fn V$
5	2 3 4	mp2b	$⊢ 2^{nd} Fn V$
6		ssv	$⊢ T \subseteq V$
7		fnssres	$⊢ (2^{nd} Fn V \land T \subseteq V) \to ({2^{nd} ↾}_{T}) Fn T$
8	5 6 7	mp2an	$⊢ ({2^{nd} ↾}_{T}) Fn T$
9		df-ima	$⊢ 2^{nd} [T] = ran ({2^{nd} ↾}_{T})$
10	1	eleq2i	$⊢ z \in T \leftrightarrow z \in ⋃_{x \in A} (\{x\} \times B)$
11		eliun	$⊢ z \in ⋃_{x \in A} (\{x\} \times B) \leftrightarrow \exists x \in A z \in (\{x\} \times B)$
12	10 11	bitri	$⊢ z \in T \leftrightarrow \exists x \in A z \in (\{x\} \times B)$
13		xp2nd	$⊢ z \in (\{x\} \times B) \to 2^{nd} (z) \in B$
14		eleq1	$⊢ 2^{nd} (z) = y \to (2^{nd} (z) \in B \leftrightarrow y \in B)$
15	13 14	imbitrid	$⊢ 2^{nd} (z) = y \to (z \in (\{x\} \times B) \to y \in B)$
16	15	reximdv	$⊢ 2^{nd} (z) = y \to (\exists x \in A z \in (\{x\} \times B) \to \exists x \in A y \in B)$
17	12 16	biimtrid	$⊢ 2^{nd} (z) = y \to (z \in T \to \exists x \in A y \in B)$
18	17	impcom	$⊢ (z \in T \land 2^{nd} (z) = y) \to \exists x \in A y \in B$
19	18	rexlimiva	$⊢ \exists z \in T 2^{nd} (z) = y \to \exists x \in A y \in B$
20		nfiu1	$⊢ \underline{Ⅎ} x ⋃_{x \in A} (\{x\} \times B)$
21	1 20	nfcxfr	$⊢ \underline{Ⅎ} x T$
22		nfv	$⊢ Ⅎ x 2^{nd} (z) = y$
23	21 22	nfrexw	$⊢ Ⅎ x \exists z \in T 2^{nd} (z) = y$
24		ssiun2	$⊢ x \in A \to \{x\} \times B \subseteq ⋃_{x \in A} (\{x\} \times B)$
25	24	adantr	$⊢ (x \in A \land y \in B) \to \{x\} \times B \subseteq ⋃_{x \in A} (\{x\} \times B)$
26		simpr	$⊢ (x \in A \land y \in B) \to y \in B$
27		vsnid	$⊢ x \in \{x\}$
28		opelxp	$⊢ ⟨x, y⟩ \in (\{x\} \times B) \leftrightarrow (x \in \{x\} \land y \in B)$
29	27 28	mpbiran	$⊢ ⟨x, y⟩ \in (\{x\} \times B) \leftrightarrow y \in B$
30	26 29	sylibr	$⊢ (x \in A \land y \in B) \to ⟨x, y⟩ \in (\{x\} \times B)$
31	25 30	sseldd	$⊢ (x \in A \land y \in B) \to ⟨x, y⟩ \in ⋃_{x \in A} (\{x\} \times B)$
32	31 1	eleqtrrdi	$⊢ (x \in A \land y \in B) \to ⟨x, y⟩ \in T$
33		vex	$⊢ x \in V$
34		vex	$⊢ y \in V$
35	33 34	op2nd	$⊢ 2^{nd} (⟨x, y⟩) = y$
36		fveqeq2	$⊢ z = ⟨x, y⟩ \to (2^{nd} (z) = y \leftrightarrow 2^{nd} (⟨x, y⟩) = y)$
37	36	rspcev	$⊢ (⟨x, y⟩ \in T \land 2^{nd} (⟨x, y⟩) = y) \to \exists z \in T 2^{nd} (z) = y$
38	32 35 37	sylancl	$⊢ (x \in A \land y \in B) \to \exists z \in T 2^{nd} (z) = y$
39	38	ex	$⊢ x \in A \to (y \in B \to \exists z \in T 2^{nd} (z) = y)$
40	23 39	rexlimi	$⊢ \exists x \in A y \in B \to \exists z \in T 2^{nd} (z) = y$
41	19 40	impbii	$⊢ \exists z \in T 2^{nd} (z) = y \leftrightarrow \exists x \in A y \in B$
42		fvelimab	$⊢ (2^{nd} Fn V \land T \subseteq V) \to (y \in 2^{nd} [T] \leftrightarrow \exists z \in T 2^{nd} (z) = y)$
43	5 6 42	mp2an	$⊢ y \in 2^{nd} [T] \leftrightarrow \exists z \in T 2^{nd} (z) = y$
44		eliun	$⊢ y \in ⋃_{x \in A} B \leftrightarrow \exists x \in A y \in B$
45	41 43 44	3bitr4i	$⊢ y \in 2^{nd} [T] \leftrightarrow y \in ⋃_{x \in A} B$
46	45	eqriv	$⊢ 2^{nd} [T] = ⋃_{x \in A} B$
47	9 46	eqtr3i	$⊢ ran ({2^{nd} ↾}_{T}) = ⋃_{x \in A} B$
48		df-fo	$⊢ ({2^{nd} ↾}_{T}) : T \underset{onto}{⟶} ⋃_{x \in A} B \leftrightarrow (({2^{nd} ↾}_{T}) Fn T \land ran ({2^{nd} ↾}_{T}) = ⋃_{x \in A} B)$
49	8 47 48	mpbir2an	$⊢ ({2^{nd} ↾}_{T}) : T \underset{onto}{⟶} ⋃_{x \in A} B$

Metamath Proof Explorer

Theorem iunfo

Proof