Theorem ixpsnf1o

Description: A bijection between a class and single-point functions to it. (Contributed by Stefan O'Rear, 24-Jan-2015)

	Ref	Expression
Hypothesis	ixpsnf1o.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( { 𝐼 } × { 𝑥 } ) )
Assertion	ixpsnf1o	⊢ ( 𝐼 ∈ 𝑉 → 𝐹 : 𝐴 –1-1-onto→ X 𝑦 ∈ { 𝐼 } 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ixpsnf1o.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( { 𝐼 } × { 𝑥 } ) )
2		snex	⊢ { 𝐼 } ∈ V
3		snex	⊢ { 𝑥 } ∈ V
4	2 3	xpex	⊢ ( { 𝐼 } × { 𝑥 } ) ∈ V
5	4	a1i	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝐴 ) → ( { 𝐼 } × { 𝑥 } ) ∈ V )
6		vex	⊢ 𝑎 ∈ V
7	6	rnex	⊢ ran 𝑎 ∈ V
8	7	uniex	⊢ ∪ ran 𝑎 ∈ V
9	8	a1i	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑎 ∈ X 𝑦 ∈ { 𝐼 } 𝐴 ) → ∪ ran 𝑎 ∈ V )
10		sneq	⊢ ( 𝑏 = 𝐼 → { 𝑏 } = { 𝐼 } )
11	10	xpeq1d	⊢ ( 𝑏 = 𝐼 → ( { 𝑏 } × { 𝑥 } ) = ( { 𝐼 } × { 𝑥 } ) )
12	11	eqeq2d	⊢ ( 𝑏 = 𝐼 → ( 𝑎 = ( { 𝑏 } × { 𝑥 } ) ↔ 𝑎 = ( { 𝐼 } × { 𝑥 } ) ) )
13	12	anbi2d	⊢ ( 𝑏 = 𝐼 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑎 = ( { 𝑏 } × { 𝑥 } ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑎 = ( { 𝐼 } × { 𝑥 } ) ) ) )
14		elixpsn	⊢ ( 𝑏 ∈ V → ( 𝑎 ∈ X 𝑦 ∈ { 𝑏 } 𝐴 ↔ ∃ 𝑐 ∈ 𝐴 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } ) )
15	14	elv	⊢ ( 𝑎 ∈ X 𝑦 ∈ { 𝑏 } 𝐴 ↔ ∃ 𝑐 ∈ 𝐴 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } )
16	10	ixpeq1d	⊢ ( 𝑏 = 𝐼 → X 𝑦 ∈ { 𝑏 } 𝐴 = X 𝑦 ∈ { 𝐼 } 𝐴 )
17	16	eleq2d	⊢ ( 𝑏 = 𝐼 → ( 𝑎 ∈ X 𝑦 ∈ { 𝑏 } 𝐴 ↔ 𝑎 ∈ X 𝑦 ∈ { 𝐼 } 𝐴 ) )
18	15 17	bitr3id	⊢ ( 𝑏 = 𝐼 → ( ∃ 𝑐 ∈ 𝐴 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } ↔ 𝑎 ∈ X 𝑦 ∈ { 𝐼 } 𝐴 ) )
19	18	anbi1d	⊢ ( 𝑏 = 𝐼 → ( ( ∃ 𝑐 ∈ 𝐴 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } ∧ 𝑥 = ∪ ran 𝑎 ) ↔ ( 𝑎 ∈ X 𝑦 ∈ { 𝐼 } 𝐴 ∧ 𝑥 = ∪ ran 𝑎 ) ) )
20		vex	⊢ 𝑏 ∈ V
21		vex	⊢ 𝑥 ∈ V
22	20 21	xpsn	⊢ ( { 𝑏 } × { 𝑥 } ) = { ⟨ 𝑏 , 𝑥 ⟩ }
23	22	eqeq2i	⊢ ( 𝑎 = ( { 𝑏 } × { 𝑥 } ) ↔ 𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } )
24	23	anbi2i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑎 = ( { 𝑏 } × { 𝑥 } ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } ) )
25		eqid	⊢ { ⟨ 𝑏 , 𝑥 ⟩ } = { ⟨ 𝑏 , 𝑥 ⟩ }
26		opeq2	⊢ ( 𝑐 = 𝑥 → ⟨ 𝑏 , 𝑐 ⟩ = ⟨ 𝑏 , 𝑥 ⟩ )
27	26	sneqd	⊢ ( 𝑐 = 𝑥 → { ⟨ 𝑏 , 𝑐 ⟩ } = { ⟨ 𝑏 , 𝑥 ⟩ } )
28	27	rspceeqv	⊢ ( ( 𝑥 ∈ 𝐴 ∧ { ⟨ 𝑏 , 𝑥 ⟩ } = { ⟨ 𝑏 , 𝑥 ⟩ } ) → ∃ 𝑐 ∈ 𝐴 { ⟨ 𝑏 , 𝑥 ⟩ } = { ⟨ 𝑏 , 𝑐 ⟩ } )
29	25 28	mpan2	⊢ ( 𝑥 ∈ 𝐴 → ∃ 𝑐 ∈ 𝐴 { ⟨ 𝑏 , 𝑥 ⟩ } = { ⟨ 𝑏 , 𝑐 ⟩ } )
30	20 21	op2nda	⊢ ∪ ran { ⟨ 𝑏 , 𝑥 ⟩ } = 𝑥
31	30	eqcomi	⊢ 𝑥 = ∪ ran { ⟨ 𝑏 , 𝑥 ⟩ }
32	29 31	jctir	⊢ ( 𝑥 ∈ 𝐴 → ( ∃ 𝑐 ∈ 𝐴 { ⟨ 𝑏 , 𝑥 ⟩ } = { ⟨ 𝑏 , 𝑐 ⟩ } ∧ 𝑥 = ∪ ran { ⟨ 𝑏 , 𝑥 ⟩ } ) )
33		eqeq1	⊢ ( 𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } → ( 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } ↔ { ⟨ 𝑏 , 𝑥 ⟩ } = { ⟨ 𝑏 , 𝑐 ⟩ } ) )
34	33	rexbidv	⊢ ( 𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } → ( ∃ 𝑐 ∈ 𝐴 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } ↔ ∃ 𝑐 ∈ 𝐴 { ⟨ 𝑏 , 𝑥 ⟩ } = { ⟨ 𝑏 , 𝑐 ⟩ } ) )
35		rneq	⊢ ( 𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } → ran 𝑎 = ran { ⟨ 𝑏 , 𝑥 ⟩ } )
36	35	unieqd	⊢ ( 𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } → ∪ ran 𝑎 = ∪ ran { ⟨ 𝑏 , 𝑥 ⟩ } )
37	36	eqeq2d	⊢ ( 𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } → ( 𝑥 = ∪ ran 𝑎 ↔ 𝑥 = ∪ ran { ⟨ 𝑏 , 𝑥 ⟩ } ) )
38	34 37	anbi12d	⊢ ( 𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } → ( ( ∃ 𝑐 ∈ 𝐴 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } ∧ 𝑥 = ∪ ran 𝑎 ) ↔ ( ∃ 𝑐 ∈ 𝐴 { ⟨ 𝑏 , 𝑥 ⟩ } = { ⟨ 𝑏 , 𝑐 ⟩ } ∧ 𝑥 = ∪ ran { ⟨ 𝑏 , 𝑥 ⟩ } ) ) )
39	32 38	syl5ibrcom	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } → ( ∃ 𝑐 ∈ 𝐴 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } ∧ 𝑥 = ∪ ran 𝑎 ) ) )
40	39	imp	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } ) → ( ∃ 𝑐 ∈ 𝐴 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } ∧ 𝑥 = ∪ ran 𝑎 ) )
41		vex	⊢ 𝑐 ∈ V
42	20 41	op2nda	⊢ ∪ ran { ⟨ 𝑏 , 𝑐 ⟩ } = 𝑐
43	42	eqeq2i	⊢ ( 𝑥 = ∪ ran { ⟨ 𝑏 , 𝑐 ⟩ } ↔ 𝑥 = 𝑐 )
44		eqidd	⊢ ( 𝑐 ∈ 𝐴 → { ⟨ 𝑏 , 𝑐 ⟩ } = { ⟨ 𝑏 , 𝑐 ⟩ } )
45	44	ancli	⊢ ( 𝑐 ∈ 𝐴 → ( 𝑐 ∈ 𝐴 ∧ { ⟨ 𝑏 , 𝑐 ⟩ } = { ⟨ 𝑏 , 𝑐 ⟩ } ) )
46		eleq1w	⊢ ( 𝑥 = 𝑐 → ( 𝑥 ∈ 𝐴 ↔ 𝑐 ∈ 𝐴 ) )
47		opeq2	⊢ ( 𝑥 = 𝑐 → ⟨ 𝑏 , 𝑥 ⟩ = ⟨ 𝑏 , 𝑐 ⟩ )
48	47	sneqd	⊢ ( 𝑥 = 𝑐 → { ⟨ 𝑏 , 𝑥 ⟩ } = { ⟨ 𝑏 , 𝑐 ⟩ } )
49	48	eqeq2d	⊢ ( 𝑥 = 𝑐 → ( { ⟨ 𝑏 , 𝑐 ⟩ } = { ⟨ 𝑏 , 𝑥 ⟩ } ↔ { ⟨ 𝑏 , 𝑐 ⟩ } = { ⟨ 𝑏 , 𝑐 ⟩ } ) )
50	46 49	anbi12d	⊢ ( 𝑥 = 𝑐 → ( ( 𝑥 ∈ 𝐴 ∧ { ⟨ 𝑏 , 𝑐 ⟩ } = { ⟨ 𝑏 , 𝑥 ⟩ } ) ↔ ( 𝑐 ∈ 𝐴 ∧ { ⟨ 𝑏 , 𝑐 ⟩ } = { ⟨ 𝑏 , 𝑐 ⟩ } ) ) )
51	45 50	syl5ibrcom	⊢ ( 𝑐 ∈ 𝐴 → ( 𝑥 = 𝑐 → ( 𝑥 ∈ 𝐴 ∧ { ⟨ 𝑏 , 𝑐 ⟩ } = { ⟨ 𝑏 , 𝑥 ⟩ } ) ) )
52	43 51	syl5bi	⊢ ( 𝑐 ∈ 𝐴 → ( 𝑥 = ∪ ran { ⟨ 𝑏 , 𝑐 ⟩ } → ( 𝑥 ∈ 𝐴 ∧ { ⟨ 𝑏 , 𝑐 ⟩ } = { ⟨ 𝑏 , 𝑥 ⟩ } ) ) )
53		rneq	⊢ ( 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } → ran 𝑎 = ran { ⟨ 𝑏 , 𝑐 ⟩ } )
54	53	unieqd	⊢ ( 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } → ∪ ran 𝑎 = ∪ ran { ⟨ 𝑏 , 𝑐 ⟩ } )
55	54	eqeq2d	⊢ ( 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } → ( 𝑥 = ∪ ran 𝑎 ↔ 𝑥 = ∪ ran { ⟨ 𝑏 , 𝑐 ⟩ } ) )
56		eqeq1	⊢ ( 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } → ( 𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } ↔ { ⟨ 𝑏 , 𝑐 ⟩ } = { ⟨ 𝑏 , 𝑥 ⟩ } ) )
57	56	anbi2d	⊢ ( 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } → ( ( 𝑥 ∈ 𝐴 ∧ 𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } ) ↔ ( 𝑥 ∈ 𝐴 ∧ { ⟨ 𝑏 , 𝑐 ⟩ } = { ⟨ 𝑏 , 𝑥 ⟩ } ) ) )
58	55 57	imbi12d	⊢ ( 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } → ( ( 𝑥 = ∪ ran 𝑎 → ( 𝑥 ∈ 𝐴 ∧ 𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } ) ) ↔ ( 𝑥 = ∪ ran { ⟨ 𝑏 , 𝑐 ⟩ } → ( 𝑥 ∈ 𝐴 ∧ { ⟨ 𝑏 , 𝑐 ⟩ } = { ⟨ 𝑏 , 𝑥 ⟩ } ) ) ) )
59	52 58	syl5ibrcom	⊢ ( 𝑐 ∈ 𝐴 → ( 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } → ( 𝑥 = ∪ ran 𝑎 → ( 𝑥 ∈ 𝐴 ∧ 𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } ) ) ) )
60	59	rexlimiv	⊢ ( ∃ 𝑐 ∈ 𝐴 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } → ( 𝑥 = ∪ ran 𝑎 → ( 𝑥 ∈ 𝐴 ∧ 𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } ) ) )
61	60	imp	⊢ ( ( ∃ 𝑐 ∈ 𝐴 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } ∧ 𝑥 = ∪ ran 𝑎 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } ) )
62	40 61	impbii	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑎 = { ⟨ 𝑏 , 𝑥 ⟩ } ) ↔ ( ∃ 𝑐 ∈ 𝐴 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } ∧ 𝑥 = ∪ ran 𝑎 ) )
63	24 62	bitri	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑎 = ( { 𝑏 } × { 𝑥 } ) ) ↔ ( ∃ 𝑐 ∈ 𝐴 𝑎 = { ⟨ 𝑏 , 𝑐 ⟩ } ∧ 𝑥 = ∪ ran 𝑎 ) )
64	13 19 63	vtoclbg	⊢ ( 𝐼 ∈ 𝑉 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑎 = ( { 𝐼 } × { 𝑥 } ) ) ↔ ( 𝑎 ∈ X 𝑦 ∈ { 𝐼 } 𝐴 ∧ 𝑥 = ∪ ran 𝑎 ) ) )
65	1 5 9 64	f1od	⊢ ( 𝐼 ∈ 𝑉 → 𝐹 : 𝐴 –1-1-onto→ X 𝑦 ∈ { 𝐼 } 𝐴 )