Metamath Proof Explorer

Theorem fparlem1

Description: Lemma for fpar . (Contributed by NM, 22-Dec-2008) (Revised by Mario Carneiro, 28-Apr-2015)

		Ref	Expression
	Assertion	fparlem1	⊢ ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑥 } ) = ( { 𝑥 } × V )

Proof

Step	Hyp	Ref	Expression
1		fvres	⊢ ( 𝑦 ∈ ( V × V ) → ( ( 1^st ↾ ( V × V ) ) ‘ 𝑦 ) = ( 1^st ‘ 𝑦 ) )
2	1	eqeq1d	⊢ ( 𝑦 ∈ ( V × V ) → ( ( ( 1^st ↾ ( V × V ) ) ‘ 𝑦 ) = 𝑥 ↔ ( 1^st ‘ 𝑦 ) = 𝑥 ) )
3		vex	⊢ 𝑥 ∈ V
4	3	elsn2	⊢ ( ( 1^st ‘ 𝑦 ) ∈ { 𝑥 } ↔ ( 1^st ‘ 𝑦 ) = 𝑥 )
5		fvex	⊢ ( 2^nd ‘ 𝑦 ) ∈ V
6	5	biantru	⊢ ( ( 1^st ‘ 𝑦 ) ∈ { 𝑥 } ↔ ( ( 1^st ‘ 𝑦 ) ∈ { 𝑥 } ∧ ( 2^nd ‘ 𝑦 ) ∈ V ) )
7	4 6	bitr3i	⊢ ( ( 1^st ‘ 𝑦 ) = 𝑥 ↔ ( ( 1^st ‘ 𝑦 ) ∈ { 𝑥 } ∧ ( 2^nd ‘ 𝑦 ) ∈ V ) )
8	2 7	bitrdi	⊢ ( 𝑦 ∈ ( V × V ) → ( ( ( 1^st ↾ ( V × V ) ) ‘ 𝑦 ) = 𝑥 ↔ ( ( 1^st ‘ 𝑦 ) ∈ { 𝑥 } ∧ ( 2^nd ‘ 𝑦 ) ∈ V ) ) )
9	8	pm5.32i	⊢ ( ( 𝑦 ∈ ( V × V ) ∧ ( ( 1^st ↾ ( V × V ) ) ‘ 𝑦 ) = 𝑥 ) ↔ ( 𝑦 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑦 ) ∈ { 𝑥 } ∧ ( 2^nd ‘ 𝑦 ) ∈ V ) ) )
10		f1stres	⊢ ( 1^st ↾ ( V × V ) ) : ( V × V ) ⟶ V
11		ffn	⊢ ( ( 1^st ↾ ( V × V ) ) : ( V × V ) ⟶ V → ( 1^st ↾ ( V × V ) ) Fn ( V × V ) )
12		fniniseg	⊢ ( ( 1^st ↾ ( V × V ) ) Fn ( V × V ) → ( 𝑦 ∈ ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑥 } ) ↔ ( 𝑦 ∈ ( V × V ) ∧ ( ( 1^st ↾ ( V × V ) ) ‘ 𝑦 ) = 𝑥 ) ) )
13	10 11 12	mp2b	⊢ ( 𝑦 ∈ ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑥 } ) ↔ ( 𝑦 ∈ ( V × V ) ∧ ( ( 1^st ↾ ( V × V ) ) ‘ 𝑦 ) = 𝑥 ) )
14		elxp7	⊢ ( 𝑦 ∈ ( { 𝑥 } × V ) ↔ ( 𝑦 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑦 ) ∈ { 𝑥 } ∧ ( 2^nd ‘ 𝑦 ) ∈ V ) ) )
15	9 13 14	3bitr4i	⊢ ( 𝑦 ∈ ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑥 } ) ↔ 𝑦 ∈ ( { 𝑥 } × V ) )
16	15	eqriv	⊢ ( ^◡ ( 1^st ↾ ( V × V ) ) “ { 𝑥 } ) = ( { 𝑥 } × V )