Metamath Proof Explorer


Theorem elixpsn

Description: Membership in a class of singleton functions. (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Assertion elixpsn ( 𝐴𝑉 → ( 𝐹X 𝑥 ∈ { 𝐴 } 𝐵 ↔ ∃ 𝑦𝐵 𝐹 = { ⟨ 𝐴 , 𝑦 ⟩ } ) )

Proof

Step Hyp Ref Expression
1 sneq ( 𝑧 = 𝐴 → { 𝑧 } = { 𝐴 } )
2 1 ixpeq1d ( 𝑧 = 𝐴X 𝑥 ∈ { 𝑧 } 𝐵 = X 𝑥 ∈ { 𝐴 } 𝐵 )
3 2 eleq2d ( 𝑧 = 𝐴 → ( 𝐹X 𝑥 ∈ { 𝑧 } 𝐵𝐹X 𝑥 ∈ { 𝐴 } 𝐵 ) )
4 opeq1 ( 𝑧 = 𝐴 → ⟨ 𝑧 , 𝑦 ⟩ = ⟨ 𝐴 , 𝑦 ⟩ )
5 4 sneqd ( 𝑧 = 𝐴 → { ⟨ 𝑧 , 𝑦 ⟩ } = { ⟨ 𝐴 , 𝑦 ⟩ } )
6 5 eqeq2d ( 𝑧 = 𝐴 → ( 𝐹 = { ⟨ 𝑧 , 𝑦 ⟩ } ↔ 𝐹 = { ⟨ 𝐴 , 𝑦 ⟩ } ) )
7 6 rexbidv ( 𝑧 = 𝐴 → ( ∃ 𝑦𝐵 𝐹 = { ⟨ 𝑧 , 𝑦 ⟩ } ↔ ∃ 𝑦𝐵 𝐹 = { ⟨ 𝐴 , 𝑦 ⟩ } ) )
8 elex ( 𝐹X 𝑥 ∈ { 𝑧 } 𝐵𝐹 ∈ V )
9 snex { ⟨ 𝑧 , 𝑦 ⟩ } ∈ V
10 eleq1 ( 𝐹 = { ⟨ 𝑧 , 𝑦 ⟩ } → ( 𝐹 ∈ V ↔ { ⟨ 𝑧 , 𝑦 ⟩ } ∈ V ) )
11 9 10 mpbiri ( 𝐹 = { ⟨ 𝑧 , 𝑦 ⟩ } → 𝐹 ∈ V )
12 11 rexlimivw ( ∃ 𝑦𝐵 𝐹 = { ⟨ 𝑧 , 𝑦 ⟩ } → 𝐹 ∈ V )
13 eleq1 ( 𝑤 = 𝐹 → ( 𝑤X 𝑥 ∈ { 𝑧 } 𝐵𝐹X 𝑥 ∈ { 𝑧 } 𝐵 ) )
14 eqeq1 ( 𝑤 = 𝐹 → ( 𝑤 = { ⟨ 𝑧 , 𝑦 ⟩ } ↔ 𝐹 = { ⟨ 𝑧 , 𝑦 ⟩ } ) )
15 14 rexbidv ( 𝑤 = 𝐹 → ( ∃ 𝑦𝐵 𝑤 = { ⟨ 𝑧 , 𝑦 ⟩ } ↔ ∃ 𝑦𝐵 𝐹 = { ⟨ 𝑧 , 𝑦 ⟩ } ) )
16 vex 𝑤 ∈ V
17 16 elixp ( 𝑤X 𝑥 ∈ { 𝑧 } 𝐵 ↔ ( 𝑤 Fn { 𝑧 } ∧ ∀ 𝑥 ∈ { 𝑧 } ( 𝑤𝑥 ) ∈ 𝐵 ) )
18 vex 𝑧 ∈ V
19 fveq2 ( 𝑥 = 𝑧 → ( 𝑤𝑥 ) = ( 𝑤𝑧 ) )
20 19 eleq1d ( 𝑥 = 𝑧 → ( ( 𝑤𝑥 ) ∈ 𝐵 ↔ ( 𝑤𝑧 ) ∈ 𝐵 ) )
21 18 20 ralsn ( ∀ 𝑥 ∈ { 𝑧 } ( 𝑤𝑥 ) ∈ 𝐵 ↔ ( 𝑤𝑧 ) ∈ 𝐵 )
22 21 anbi2i ( ( 𝑤 Fn { 𝑧 } ∧ ∀ 𝑥 ∈ { 𝑧 } ( 𝑤𝑥 ) ∈ 𝐵 ) ↔ ( 𝑤 Fn { 𝑧 } ∧ ( 𝑤𝑧 ) ∈ 𝐵 ) )
23 simpl ( ( 𝑤 Fn { 𝑧 } ∧ ( 𝑤𝑧 ) ∈ 𝐵 ) → 𝑤 Fn { 𝑧 } )
24 fveq2 ( 𝑦 = 𝑧 → ( 𝑤𝑦 ) = ( 𝑤𝑧 ) )
25 24 eleq1d ( 𝑦 = 𝑧 → ( ( 𝑤𝑦 ) ∈ 𝐵 ↔ ( 𝑤𝑧 ) ∈ 𝐵 ) )
26 18 25 ralsn ( ∀ 𝑦 ∈ { 𝑧 } ( 𝑤𝑦 ) ∈ 𝐵 ↔ ( 𝑤𝑧 ) ∈ 𝐵 )
27 26 biimpri ( ( 𝑤𝑧 ) ∈ 𝐵 → ∀ 𝑦 ∈ { 𝑧 } ( 𝑤𝑦 ) ∈ 𝐵 )
28 27 adantl ( ( 𝑤 Fn { 𝑧 } ∧ ( 𝑤𝑧 ) ∈ 𝐵 ) → ∀ 𝑦 ∈ { 𝑧 } ( 𝑤𝑦 ) ∈ 𝐵 )
29 ffnfv ( 𝑤 : { 𝑧 } ⟶ 𝐵 ↔ ( 𝑤 Fn { 𝑧 } ∧ ∀ 𝑦 ∈ { 𝑧 } ( 𝑤𝑦 ) ∈ 𝐵 ) )
30 23 28 29 sylanbrc ( ( 𝑤 Fn { 𝑧 } ∧ ( 𝑤𝑧 ) ∈ 𝐵 ) → 𝑤 : { 𝑧 } ⟶ 𝐵 )
31 18 fsn2 ( 𝑤 : { 𝑧 } ⟶ 𝐵 ↔ ( ( 𝑤𝑧 ) ∈ 𝐵𝑤 = { ⟨ 𝑧 , ( 𝑤𝑧 ) ⟩ } ) )
32 30 31 sylib ( ( 𝑤 Fn { 𝑧 } ∧ ( 𝑤𝑧 ) ∈ 𝐵 ) → ( ( 𝑤𝑧 ) ∈ 𝐵𝑤 = { ⟨ 𝑧 , ( 𝑤𝑧 ) ⟩ } ) )
33 opeq2 ( 𝑦 = ( 𝑤𝑧 ) → ⟨ 𝑧 , 𝑦 ⟩ = ⟨ 𝑧 , ( 𝑤𝑧 ) ⟩ )
34 33 sneqd ( 𝑦 = ( 𝑤𝑧 ) → { ⟨ 𝑧 , 𝑦 ⟩ } = { ⟨ 𝑧 , ( 𝑤𝑧 ) ⟩ } )
35 34 rspceeqv ( ( ( 𝑤𝑧 ) ∈ 𝐵𝑤 = { ⟨ 𝑧 , ( 𝑤𝑧 ) ⟩ } ) → ∃ 𝑦𝐵 𝑤 = { ⟨ 𝑧 , 𝑦 ⟩ } )
36 32 35 syl ( ( 𝑤 Fn { 𝑧 } ∧ ( 𝑤𝑧 ) ∈ 𝐵 ) → ∃ 𝑦𝐵 𝑤 = { ⟨ 𝑧 , 𝑦 ⟩ } )
37 vex 𝑦 ∈ V
38 18 37 fvsn ( { ⟨ 𝑧 , 𝑦 ⟩ } ‘ 𝑧 ) = 𝑦
39 id ( 𝑦𝐵𝑦𝐵 )
40 38 39 eqeltrid ( 𝑦𝐵 → ( { ⟨ 𝑧 , 𝑦 ⟩ } ‘ 𝑧 ) ∈ 𝐵 )
41 18 37 fnsn { ⟨ 𝑧 , 𝑦 ⟩ } Fn { 𝑧 }
42 40 41 jctil ( 𝑦𝐵 → ( { ⟨ 𝑧 , 𝑦 ⟩ } Fn { 𝑧 } ∧ ( { ⟨ 𝑧 , 𝑦 ⟩ } ‘ 𝑧 ) ∈ 𝐵 ) )
43 fneq1 ( 𝑤 = { ⟨ 𝑧 , 𝑦 ⟩ } → ( 𝑤 Fn { 𝑧 } ↔ { ⟨ 𝑧 , 𝑦 ⟩ } Fn { 𝑧 } ) )
44 fveq1 ( 𝑤 = { ⟨ 𝑧 , 𝑦 ⟩ } → ( 𝑤𝑧 ) = ( { ⟨ 𝑧 , 𝑦 ⟩ } ‘ 𝑧 ) )
45 44 eleq1d ( 𝑤 = { ⟨ 𝑧 , 𝑦 ⟩ } → ( ( 𝑤𝑧 ) ∈ 𝐵 ↔ ( { ⟨ 𝑧 , 𝑦 ⟩ } ‘ 𝑧 ) ∈ 𝐵 ) )
46 43 45 anbi12d ( 𝑤 = { ⟨ 𝑧 , 𝑦 ⟩ } → ( ( 𝑤 Fn { 𝑧 } ∧ ( 𝑤𝑧 ) ∈ 𝐵 ) ↔ ( { ⟨ 𝑧 , 𝑦 ⟩ } Fn { 𝑧 } ∧ ( { ⟨ 𝑧 , 𝑦 ⟩ } ‘ 𝑧 ) ∈ 𝐵 ) ) )
47 42 46 syl5ibrcom ( 𝑦𝐵 → ( 𝑤 = { ⟨ 𝑧 , 𝑦 ⟩ } → ( 𝑤 Fn { 𝑧 } ∧ ( 𝑤𝑧 ) ∈ 𝐵 ) ) )
48 47 rexlimiv ( ∃ 𝑦𝐵 𝑤 = { ⟨ 𝑧 , 𝑦 ⟩ } → ( 𝑤 Fn { 𝑧 } ∧ ( 𝑤𝑧 ) ∈ 𝐵 ) )
49 36 48 impbii ( ( 𝑤 Fn { 𝑧 } ∧ ( 𝑤𝑧 ) ∈ 𝐵 ) ↔ ∃ 𝑦𝐵 𝑤 = { ⟨ 𝑧 , 𝑦 ⟩ } )
50 17 22 49 3bitri ( 𝑤X 𝑥 ∈ { 𝑧 } 𝐵 ↔ ∃ 𝑦𝐵 𝑤 = { ⟨ 𝑧 , 𝑦 ⟩ } )
51 13 15 50 vtoclbg ( 𝐹 ∈ V → ( 𝐹X 𝑥 ∈ { 𝑧 } 𝐵 ↔ ∃ 𝑦𝐵 𝐹 = { ⟨ 𝑧 , 𝑦 ⟩ } ) )
52 8 12 51 pm5.21nii ( 𝐹X 𝑥 ∈ { 𝑧 } 𝐵 ↔ ∃ 𝑦𝐵 𝐹 = { ⟨ 𝑧 , 𝑦 ⟩ } )
53 3 7 52 vtoclbg ( 𝐴𝑉 → ( 𝐹X 𝑥 ∈ { 𝐴 } 𝐵 ↔ ∃ 𝑦𝐵 𝐹 = { ⟨ 𝐴 , 𝑦 ⟩ } ) )