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