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	imbitrid	⊢ ( ( 2nd ‘ 𝑧 ) = 𝑦 → ( 𝑧 ∈ ( { 𝑥 } × 𝐵 ) → 𝑦 ∈ 𝐵 ) )
16	15	reximdv	⊢ ( ( 2nd ‘ 𝑧 ) = 𝑦 → ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ ( { 𝑥 } × 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) )
17	12 16	biimtrid	⊢ ( ( 2nd ‘ 𝑧 ) = 𝑦 → ( 𝑧 ∈ 𝑇 → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) )
18	17	impcom	⊢ ( ( 𝑧 ∈ 𝑇 ∧ ( 2nd ‘ 𝑧 ) = 𝑦 ) → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
19	18	rexlimiva	⊢ ( ∃ 𝑧 ∈ 𝑇 ( 2nd ‘ 𝑧 ) = 𝑦 → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
20		nfiu1	⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 )
21	1 20	nfcxfr	⊢ Ⅎ 𝑥 𝑇
22		nfv	⊢ Ⅎ 𝑥 ( 2nd ‘ 𝑧 ) = 𝑦
23	21 22	nfrexw	⊢ Ⅎ 𝑥 ∃ 𝑧 ∈ 𝑇 ( 2nd ‘ 𝑧 ) = 𝑦
24		ssiun2	⊢ ( 𝑥 ∈ 𝐴 → ( { 𝑥 } × 𝐵 ) ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) )
25	24	adantr	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( { 𝑥 } × 𝐵 ) ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) )
26		vsnid	⊢ 𝑥 ∈ { 𝑥 }
27		opelxp	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑥 } × 𝐵 ) ↔ ( 𝑥 ∈ { 𝑥 } ∧ 𝑦 ∈ 𝐵 ) )
28	26 27	mpbiran	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑥 } × 𝐵 ) ↔ 𝑦 ∈ 𝐵 )
29	28	bilanri	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( { 𝑥 } × 𝐵 ) )
30	25 29	sseldd	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) )
31	30 1	eleqtrrdi	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑇 )
32		vex	⊢ 𝑥 ∈ V
33		vex	⊢ 𝑦 ∈ V
34	32 33	op2nd	⊢ ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑦
35		fveqeq2	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 2nd ‘ 𝑧 ) = 𝑦 ↔ ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑦 ) )
36	35	rspcev	⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑇 ∧ ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑦 ) → ∃ 𝑧 ∈ 𝑇 ( 2nd ‘ 𝑧 ) = 𝑦 )
37	31 34 36	sylancl	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑧 ∈ 𝑇 ( 2nd ‘ 𝑧 ) = 𝑦 )
38	37	ex	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → ∃ 𝑧 ∈ 𝑇 ( 2nd ‘ 𝑧 ) = 𝑦 ) )
39	23 38	rexlimi	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃ 𝑧 ∈ 𝑇 ( 2nd ‘ 𝑧 ) = 𝑦 )
40	19 39	impbii	⊢ ( ∃ 𝑧 ∈ 𝑇 ( 2nd ‘ 𝑧 ) = 𝑦 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
41		fvelimab	⊢ ( ( 2nd Fn V ∧ 𝑇 ⊆ V ) → ( 𝑦 ∈ ( 2nd “ 𝑇 ) ↔ ∃ 𝑧 ∈ 𝑇 ( 2nd ‘ 𝑧 ) = 𝑦 ) )
42	5 6 41	mp2an	⊢ ( 𝑦 ∈ ( 2nd “ 𝑇 ) ↔ ∃ 𝑧 ∈ 𝑇 ( 2nd ‘ 𝑧 ) = 𝑦 )
43		eliun	⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
44	40 42 43	3bitr4i	⊢ ( 𝑦 ∈ ( 2nd “ 𝑇 ) ↔ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
45	44	eqriv	⊢ ( 2nd “ 𝑇 ) = ∪ 𝑥 ∈ 𝐴 𝐵
46	9 45	eqtr3i	⊢ ran ( 2nd ↾ 𝑇 ) = ∪ 𝑥 ∈ 𝐴 𝐵
47		df-fo	⊢ ( ( 2nd ↾ 𝑇 ) : 𝑇 –onto→ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ( ( 2nd ↾ 𝑇 ) Fn 𝑇 ∧ ran ( 2nd ↾ 𝑇 ) = ∪ 𝑥 ∈ 𝐴 𝐵 ) )
48	8 46 47	mpbir2an	⊢ ( 2nd ↾ 𝑇 ) : 𝑇 –onto→ ∪ 𝑥 ∈ 𝐴 𝐵