Theorem 1stconst 5862

Description: The mapping of a restriction of the 1^st function to a constant function. (Contributed by NM, 14-Dec-2008.)

Assertion

Ref	Expression
1stconst	⊢ (𝐵 ∈ 𝑉 → (1st ↾ (𝐴 × {𝐵})):(𝐴 × {𝐵})–1-1-onto→𝐴)

Proof of Theorem 1stconst

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

Step	Hyp	Ref	Expression
1		snmg 3508	. . 3 ⊢ (𝐵 ∈ 𝑉 → ∃𝑥 𝑥 ∈ {𝐵})
2		fo1stresm 5808	. . 3 ⊢ (∃𝑥 𝑥 ∈ {𝐵} → (1st ↾ (𝐴 × {𝐵})):(𝐴 × {𝐵})–onto→𝐴)
3	1, 2	syl 14	. 2 ⊢ (𝐵 ∈ 𝑉 → (1st ↾ (𝐴 × {𝐵})):(𝐴 × {𝐵})–onto→𝐴)
4		moeq 2767	. . . . . 6 ⊢ ∃*𝑥 𝑥 = ⟨𝑦, 𝐵⟩
5	4	moani 2011	. . . . 5 ⊢ ∃*𝑥(𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨𝑦, 𝐵⟩)
6		vex 2604	. . . . . . . 8 ⊢ 𝑦 ∈ V
7	6	brres 4636	. . . . . . 7 ⊢ (𝑥(1st ↾ (𝐴 × {𝐵}))𝑦 ↔ (𝑥1st 𝑦 ∧ 𝑥 ∈ (𝐴 × {𝐵})))
8		fo1st 5804	. . . . . . . . . . 11 ⊢ 1st :V–onto→V
9		fofn 5128	. . . . . . . . . . 11 ⊢ (1st :V–onto→V → 1st Fn V)
10	8, 9	ax-mp 7	. . . . . . . . . 10 ⊢ 1st Fn V
11		vex 2604	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
12		fnbrfvb 5235	. . . . . . . . . 10 ⊢ ((1st Fn V ∧ 𝑥 ∈ V) → ((1st ‘𝑥) = 𝑦 ↔ 𝑥1st 𝑦))
13	10, 11, 12	mp2an 416	. . . . . . . . 9 ⊢ ((1st ‘𝑥) = 𝑦 ↔ 𝑥1st 𝑦)
14	13	anbi1i 445	. . . . . . . 8 ⊢ (((1st ‘𝑥) = 𝑦 ∧ 𝑥 ∈ (𝐴 × {𝐵})) ↔ (𝑥1st 𝑦 ∧ 𝑥 ∈ (𝐴 × {𝐵})))
15		elxp7 5817	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴 × {𝐵}) ↔ (𝑥 ∈ (V × V) ∧ ((1st ‘𝑥) ∈ 𝐴 ∧ (2nd ‘𝑥) ∈ {𝐵})))
16		eleq1 2141	. . . . . . . . . . . . . . 15 ⊢ ((1st ‘𝑥) = 𝑦 → ((1st ‘𝑥) ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
17	16	biimpa 290	. . . . . . . . . . . . . 14 ⊢ (((1st ‘𝑥) = 𝑦 ∧ (1st ‘𝑥) ∈ 𝐴) → 𝑦 ∈ 𝐴)
18	17	adantrr 462	. . . . . . . . . . . . 13 ⊢ (((1st ‘𝑥) = 𝑦 ∧ ((1st ‘𝑥) ∈ 𝐴 ∧ (2nd ‘𝑥) ∈ {𝐵})) → 𝑦 ∈ 𝐴)
19	18	adantrl 461	. . . . . . . . . . . 12 ⊢ (((1st ‘𝑥) = 𝑦 ∧ (𝑥 ∈ (V × V) ∧ ((1st ‘𝑥) ∈ 𝐴 ∧ (2nd ‘𝑥) ∈ {𝐵}))) → 𝑦 ∈ 𝐴)
20		elsni 3416	. . . . . . . . . . . . . 14 ⊢ ((2nd ‘𝑥) ∈ {𝐵} → (2nd ‘𝑥) = 𝐵)
21		eqopi 5818	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ (V × V) ∧ ((1st ‘𝑥) = 𝑦 ∧ (2nd ‘𝑥) = 𝐵)) → 𝑥 = ⟨𝑦, 𝐵⟩)
22	21	an12s 529	. . . . . . . . . . . . . 14 ⊢ (((1st ‘𝑥) = 𝑦 ∧ (𝑥 ∈ (V × V) ∧ (2nd ‘𝑥) = 𝐵)) → 𝑥 = ⟨𝑦, 𝐵⟩)
23	20, 22	sylanr2 397	. . . . . . . . . . . . 13 ⊢ (((1st ‘𝑥) = 𝑦 ∧ (𝑥 ∈ (V × V) ∧ (2nd ‘𝑥) ∈ {𝐵})) → 𝑥 = ⟨𝑦, 𝐵⟩)
24	23	adantrrl 469	. . . . . . . . . . . 12 ⊢ (((1st ‘𝑥) = 𝑦 ∧ (𝑥 ∈ (V × V) ∧ ((1st ‘𝑥) ∈ 𝐴 ∧ (2nd ‘𝑥) ∈ {𝐵}))) → 𝑥 = ⟨𝑦, 𝐵⟩)
25	19, 24	jca 300	. . . . . . . . . . 11 ⊢ (((1st ‘𝑥) = 𝑦 ∧ (𝑥 ∈ (V × V) ∧ ((1st ‘𝑥) ∈ 𝐴 ∧ (2nd ‘𝑥) ∈ {𝐵}))) → (𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨𝑦, 𝐵⟩))
26	15, 25	sylan2b 281	. . . . . . . . . 10 ⊢ (((1st ‘𝑥) = 𝑦 ∧ 𝑥 ∈ (𝐴 × {𝐵})) → (𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨𝑦, 𝐵⟩))
27	26	adantl 271	. . . . . . . . 9 ⊢ ((𝐵 ∈ 𝑉 ∧ ((1st ‘𝑥) = 𝑦 ∧ 𝑥 ∈ (𝐴 × {𝐵}))) → (𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨𝑦, 𝐵⟩))
28		simprr 498	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ 𝑉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨𝑦, 𝐵⟩)) → 𝑥 = ⟨𝑦, 𝐵⟩)
29	28	fveq2d 5202	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ 𝑉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨𝑦, 𝐵⟩)) → (1st ‘𝑥) = (1st ‘⟨𝑦, 𝐵⟩))
30		simprl 497	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ 𝑉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨𝑦, 𝐵⟩)) → 𝑦 ∈ 𝐴)
31		simpl 107	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ 𝑉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨𝑦, 𝐵⟩)) → 𝐵 ∈ 𝑉)
32		op1stg 5797	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → (1st ‘⟨𝑦, 𝐵⟩) = 𝑦)
33	30, 31, 32	syl2anc 403	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ 𝑉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨𝑦, 𝐵⟩)) → (1st ‘⟨𝑦, 𝐵⟩) = 𝑦)
34	29, 33	eqtrd 2113	. . . . . . . . . 10 ⊢ ((𝐵 ∈ 𝑉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨𝑦, 𝐵⟩)) → (1st ‘𝑥) = 𝑦)
35		snidg 3423	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐵})
36	35	adantr 270	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ 𝑉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨𝑦, 𝐵⟩)) → 𝐵 ∈ {𝐵})
37		opelxpi 4394	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝐴 ∧ 𝐵 ∈ {𝐵}) → ⟨𝑦, 𝐵⟩ ∈ (𝐴 × {𝐵}))
38	30, 36, 37	syl2anc 403	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ 𝑉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨𝑦, 𝐵⟩)) → ⟨𝑦, 𝐵⟩ ∈ (𝐴 × {𝐵}))
39	28, 38	eqeltrd 2155	. . . . . . . . . 10 ⊢ ((𝐵 ∈ 𝑉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨𝑦, 𝐵⟩)) → 𝑥 ∈ (𝐴 × {𝐵}))
40	34, 39	jca 300	. . . . . . . . 9 ⊢ ((𝐵 ∈ 𝑉 ∧ (𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨𝑦, 𝐵⟩)) → ((1st ‘𝑥) = 𝑦 ∧ 𝑥 ∈ (𝐴 × {𝐵})))
41	27, 40	impbida 560	. . . . . . . 8 ⊢ (𝐵 ∈ 𝑉 → (((1st ‘𝑥) = 𝑦 ∧ 𝑥 ∈ (𝐴 × {𝐵})) ↔ (𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨𝑦, 𝐵⟩)))
42	14, 41	syl5bbr 192	. . . . . . 7 ⊢ (𝐵 ∈ 𝑉 → ((𝑥1st 𝑦 ∧ 𝑥 ∈ (𝐴 × {𝐵})) ↔ (𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨𝑦, 𝐵⟩)))
43	7, 42	syl5bb 190	. . . . . 6 ⊢ (𝐵 ∈ 𝑉 → (𝑥(1st ↾ (𝐴 × {𝐵}))𝑦 ↔ (𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨𝑦, 𝐵⟩)))
44	43	mobidv 1977	. . . . 5 ⊢ (𝐵 ∈ 𝑉 → (∃*𝑥 𝑥(1st ↾ (𝐴 × {𝐵}))𝑦 ↔ ∃*𝑥(𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨𝑦, 𝐵⟩)))
45	5, 44	mpbiri 166	. . . 4 ⊢ (𝐵 ∈ 𝑉 → ∃*𝑥 𝑥(1st ↾ (𝐴 × {𝐵}))𝑦)
46	45	alrimiv 1795	. . 3 ⊢ (𝐵 ∈ 𝑉 → ∀𝑦∃*𝑥 𝑥(1st ↾ (𝐴 × {𝐵}))𝑦)
47		funcnv2 4979	. . 3 ⊢ (Fun ◡(1st ↾ (𝐴 × {𝐵})) ↔ ∀𝑦∃*𝑥 𝑥(1st ↾ (𝐴 × {𝐵}))𝑦)
48	46, 47	sylibr 132	. 2 ⊢ (𝐵 ∈ 𝑉 → Fun ◡(1st ↾ (𝐴 × {𝐵})))
49		dff1o3 5152	. 2 ⊢ ((1st ↾ (𝐴 × {𝐵})):(𝐴 × {𝐵})–1-1-onto→𝐴 ↔ ((1st ↾ (𝐴 × {𝐵})):(𝐴 × {𝐵})–onto→𝐴 ∧ Fun ◡(1st ↾ (𝐴 × {𝐵}))))
50	3, 48, 49	sylanbrc 408	1 ⊢ (𝐵 ∈ 𝑉 → (1st ↾ (𝐴 × {𝐵})):(𝐴 × {𝐵})–1-1-onto→𝐴)

Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103  ∀wal 1282   = wceq 1284  ∃wex 1421   ∈ wcel 1433  ∃*wmo 1942  Vcvv 2601  {csn 3398  ⟨cop 3401   class class class wbr 3785   × cxp 4361  ^◡ccnv 4362   ↾ cres 4365  Fun wfun 4916   Fn wfn 4917  –onto→wfo 4920  –1-1-onto→wf1o 4921  ‘cfv 4922  1^st c1st 5785  2^nd c2nd 5786

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 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-13 1444  ax-14 1445  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-sep 3896  ax-pow 3948  ax-pr 3964  ax-un 4188

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-eu 1944  df-mo 1945  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ral 2353  df-rex 2354  df-rab 2357  df-v 2603  df-sbc 2816  df-csb 2909  df-un 2977  df-in 2979  df-ss 2986  df-pw 3384  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-iun 3680  df-br 3786  df-opab 3840  df-mpt 3841  df-id 4048  df-xp 4369  df-rel 4370  df-cnv 4371  df-co 4372  df-dm 4373  df-rn 4374  df-res 4375  df-ima 4376  df-iota 4887  df-fun 4924  df-fn 4925  df-f 4926  df-f1 4927  df-fo 4928  df-f1o 4929  df-fv 4930  df-1st 5787  df-2nd 5788

This theorem is referenced by: (None)