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	bilanri	⊢ ( ( 𝑤 Fn { 𝑧 } ∧ ( 𝑤 ‘ 𝑧 ) ∈ 𝐵 ) → ∀ 𝑦 ∈ { 𝑧 } ( 𝑤 ‘ 𝑦 ) ∈ 𝐵 )
28		ffnfv	⊢ ( 𝑤 : { 𝑧 } ⟶ 𝐵 ↔ ( 𝑤 Fn { 𝑧 } ∧ ∀ 𝑦 ∈ { 𝑧 } ( 𝑤 ‘ 𝑦 ) ∈ 𝐵 ) )
29	23 27 28	sylanbrc	⊢ ( ( 𝑤 Fn { 𝑧 } ∧ ( 𝑤 ‘ 𝑧 ) ∈ 𝐵 ) → 𝑤 : { 𝑧 } ⟶ 𝐵 )
30	18	fsn2	⊢ ( 𝑤 : { 𝑧 } ⟶ 𝐵 ↔ ( ( 𝑤 ‘ 𝑧 ) ∈ 𝐵 ∧ 𝑤 = { ⟨ 𝑧 , ( 𝑤 ‘ 𝑧 ) ⟩ } ) )
31	29 30	sylib	⊢ ( ( 𝑤 Fn { 𝑧 } ∧ ( 𝑤 ‘ 𝑧 ) ∈ 𝐵 ) → ( ( 𝑤 ‘ 𝑧 ) ∈ 𝐵 ∧ 𝑤 = { ⟨ 𝑧 , ( 𝑤 ‘ 𝑧 ) ⟩ } ) )
32		opeq2	⊢ ( 𝑦 = ( 𝑤 ‘ 𝑧 ) → ⟨ 𝑧 , 𝑦 ⟩ = ⟨ 𝑧 , ( 𝑤 ‘ 𝑧 ) ⟩ )
33	32	sneqd	⊢ ( 𝑦 = ( 𝑤 ‘ 𝑧 ) → { ⟨ 𝑧 , 𝑦 ⟩ } = { ⟨ 𝑧 , ( 𝑤 ‘ 𝑧 ) ⟩ } )
34	33	rspceeqv	⊢ ( ( ( 𝑤 ‘ 𝑧 ) ∈ 𝐵 ∧ 𝑤 = { ⟨ 𝑧 , ( 𝑤 ‘ 𝑧 ) ⟩ } ) → ∃ 𝑦 ∈ 𝐵 𝑤 = { ⟨ 𝑧 , 𝑦 ⟩ } )
35	31 34	syl	⊢ ( ( 𝑤 Fn { 𝑧 } ∧ ( 𝑤 ‘ 𝑧 ) ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐵 𝑤 = { ⟨ 𝑧 , 𝑦 ⟩ } )
36		vex	⊢ 𝑦 ∈ V
37	18 36	fvsn	⊢ ( { ⟨ 𝑧 , 𝑦 ⟩ } ‘ 𝑧 ) = 𝑦
38		id	⊢ ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐵 )
39	37 38	eqeltrid	⊢ ( 𝑦 ∈ 𝐵 → ( { ⟨ 𝑧 , 𝑦 ⟩ } ‘ 𝑧 ) ∈ 𝐵 )
40	18 36	fnsn	⊢ { ⟨ 𝑧 , 𝑦 ⟩ } Fn { 𝑧 }
41	39 40	jctil	⊢ ( 𝑦 ∈ 𝐵 → ( { ⟨ 𝑧 , 𝑦 ⟩ } Fn { 𝑧 } ∧ ( { ⟨ 𝑧 , 𝑦 ⟩ } ‘ 𝑧 ) ∈ 𝐵 ) )
42		fneq1	⊢ ( 𝑤 = { ⟨ 𝑧 , 𝑦 ⟩ } → ( 𝑤 Fn { 𝑧 } ↔ { ⟨ 𝑧 , 𝑦 ⟩ } Fn { 𝑧 } ) )
43		fveq1	⊢ ( 𝑤 = { ⟨ 𝑧 , 𝑦 ⟩ } → ( 𝑤 ‘ 𝑧 ) = ( { ⟨ 𝑧 , 𝑦 ⟩ } ‘ 𝑧 ) )
44	43	eleq1d	⊢ ( 𝑤 = { ⟨ 𝑧 , 𝑦 ⟩ } → ( ( 𝑤 ‘ 𝑧 ) ∈ 𝐵 ↔ ( { ⟨ 𝑧 , 𝑦 ⟩ } ‘ 𝑧 ) ∈ 𝐵 ) )
45	42 44	anbi12d	⊢ ( 𝑤 = { ⟨ 𝑧 , 𝑦 ⟩ } → ( ( 𝑤 Fn { 𝑧 } ∧ ( 𝑤 ‘ 𝑧 ) ∈ 𝐵 ) ↔ ( { ⟨ 𝑧 , 𝑦 ⟩ } Fn { 𝑧 } ∧ ( { ⟨ 𝑧 , 𝑦 ⟩ } ‘ 𝑧 ) ∈ 𝐵 ) ) )
46	41 45	syl5ibrcom	⊢ ( 𝑦 ∈ 𝐵 → ( 𝑤 = { ⟨ 𝑧 , 𝑦 ⟩ } → ( 𝑤 Fn { 𝑧 } ∧ ( 𝑤 ‘ 𝑧 ) ∈ 𝐵 ) ) )
47	46	rexlimiv	⊢ ( ∃ 𝑦 ∈ 𝐵 𝑤 = { ⟨ 𝑧 , 𝑦 ⟩ } → ( 𝑤 Fn { 𝑧 } ∧ ( 𝑤 ‘ 𝑧 ) ∈ 𝐵 ) )
48	35 47	impbii	⊢ ( ( 𝑤 Fn { 𝑧 } ∧ ( 𝑤 ‘ 𝑧 ) ∈ 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐵 𝑤 = { ⟨ 𝑧 , 𝑦 ⟩ } )
49	17 22 48	3bitri	⊢ ( 𝑤 ∈ X 𝑥 ∈ { 𝑧 } 𝐵 ↔ ∃ 𝑦 ∈ 𝐵 𝑤 = { ⟨ 𝑧 , 𝑦 ⟩ } )
50	13 15 49	vtoclbg	⊢ ( 𝐹 ∈ V → ( 𝐹 ∈ X 𝑥 ∈ { 𝑧 } 𝐵 ↔ ∃ 𝑦 ∈ 𝐵 𝐹 = { ⟨ 𝑧 , 𝑦 ⟩ } ) )
51	8 12 50	pm5.21nii	⊢ ( 𝐹 ∈ X 𝑥 ∈ { 𝑧 } 𝐵 ↔ ∃ 𝑦 ∈ 𝐵 𝐹 = { ⟨ 𝑧 , 𝑦 ⟩ } )
52	3 7 51	vtoclbg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 ∈ X 𝑥 ∈ { 𝐴 } 𝐵 ↔ ∃ 𝑦 ∈ 𝐵 𝐹 = { ⟨ 𝐴 , 𝑦 ⟩ } ) )