fv1stcnv

Description: The value of the converse of 1st restricted to a singleton. (Contributed by Scott Fenton, 2-Jul-2020)

		Ref	Expression
	Assertion	fv1stcnv	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉 ) → ( ^◡ ( 1^st ↾ ( 𝐴 × { 𝑌 } ) ) ‘ 𝑋 ) = ⟨ 𝑋 , 𝑌 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		snidg	⊢ ( 𝑌 ∈ 𝑉 → 𝑌 ∈ { 𝑌 } )
2	1	anim2i	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ { 𝑌 } ) )
3		eqid	⊢ 𝑋 = 𝑋
4	2 3	jctir	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ { 𝑌 } ) ∧ 𝑋 = 𝑋 ) )
5		opex	⊢ ⟨ 𝑋 , 𝑌 ⟩ ∈ V
6		brcnvg	⊢ ( ( 𝑋 ∈ 𝐴 ∧ ⟨ 𝑋 , 𝑌 ⟩ ∈ V ) → ( 𝑋 ^◡ ( 1^st ↾ ( 𝐴 × { 𝑌 } ) ) ⟨ 𝑋 , 𝑌 ⟩ ↔ ⟨ 𝑋 , 𝑌 ⟩ ( 1^st ↾ ( 𝐴 × { 𝑌 } ) ) 𝑋 ) )
7	5 6	mpan2	⊢ ( 𝑋 ∈ 𝐴 → ( 𝑋 ^◡ ( 1^st ↾ ( 𝐴 × { 𝑌 } ) ) ⟨ 𝑋 , 𝑌 ⟩ ↔ ⟨ 𝑋 , 𝑌 ⟩ ( 1^st ↾ ( 𝐴 × { 𝑌 } ) ) 𝑋 ) )
8		brres	⊢ ( 𝑋 ∈ 𝐴 → ( ⟨ 𝑋 , 𝑌 ⟩ ( 1^st ↾ ( 𝐴 × { 𝑌 } ) ) 𝑋 ↔ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐴 × { 𝑌 } ) ∧ ⟨ 𝑋 , 𝑌 ⟩ 1^st 𝑋 ) ) )
9	7 8	bitrd	⊢ ( 𝑋 ∈ 𝐴 → ( 𝑋 ^◡ ( 1^st ↾ ( 𝐴 × { 𝑌 } ) ) ⟨ 𝑋 , 𝑌 ⟩ ↔ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐴 × { 𝑌 } ) ∧ ⟨ 𝑋 , 𝑌 ⟩ 1^st 𝑋 ) ) )
10	9	adantr	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ^◡ ( 1^st ↾ ( 𝐴 × { 𝑌 } ) ) ⟨ 𝑋 , 𝑌 ⟩ ↔ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐴 × { 𝑌 } ) ∧ ⟨ 𝑋 , 𝑌 ⟩ 1^st 𝑋 ) ) )
11		opelxp	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐴 × { 𝑌 } ) ↔ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ { 𝑌 } ) )
12	11	anbi1i	⊢ ( ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐴 × { 𝑌 } ) ∧ ⟨ 𝑋 , 𝑌 ⟩ 1^st 𝑋 ) ↔ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ { 𝑌 } ) ∧ ⟨ 𝑋 , 𝑌 ⟩ 1^st 𝑋 ) )
13		br1steqg	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉 ) → ( ⟨ 𝑋 , 𝑌 ⟩ 1^st 𝑋 ↔ 𝑋 = 𝑋 ) )
14	13	anbi2d	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉 ) → ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ { 𝑌 } ) ∧ ⟨ 𝑋 , 𝑌 ⟩ 1^st 𝑋 ) ↔ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ { 𝑌 } ) ∧ 𝑋 = 𝑋 ) ) )
15	12 14	syl5bb	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉 ) → ( ( ⟨ 𝑋 , 𝑌 ⟩ ∈ ( 𝐴 × { 𝑌 } ) ∧ ⟨ 𝑋 , 𝑌 ⟩ 1^st 𝑋 ) ↔ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ { 𝑌 } ) ∧ 𝑋 = 𝑋 ) ) )
16	10 15	bitrd	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ^◡ ( 1^st ↾ ( 𝐴 × { 𝑌 } ) ) ⟨ 𝑋 , 𝑌 ⟩ ↔ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ { 𝑌 } ) ∧ 𝑋 = 𝑋 ) ) )
17	4 16	mpbird	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉 ) → 𝑋 ^◡ ( 1^st ↾ ( 𝐴 × { 𝑌 } ) ) ⟨ 𝑋 , 𝑌 ⟩ )
18		1stconst	⊢ ( 𝑌 ∈ 𝑉 → ( 1^st ↾ ( 𝐴 × { 𝑌 } ) ) : ( 𝐴 × { 𝑌 } ) –1-1-onto→ 𝐴 )
19		f1ocnv	⊢ ( ( 1^st ↾ ( 𝐴 × { 𝑌 } ) ) : ( 𝐴 × { 𝑌 } ) –1-1-onto→ 𝐴 → ^◡ ( 1^st ↾ ( 𝐴 × { 𝑌 } ) ) : 𝐴 –1-1-onto→ ( 𝐴 × { 𝑌 } ) )
20		f1ofn	⊢ ( ^◡ ( 1^st ↾ ( 𝐴 × { 𝑌 } ) ) : 𝐴 –1-1-onto→ ( 𝐴 × { 𝑌 } ) → ^◡ ( 1^st ↾ ( 𝐴 × { 𝑌 } ) ) Fn 𝐴 )
21	18 19 20	3syl	⊢ ( 𝑌 ∈ 𝑉 → ^◡ ( 1^st ↾ ( 𝐴 × { 𝑌 } ) ) Fn 𝐴 )
22		simpl	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉 ) → 𝑋 ∈ 𝐴 )
23		fnbrfvb	⊢ ( ( ^◡ ( 1^st ↾ ( 𝐴 × { 𝑌 } ) ) Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ( ^◡ ( 1^st ↾ ( 𝐴 × { 𝑌 } ) ) ‘ 𝑋 ) = ⟨ 𝑋 , 𝑌 ⟩ ↔ 𝑋 ^◡ ( 1^st ↾ ( 𝐴 × { 𝑌 } ) ) ⟨ 𝑋 , 𝑌 ⟩ ) )
24	21 22 23	syl2an2	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉 ) → ( ( ^◡ ( 1^st ↾ ( 𝐴 × { 𝑌 } ) ) ‘ 𝑋 ) = ⟨ 𝑋 , 𝑌 ⟩ ↔ 𝑋 ^◡ ( 1^st ↾ ( 𝐴 × { 𝑌 } ) ) ⟨ 𝑋 , 𝑌 ⟩ ) )
25	17 24	mpbird	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉 ) → ( ^◡ ( 1^st ↾ ( 𝐴 × { 𝑌 } ) ) ‘ 𝑋 ) = ⟨ 𝑋 , 𝑌 ⟩ )

Metamath Proof Explorer

Theorem fv1stcnv

Proof