Theorem 2ndimaxp 30492

Description: Image of a cartesian product by 2^nd. (Contributed by Thierry Arnoux, 23-Jun-2024.)

Assertion

Ref	Expression
2ndimaxp	⊢ (𝐴 ≠ ∅ → (2nd “ (𝐴 × 𝐵)) = 𝐵)

Proof of Theorem 2ndimaxp

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

Step	Hyp	Ref	Expression
1		ima0 5910	. . . 4 ⊢ (2nd “ ∅) = ∅
2		xpeq2 5538	. . . . . 6 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = (𝐴 × ∅))
3		xp0 5980	. . . . . 6 ⊢ (𝐴 × ∅) = ∅
4	2, 3	eqtrdi 2810	. . . . 5 ⊢ (𝐵 = ∅ → (𝐴 × 𝐵) = ∅)
5	4	imaeq2d 5894	. . . 4 ⊢ (𝐵 = ∅ → (2nd “ (𝐴 × 𝐵)) = (2nd “ ∅))
6		id 22	. . . 4 ⊢ (𝐵 = ∅ → 𝐵 = ∅)
7	1, 5, 6	3eqtr4a 2820	. . 3 ⊢ (𝐵 = ∅ → (2nd “ (𝐴 × 𝐵)) = 𝐵)
8	7	adantl 486	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 = ∅) → (2nd “ (𝐴 × 𝐵)) = 𝐵)
9		xpnz 5981	. . . . 5 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ↔ (𝐴 × 𝐵) ≠ ∅)
10		fo2nd 7707	. . . . . . 7 ⊢ 2nd :V–onto→V
11		fofn 6571	. . . . . . 7 ⊢ (2nd :V–onto→V → 2nd Fn V)
12	10, 11	mp1i 13	. . . . . 6 ⊢ ((𝐴 × 𝐵) ≠ ∅ → 2nd Fn V)
13		ssv 3912	. . . . . . 7 ⊢ (𝐴 × 𝐵) ⊆ V
14	13	a1i 11	. . . . . 6 ⊢ ((𝐴 × 𝐵) ≠ ∅ → (𝐴 × 𝐵) ⊆ V)
15	12, 14	fvelimabd 6719	. . . . 5 ⊢ ((𝐴 × 𝐵) ≠ ∅ → (𝑦 ∈ (2nd “ (𝐴 × 𝐵)) ↔ ∃𝑝 ∈ (𝐴 × 𝐵)(2nd ‘𝑝) = 𝑦))
16	9, 15	sylbi 220	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (𝑦 ∈ (2nd “ (𝐴 × 𝐵)) ↔ ∃𝑝 ∈ (𝐴 × 𝐵)(2nd ‘𝑝) = 𝑦))
17		simpr 489	. . . . . . 7 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ (2nd ‘𝑝) = 𝑦) → (2nd ‘𝑝) = 𝑦)
18		xp2nd 7719	. . . . . . . 8 ⊢ (𝑝 ∈ (𝐴 × 𝐵) → (2nd ‘𝑝) ∈ 𝐵)
19	18	ad2antlr 727	. . . . . . 7 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ (2nd ‘𝑝) = 𝑦) → (2nd ‘𝑝) ∈ 𝐵)
20	17, 19	eqeltrrd 2852	. . . . . 6 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ 𝑝 ∈ (𝐴 × 𝐵)) ∧ (2nd ‘𝑝) = 𝑦) → 𝑦 ∈ 𝐵)
21	20	r19.29an 3210	. . . . 5 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ ∃𝑝 ∈ (𝐴 × 𝐵)(2nd ‘𝑝) = 𝑦) → 𝑦 ∈ 𝐵)
22		n0 4239	. . . . . . . 8 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ 𝐴)
23	22	biimpi 219	. . . . . . 7 ⊢ (𝐴 ≠ ∅ → ∃𝑥 𝑥 ∈ 𝐴)
24	23	ad2antrr 726	. . . . . 6 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ 𝑦 ∈ 𝐵) → ∃𝑥 𝑥 ∈ 𝐴)
25		opelxpi 5554	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵))
26	25	ancoms 463	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) → ⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵))
27	26	adantll 714	. . . . . . 7 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ 𝑦 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → ⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵))
28		fveqeq2 6660	. . . . . . . 8 ⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → ((2nd ‘𝑝) = 𝑦 ↔ (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦))
29	28	adantl 486	. . . . . . 7 ⊢ (((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ 𝑦 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑝 = ⟨𝑥, 𝑦⟩) → ((2nd ‘𝑝) = 𝑦 ↔ (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦))
30		vex 3411	. . . . . . . . 9 ⊢ 𝑥 ∈ V
31		vex 3411	. . . . . . . . 9 ⊢ 𝑦 ∈ V
32	30, 31	op2nd 7695	. . . . . . . 8 ⊢ (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦
33	32	a1i 11	. . . . . . 7 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ 𝑦 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦)
34	27, 29, 33	rspcedvd 3542	. . . . . 6 ⊢ ((((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ 𝑦 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → ∃𝑝 ∈ (𝐴 × 𝐵)(2nd ‘𝑝) = 𝑦)
35	24, 34	exlimddv 1937	. . . . 5 ⊢ (((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ∧ 𝑦 ∈ 𝐵) → ∃𝑝 ∈ (𝐴 × 𝐵)(2nd ‘𝑝) = 𝑦)
36	21, 35	impbida 801	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (∃𝑝 ∈ (𝐴 × 𝐵)(2nd ‘𝑝) = 𝑦 ↔ 𝑦 ∈ 𝐵))
37	16, 36	bitrd 282	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (𝑦 ∈ (2nd “ (𝐴 × 𝐵)) ↔ 𝑦 ∈ 𝐵))
38	37	eqrdv 2757	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → (2nd “ (𝐴 × 𝐵)) = 𝐵)
39	8, 38	pm2.61dane 3036	1 ⊢ (𝐴 ≠ ∅ → (2nd “ (𝐴 × 𝐵)) = 𝐵)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1539  ∃wex 1782   ∈ wcel 2112   ≠ wne 2949  ∃wrex 3069  Vcvv 3407   ⊆ wss 3854  ∅c0 4221  ⟨cop 4521   × cxp 5515   “ cima 5520   Fn wfn 6323  –onto→wfo 6326  ‘cfv 6328  2^nd c2nd 7685

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5162  ax-nul 5169  ax-pr 5291  ax-un 7452

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3an 1087  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2899  df-ne 2950  df-ral 3073  df-rex 3074  df-rab 3077  df-v 3409  df-sbc 3694  df-dif 3857  df-un 3859  df-in 3861  df-ss 3871  df-nul 4222  df-if 4414  df-sn 4516  df-pr 4518  df-op 4522  df-uni 4792  df-br 5026  df-opab 5088  df-mpt 5106  df-id 5423  df-xp 5523  df-rel 5524  df-cnv 5525  df-co 5526  df-dm 5527  df-rn 5528  df-res 5529  df-ima 5530  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-fo 6334  df-fv 6336  df-2nd 7687

This theorem is referenced by:  gsumpart  30826