Theorem 2ndconst

Description: The mapping of a restriction of the 2nd function to a converse constant function. (Contributed by NM, 27-Mar-2008) (Proof shortened by Peter Mazsa, 2-Oct-2022)

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

Proof

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