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		vsnid	$⊢ x \in \{x\}$
27		opelxp	$⊢ ⟨x, y⟩ \in (\{x\} \times B) \leftrightarrow (x \in \{x\} \land y \in B)$
28	26 27	mpbiran	$⊢ ⟨x, y⟩ \in (\{x\} \times B) \leftrightarrow y \in B$
29	28	bilanri	$⊢ (x \in A \land y \in B) \to ⟨x, y⟩ \in (\{x\} \times B)$
30	25 29	sseldd	$⊢ (x \in A \land y \in B) \to ⟨x, y⟩ \in ⋃_{x \in A} (\{x\} \times B)$
31	30 1	eleqtrrdi	$⊢ (x \in A \land y \in B) \to ⟨x, y⟩ \in T$
32		vex	$⊢ x \in V$
33		vex	$⊢ y \in V$
34	32 33	op2nd	$⊢ 2^{nd} (⟨x, y⟩) = y$
35		fveqeq2	$⊢ z = ⟨x, y⟩ \to (2^{nd} (z) = y \leftrightarrow 2^{nd} (⟨x, y⟩) = y)$
36	35	rspcev	$⊢ (⟨x, y⟩ \in T \land 2^{nd} (⟨x, y⟩) = y) \to \exists z \in T 2^{nd} (z) = y$
37	31 34 36	sylancl	$⊢ (x \in A \land y \in B) \to \exists z \in T 2^{nd} (z) = y$
38	37	ex	$⊢ x \in A \to (y \in B \to \exists z \in T 2^{nd} (z) = y)$
39	23 38	rexlimi	$⊢ \exists x \in A y \in B \to \exists z \in T 2^{nd} (z) = y$
40	19 39	impbii	$⊢ \exists z \in T 2^{nd} (z) = y \leftrightarrow \exists x \in A y \in B$
41		fvelimab	$⊢ (2^{nd} Fn V \land T \subseteq V) \to (y \in 2^{nd} [T] \leftrightarrow \exists z \in T 2^{nd} (z) = y)$
42	5 6 41	mp2an	$⊢ y \in 2^{nd} [T] \leftrightarrow \exists z \in T 2^{nd} (z) = y$
43		eliun	$⊢ y \in ⋃_{x \in A} B \leftrightarrow \exists x \in A y \in B$
44	40 42 43	3bitr4i	$⊢ y \in 2^{nd} [T] \leftrightarrow y \in ⋃_{x \in A} B$
45	44	eqriv	$⊢ 2^{nd} [T] = ⋃_{x \in A} B$
46	9 45	eqtr3i	$⊢ ran ({2^{nd} ↾}_{T}) = ⋃_{x \in A} B$
47		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)$
48	8 46 47	mpbir2an	$⊢ ({2^{nd} ↾}_{T}) : T \underset{onto}{⟶} ⋃_{x \in A} B$

Metamath Proof Explorer

Theorem iunfo

Proof