Theorem 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	⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 )
Assertion	iunfo	⊢ ( 2nd ↾ 𝑇 ) : 𝑇 –onto→ ∪ 𝑥 ∈ 𝐴 𝐵

Proof

Step	Hyp	Ref	Expression
1		iunfo.1	⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 )
2		fo2nd	⊢ 2nd : V –onto→ V
3		fof	⊢ ( 2nd : V –onto→ V → 2nd : V ⟶ V )
4		ffn	⊢ ( 2nd : V ⟶ V → 2nd Fn V )
5	2 3 4	mp2b	⊢ 2nd Fn V
6		ssv	⊢ 𝑇 ⊆ V
7		fnssres	⊢ ( ( 2nd Fn V ∧ 𝑇 ⊆ V ) → ( 2nd ↾ 𝑇 ) Fn 𝑇 )
8	5 6 7	mp2an	⊢ ( 2nd ↾ 𝑇 ) Fn 𝑇
9		df-ima	⊢ ( 2nd “ 𝑇 ) = ran ( 2nd ↾ 𝑇 )
10	1	eleq2i	⊢ ( 𝑧 ∈ 𝑇 ↔ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) )
11		eliun	⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ ( { 𝑥 } × 𝐵 ) )
12	10 11	bitri	⊢ ( 𝑧 ∈ 𝑇 ↔ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ ( { 𝑥 } × 𝐵 ) )
13		xp2nd	⊢ ( 𝑧 ∈ ( { 𝑥 } × 𝐵 ) → ( 2nd ‘ 𝑧 ) ∈ 𝐵 )
14		eleq1	⊢ ( ( 2nd ‘ 𝑧 ) = 𝑦 → ( ( 2nd ‘ 𝑧 ) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) )
15	13 14	syl5ib	⊢ ( ( 2nd ‘ 𝑧 ) = 𝑦 → ( 𝑧 ∈ ( { 𝑥 } × 𝐵 ) → 𝑦 ∈ 𝐵 ) )
16	15	reximdv	⊢ ( ( 2nd ‘ 𝑧 ) = 𝑦 → ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ ( { 𝑥 } × 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) )
17	12 16	syl5bi	⊢ ( ( 2nd ‘ 𝑧 ) = 𝑦 → ( 𝑧 ∈ 𝑇 → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) )
18	17	impcom	⊢ ( ( 𝑧 ∈ 𝑇 ∧ ( 2nd ‘ 𝑧 ) = 𝑦 ) → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
19	18	rexlimiva	⊢ ( ∃ 𝑧 ∈ 𝑇 ( 2nd ‘ 𝑧 ) = 𝑦 → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
20		nfiu1	⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 )
21	1 20	nfcxfr	⊢ Ⅎ 𝑥 𝑇
22		nfv	⊢ Ⅎ 𝑥 ( 2nd ‘ 𝑧 ) = 𝑦
23	21 22	nfrex	⊢ Ⅎ 𝑥 ∃ 𝑧 ∈ 𝑇 ( 2nd ‘ 𝑧 ) = 𝑦
24		ssiun2	⊢ ( 𝑥 ∈ 𝐴 → ( { 𝑥 } × 𝐵 ) ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) )
25	24	adantr	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( { 𝑥 } × 𝐵 ) ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) )
26		simpr	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
27		vsnid	⊢ 𝑥 ∈ { 𝑥 }
28		opelxp	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑥 } × 𝐵 ) ↔ ( 𝑥 ∈ { 𝑥 } ∧ 𝑦 ∈ 𝐵 ) )
29	27 28	mpbiran	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑥 } × 𝐵 ) ↔ 𝑦 ∈ 𝐵 )
30	26 29	sylibr	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑥 } × 𝐵 ) )
31	25 30	sseldd	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) )
32	31 1	eleqtrrdi	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑇 )
33		vex	⊢ 𝑥 ∈ V
34		vex	⊢ 𝑦 ∈ V
35	33 34	op2nd	⊢ ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑦
36		fveqeq2	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 2nd ‘ 𝑧 ) = 𝑦 ↔ ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑦 ) )
37	36	rspcev	⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑇 ∧ ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑦 ) → ∃ 𝑧 ∈ 𝑇 ( 2nd ‘ 𝑧 ) = 𝑦 )
38	32 35 37	sylancl	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑧 ∈ 𝑇 ( 2nd ‘ 𝑧 ) = 𝑦 )
39	38	ex	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → ∃ 𝑧 ∈ 𝑇 ( 2nd ‘ 𝑧 ) = 𝑦 ) )
40	23 39	rexlimi	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃ 𝑧 ∈ 𝑇 ( 2nd ‘ 𝑧 ) = 𝑦 )
41	19 40	impbii	⊢ ( ∃ 𝑧 ∈ 𝑇 ( 2nd ‘ 𝑧 ) = 𝑦 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
42		fvelimab	⊢ ( ( 2nd Fn V ∧ 𝑇 ⊆ V ) → ( 𝑦 ∈ ( 2nd “ 𝑇 ) ↔ ∃ 𝑧 ∈ 𝑇 ( 2nd ‘ 𝑧 ) = 𝑦 ) )
43	5 6 42	mp2an	⊢ ( 𝑦 ∈ ( 2nd “ 𝑇 ) ↔ ∃ 𝑧 ∈ 𝑇 ( 2nd ‘ 𝑧 ) = 𝑦 )
44		eliun	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
45	41 43 44	3bitr4i	⊢ ( 𝑦 ∈ ( 2nd “ 𝑇 ) ↔ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
46	45	eqriv	⊢ ( 2nd “ 𝑇 ) = ∪ 𝑥 ∈ 𝐴 𝐵
47	9 46	eqtr3i	⊢ ran ( 2nd ↾ 𝑇 ) = ∪ 𝑥 ∈ 𝐴 𝐵
48		df-fo	⊢ ( ( 2nd ↾ 𝑇 ) : 𝑇 –onto→ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ( ( 2nd ↾ 𝑇 ) Fn 𝑇 ∧ ran ( 2nd ↾ 𝑇 ) = ∪ 𝑥 ∈ 𝐴 𝐵 ) )
49	8 47 48	mpbir2an	⊢ ( 2nd ↾ 𝑇 ) : 𝑇 –onto→ ∪ 𝑥 ∈ 𝐴 𝐵