Metamath Proof Explorer

Theorem fparlem2

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

		Ref	Expression
	Assertion	fparlem2	⊢ ( ^◡ ( 2^nd ↾ ( V × V ) ) “ { 𝑦 } ) = ( V × { 𝑦 } )

Proof

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