Theorem f2ndres 5931

Description: Mapping of a restriction of the 2^nd (second member of an ordered pair) function. (Contributed by NM, 7-Aug-2006.) (Revised by Mario Carneiro, 8-Sep-2013.)

Assertion

Ref	Expression
f2ndres	⊢ (2nd ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)⟶𝐵

Proof of Theorem f2ndres

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2622	. . . . . . . 8 ⊢ 𝑦 ∈ V
2		vex 2622	. . . . . . . 8 ⊢ 𝑧 ∈ V
3	1, 2	op2nda 4915	. . . . . . 7 ⊢ ∪ ran {⟨𝑦, 𝑧⟩} = 𝑧
4	3	eleq1i 2153	. . . . . 6 ⊢ (∪ ran {⟨𝑦, 𝑧⟩} ∈ 𝐵 ↔ 𝑧 ∈ 𝐵)
5	4	biimpri 131	. . . . 5 ⊢ (𝑧 ∈ 𝐵 → ∪ ran {⟨𝑦, 𝑧⟩} ∈ 𝐵)
6	5	adantl 271	. . . 4 ⊢ ((𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → ∪ ran {⟨𝑦, 𝑧⟩} ∈ 𝐵)
7	6	rgen2 2459	. . 3 ⊢ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ∪ ran {⟨𝑦, 𝑧⟩} ∈ 𝐵
8		sneq 3457	. . . . . . 7 ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → {𝑥} = {⟨𝑦, 𝑧⟩})
9	8	rneqd 4664	. . . . . 6 ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → ran {𝑥} = ran {⟨𝑦, 𝑧⟩})
10	9	unieqd 3664	. . . . 5 ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → ∪ ran {𝑥} = ∪ ran {⟨𝑦, 𝑧⟩})
11	10	eleq1d 2156	. . . 4 ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → (∪ ran {𝑥} ∈ 𝐵 ↔ ∪ ran {⟨𝑦, 𝑧⟩} ∈ 𝐵))
12	11	ralxp 4579	. . 3 ⊢ (∀𝑥 ∈ (𝐴 × 𝐵)∪ ran {𝑥} ∈ 𝐵 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐵 ∪ ran {⟨𝑦, 𝑧⟩} ∈ 𝐵)
13	7, 12	mpbir 144	. 2 ⊢ ∀𝑥 ∈ (𝐴 × 𝐵)∪ ran {𝑥} ∈ 𝐵
14		df-2nd 5912	. . . . 5 ⊢ 2nd = (𝑥 ∈ V ↦ ∪ ran {𝑥})
15	14	reseq1i 4709	. . . 4 ⊢ (2nd ↾ (𝐴 × 𝐵)) = ((𝑥 ∈ V ↦ ∪ ran {𝑥}) ↾ (𝐴 × 𝐵))
16		ssv 3046	. . . . 5 ⊢ (𝐴 × 𝐵) ⊆ V
17		resmpt 4760	. . . . 5 ⊢ ((𝐴 × 𝐵) ⊆ V → ((𝑥 ∈ V ↦ ∪ ran {𝑥}) ↾ (𝐴 × 𝐵)) = (𝑥 ∈ (𝐴 × 𝐵) ↦ ∪ ran {𝑥}))
18	16, 17	ax-mp 7	. . . 4 ⊢ ((𝑥 ∈ V ↦ ∪ ran {𝑥}) ↾ (𝐴 × 𝐵)) = (𝑥 ∈ (𝐴 × 𝐵) ↦ ∪ ran {𝑥})
19	15, 18	eqtri 2108	. . 3 ⊢ (2nd ↾ (𝐴 × 𝐵)) = (𝑥 ∈ (𝐴 × 𝐵) ↦ ∪ ran {𝑥})
20	19	fmpt 5449	. 2 ⊢ (∀𝑥 ∈ (𝐴 × 𝐵)∪ ran {𝑥} ∈ 𝐵 ↔ (2nd ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)⟶𝐵)
21	13, 20	mpbi 143	1 ⊢ (2nd ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)⟶𝐵

Syntax hints:   = wceq 1289   ∈ wcel 1438  ∀wral 2359  Vcvv 2619   ⊆ wss 2999  {csn 3446  ⟨cop 3449  ∪ cuni 3653   ↦ cmpt 3899   × cxp 4436  ran crn 4439   ↾ cres 4440  ⟶wf 5011  2^nd c2nd 5910

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3957  ax-pow 4009  ax-pr 4036

This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-rab 2368  df-v 2621  df-sbc 2841  df-csb 2934  df-un 3003  df-in 3005  df-ss 3012  df-pw 3431  df-sn 3452  df-pr 3453  df-op 3455  df-uni 3654  df-iun 3732  df-br 3846  df-opab 3900  df-mpt 3901  df-id 4120  df-xp 4444  df-rel 4445  df-cnv 4446  df-co 4447  df-dm 4448  df-rn 4449  df-res 4450  df-ima 4451  df-iota 4980  df-fun 5017  df-fn 5018  df-f 5019  df-fv 5023  df-2nd 5912

This theorem is referenced by:  fo2ndresm  5933  2ndcof  5935  f2ndf  5991  eucialgcvga  11318