Theorem 1stconst

Description: The mapping of a restriction of the 1st function to a constant function. (Contributed by NM, 14-Dec-2008) (Proof shortened by Peter Mazsa, 2-Oct-2022)

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

Proof

Step	Hyp	Ref	Expression
1		snnzg	⊢ ( 𝐵 ∈ 𝑉 → { 𝐵 } ≠ ∅ )
2		fo1stres	⊢ ( { 𝐵 } ≠ ∅ → ( 1st ↾ ( 𝐴 × { 𝐵 } ) ) : ( 𝐴 × { 𝐵 } ) –onto→ 𝐴 )
3	1 2	syl	⊢ ( 𝐵 ∈ 𝑉 → ( 1st ↾ ( 𝐴 × { 𝐵 } ) ) : ( 𝐴 × { 𝐵 } ) –onto→ 𝐴 )
4		moeq	⊢ ∃* 𝑥 𝑥 = ⟨ 𝑦 , 𝐵 ⟩
5	4	moani	⊢ ∃* 𝑥 ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨ 𝑦 , 𝐵 ⟩ )
6		vex	⊢ 𝑦 ∈ V
7	6	brresi	⊢ ( 𝑥 ( 1st ↾ ( 𝐴 × { 𝐵 } ) ) 𝑦 ↔ ( 𝑥 ∈ ( 𝐴 × { 𝐵 } ) ∧ 𝑥 1st 𝑦 ) )
8		fo1st	⊢ 1st : V –onto→ V
9		fofn	⊢ ( 1st : V –onto→ V → 1st Fn V )
10	8 9	ax-mp	⊢ 1st Fn V
11		vex	⊢ 𝑥 ∈ V
12		fnbrfvb	⊢ ( ( 1st Fn V ∧ 𝑥 ∈ V ) → ( ( 1st ‘ 𝑥 ) = 𝑦 ↔ 𝑥 1st 𝑦 ) )
13	10 11 12	mp2an	⊢ ( ( 1st ‘ 𝑥 ) = 𝑦 ↔ 𝑥 1st 𝑦 )
14	13	anbi2i	⊢ ( ( 𝑥 ∈ ( 𝐴 × { 𝐵 } ) ∧ ( 1st ‘ 𝑥 ) = 𝑦 ) ↔ ( 𝑥 ∈ ( 𝐴 × { 𝐵 } ) ∧ 𝑥 1st 𝑦 ) )
15		elxp7	⊢ ( 𝑥 ∈ ( 𝐴 × { 𝐵 } ) ↔ ( 𝑥 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝐴 ∧ ( 2nd ‘ 𝑥 ) ∈ { 𝐵 } ) ) )
16		eleq1	⊢ ( ( 1st ‘ 𝑥 ) = 𝑦 → ( ( 1st ‘ 𝑥 ) ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
17	16	biimpac	⊢ ( ( ( 1st ‘ 𝑥 ) ∈ 𝐴 ∧ ( 1st ‘ 𝑥 ) = 𝑦 ) → 𝑦 ∈ 𝐴 )
18	17	adantlr	⊢ ( ( ( ( 1st ‘ 𝑥 ) ∈ 𝐴 ∧ ( 2nd ‘ 𝑥 ) ∈ { 𝐵 } ) ∧ ( 1st ‘ 𝑥 ) = 𝑦 ) → 𝑦 ∈ 𝐴 )
19	18	adantll	⊢ ( ( ( 𝑥 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝐴 ∧ ( 2nd ‘ 𝑥 ) ∈ { 𝐵 } ) ) ∧ ( 1st ‘ 𝑥 ) = 𝑦 ) → 𝑦 ∈ 𝐴 )
20		elsni	⊢ ( ( 2nd ‘ 𝑥 ) ∈ { 𝐵 } → ( 2nd ‘ 𝑥 ) = 𝐵 )
21		eqopi	⊢ ( ( 𝑥 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑥 ) = 𝑦 ∧ ( 2nd ‘ 𝑥 ) = 𝐵 ) ) → 𝑥 = ⟨ 𝑦 , 𝐵 ⟩ )
22	21	anass1rs	⊢ ( ( ( 𝑥 ∈ ( V × V ) ∧ ( 2nd ‘ 𝑥 ) = 𝐵 ) ∧ ( 1st ‘ 𝑥 ) = 𝑦 ) → 𝑥 = ⟨ 𝑦 , 𝐵 ⟩ )
23	20 22	sylanl2	⊢ ( ( ( 𝑥 ∈ ( V × V ) ∧ ( 2nd ‘ 𝑥 ) ∈ { 𝐵 } ) ∧ ( 1st ‘ 𝑥 ) = 𝑦 ) → 𝑥 = ⟨ 𝑦 , 𝐵 ⟩ )
24	23	adantlrl	⊢ ( ( ( 𝑥 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝐴 ∧ ( 2nd ‘ 𝑥 ) ∈ { 𝐵 } ) ) ∧ ( 1st ‘ 𝑥 ) = 𝑦 ) → 𝑥 = ⟨ 𝑦 , 𝐵 ⟩ )
25	19 24	jca	⊢ ( ( ( 𝑥 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑥 ) ∈ 𝐴 ∧ ( 2nd ‘ 𝑥 ) ∈ { 𝐵 } ) ) ∧ ( 1st ‘ 𝑥 ) = 𝑦 ) → ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨ 𝑦 , 𝐵 ⟩ ) )
26	15 25	sylanb	⊢ ( ( 𝑥 ∈ ( 𝐴 × { 𝐵 } ) ∧ ( 1st ‘ 𝑥 ) = 𝑦 ) → ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨ 𝑦 , 𝐵 ⟩ ) )
27	26	adantl	⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝑥 ∈ ( 𝐴 × { 𝐵 } ) ∧ ( 1st ‘ 𝑥 ) = 𝑦 ) ) → ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨ 𝑦 , 𝐵 ⟩ ) )
28		simprr	⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨ 𝑦 , 𝐵 ⟩ ) ) → 𝑥 = ⟨ 𝑦 , 𝐵 ⟩ )
29		simprl	⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨ 𝑦 , 𝐵 ⟩ ) ) → 𝑦 ∈ 𝐴 )
30		snidg	⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ { 𝐵 } )
31	30	adantr	⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨ 𝑦 , 𝐵 ⟩ ) ) → 𝐵 ∈ { 𝐵 } )
32	29 31	opelxpd	⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨ 𝑦 , 𝐵 ⟩ ) ) → ⟨ 𝑦 , 𝐵 ⟩ ∈ ( 𝐴 × { 𝐵 } ) )
33	28 32	eqeltrd	⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨ 𝑦 , 𝐵 ⟩ ) ) → 𝑥 ∈ ( 𝐴 × { 𝐵 } ) )
34	28	fveq2d	⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨ 𝑦 , 𝐵 ⟩ ) ) → ( 1st ‘ 𝑥 ) = ( 1st ‘ ⟨ 𝑦 , 𝐵 ⟩ ) )
35		simpl	⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨ 𝑦 , 𝐵 ⟩ ) ) → 𝐵 ∈ 𝑉 )
36		op1stg	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉 ) → ( 1st ‘ ⟨ 𝑦 , 𝐵 ⟩ ) = 𝑦 )
37	29 35 36	syl2anc	⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨ 𝑦 , 𝐵 ⟩ ) ) → ( 1st ‘ ⟨ 𝑦 , 𝐵 ⟩ ) = 𝑦 )
38	34 37	eqtrd	⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨ 𝑦 , 𝐵 ⟩ ) ) → ( 1st ‘ 𝑥 ) = 𝑦 )
39	33 38	jca	⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨ 𝑦 , 𝐵 ⟩ ) ) → ( 𝑥 ∈ ( 𝐴 × { 𝐵 } ) ∧ ( 1st ‘ 𝑥 ) = 𝑦 ) )
40	27 39	impbida	⊢ ( 𝐵 ∈ 𝑉 → ( ( 𝑥 ∈ ( 𝐴 × { 𝐵 } ) ∧ ( 1st ‘ 𝑥 ) = 𝑦 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨ 𝑦 , 𝐵 ⟩ ) ) )
41	14 40	bitr3id	⊢ ( 𝐵 ∈ 𝑉 → ( ( 𝑥 ∈ ( 𝐴 × { 𝐵 } ) ∧ 𝑥 1st 𝑦 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨ 𝑦 , 𝐵 ⟩ ) ) )
42	7 41	bitrid	⊢ ( 𝐵 ∈ 𝑉 → ( 𝑥 ( 1st ↾ ( 𝐴 × { 𝐵 } ) ) 𝑦 ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨ 𝑦 , 𝐵 ⟩ ) ) )
43	42	mobidv	⊢ ( 𝐵 ∈ 𝑉 → ( ∃* 𝑥 𝑥 ( 1st ↾ ( 𝐴 × { 𝐵 } ) ) 𝑦 ↔ ∃* 𝑥 ( 𝑦 ∈ 𝐴 ∧ 𝑥 = ⟨ 𝑦 , 𝐵 ⟩ ) ) )
44	5 43	mpbiri	⊢ ( 𝐵 ∈ 𝑉 → ∃* 𝑥 𝑥 ( 1st ↾ ( 𝐴 × { 𝐵 } ) ) 𝑦 )
45	44	alrimiv	⊢ ( 𝐵 ∈ 𝑉 → ∀ 𝑦 ∃* 𝑥 𝑥 ( 1st ↾ ( 𝐴 × { 𝐵 } ) ) 𝑦 )
46		funcnv2	⊢ ( Fun ◡ ( 1st ↾ ( 𝐴 × { 𝐵 } ) ) ↔ ∀ 𝑦 ∃* 𝑥 𝑥 ( 1st ↾ ( 𝐴 × { 𝐵 } ) ) 𝑦 )
47	45 46	sylibr	⊢ ( 𝐵 ∈ 𝑉 → Fun ◡ ( 1st ↾ ( 𝐴 × { 𝐵 } ) ) )
48		dff1o3	⊢ ( ( 1st ↾ ( 𝐴 × { 𝐵 } ) ) : ( 𝐴 × { 𝐵 } ) –1-1-onto→ 𝐴 ↔ ( ( 1st ↾ ( 𝐴 × { 𝐵 } ) ) : ( 𝐴 × { 𝐵 } ) –onto→ 𝐴 ∧ Fun ◡ ( 1st ↾ ( 𝐴 × { 𝐵 } ) ) ) )
49	3 47 48	sylanbrc	⊢ ( 𝐵 ∈ 𝑉 → ( 1st ↾ ( 𝐴 × { 𝐵 } ) ) : ( 𝐴 × { 𝐵 } ) –1-1-onto→ 𝐴 )