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 ( ( 2nd ↾ ( V × V ) ) “ { 𝑦 } ) = ( V × { 𝑦 } )

Proof

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