This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝑥 ∈ { 𝐴 } 𝐵 ↔ ∃ 𝑦 ∈ 𝐵 𝐹 = { ⟨ 𝐴 , 𝑦 ⟩ } ) )