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	$⊢ F = (x \in A ⟼ \{I\} \times \{x\})$
	Assertion	ixpsnf1o	$⊢ I \in V \to F : A \underset{1-1 onto}{⟶} \underset{y \in \{I\}}{⨉} A$

Proof

Step	Hyp	Ref	Expression
1		ixpsnf1o.f	$⊢ F = (x \in A ⟼ \{I\} \times \{x\})$
2		snex	$⊢ \{I\} \in V$
3		snex	$⊢ \{x\} \in V$
4	2 3	xpex	$⊢ \{I\} \times \{x\} \in V$
5	4	a1i	$⊢ (I \in V \land x \in A) \to \{I\} \times \{x\} \in V$
6		vex	$⊢ a \in V$
7	6	rnex	$⊢ ran a \in V$
8	7	uniex	$⊢ ⋃ ran a \in V$
9	8	a1i	$⊢ (I \in V \land a \in \underset{y \in \{I\}}{⨉} A) \to ⋃ ran a \in V$
10		sneq	$⊢ b = I \to \{b\} = \{I\}$
11	10	xpeq1d	$⊢ b = I \to \{b\} \times \{x\} = \{I\} \times \{x\}$
12	11	eqeq2d	$⊢ b = I \to (a = \{b\} \times \{x\} \leftrightarrow a = \{I\} \times \{x\})$
13	12	anbi2d	$⊢ b = I \to ((x \in A \land a = \{b\} \times \{x\}) \leftrightarrow (x \in A \land a = \{I\} \times \{x\}))$
14		elixpsn	$⊢ b \in V \to (a \in \underset{y \in \{b\}}{⨉} A \leftrightarrow \exists c \in A a = \{⟨b, c⟩\})$
15	14	elv	$⊢ a \in \underset{y \in \{b\}}{⨉} A \leftrightarrow \exists c \in A a = \{⟨b, c⟩\}$
16	10	ixpeq1d	$⊢ b = I \to \underset{y \in \{b\}}{⨉} A = \underset{y \in \{I\}}{⨉} A$
17	16	eleq2d	$⊢ b = I \to (a \in \underset{y \in \{b\}}{⨉} A \leftrightarrow a \in \underset{y \in \{I\}}{⨉} A)$
18	15 17	bitr3id	$⊢ b = I \to (\exists c \in A a = \{⟨b, c⟩\} \leftrightarrow a \in \underset{y \in \{I\}}{⨉} A)$
19	18	anbi1d	$⊢ b = I \to ((\exists c \in A a = \{⟨b, c⟩\} \land x = ⋃ ran a) \leftrightarrow (a \in \underset{y \in \{I\}}{⨉} A \land x = ⋃ ran a))$
20		vex	$⊢ b \in V$
21		vex	$⊢ x \in V$
22	20 21	xpsn	$⊢ \{b\} \times \{x\} = \{⟨b, x⟩\}$
23	22	eqeq2i	$⊢ a = \{b\} \times \{x\} \leftrightarrow a = \{⟨b, x⟩\}$
24	23	anbi2i	$⊢ (x \in A \land a = \{b\} \times \{x\}) \leftrightarrow (x \in A \land a = \{⟨b, x⟩\})$
25		eqid	$⊢ \{⟨b, x⟩\} = \{⟨b, x⟩\}$
26		opeq2	$⊢ c = x \to ⟨b, c⟩ = ⟨b, x⟩$
27	26	sneqd	$⊢ c = x \to \{⟨b, c⟩\} = \{⟨b, x⟩\}$
28	27	rspceeqv	$⊢ (x \in A \land \{⟨b, x⟩\} = \{⟨b, x⟩\}) \to \exists c \in A \{⟨b, x⟩\} = \{⟨b, c⟩\}$
29	25 28	mpan2	$⊢ x \in A \to \exists c \in A \{⟨b, x⟩\} = \{⟨b, c⟩\}$
30	20 21	op2nda	$⊢ ⋃ ran \{⟨b, x⟩\} = x$
31	30	eqcomi	$⊢ x = ⋃ ran \{⟨b, x⟩\}$
32	29 31	jctir	$⊢ x \in A \to (\exists c \in A \{⟨b, x⟩\} = \{⟨b, c⟩\} \land x = ⋃ ran \{⟨b, x⟩\})$
33		eqeq1	$⊢ a = \{⟨b, x⟩\} \to (a = \{⟨b, c⟩\} \leftrightarrow \{⟨b, x⟩\} = \{⟨b, c⟩\})$
34	33	rexbidv	$⊢ a = \{⟨b, x⟩\} \to (\exists c \in A a = \{⟨b, c⟩\} \leftrightarrow \exists c \in A \{⟨b, x⟩\} = \{⟨b, c⟩\})$
35		rneq	$⊢ a = \{⟨b, x⟩\} \to ran a = ran \{⟨b, x⟩\}$
36	35	unieqd	$⊢ a = \{⟨b, x⟩\} \to ⋃ ran a = ⋃ ran \{⟨b, x⟩\}$
37	36	eqeq2d	$⊢ a = \{⟨b, x⟩\} \to (x = ⋃ ran a \leftrightarrow x = ⋃ ran \{⟨b, x⟩\})$
38	34 37	anbi12d	$⊢ a = \{⟨b, x⟩\} \to ((\exists c \in A a = \{⟨b, c⟩\} \land x = ⋃ ran a) \leftrightarrow (\exists c \in A \{⟨b, x⟩\} = \{⟨b, c⟩\} \land x = ⋃ ran \{⟨b, x⟩\}))$
39	32 38	syl5ibrcom	$⊢ x \in A \to (a = \{⟨b, x⟩\} \to (\exists c \in A a = \{⟨b, c⟩\} \land x = ⋃ ran a))$
40	39	imp	$⊢ (x \in A \land a = \{⟨b, x⟩\}) \to (\exists c \in A a = \{⟨b, c⟩\} \land x = ⋃ ran a)$
41		vex	$⊢ c \in V$
42	20 41	op2nda	$⊢ ⋃ ran \{⟨b, c⟩\} = c$
43	42	eqeq2i	$⊢ x = ⋃ ran \{⟨b, c⟩\} \leftrightarrow x = c$
44		eqidd	$⊢ c \in A \to \{⟨b, c⟩\} = \{⟨b, c⟩\}$
45	44	ancli	$⊢ c \in A \to (c \in A \land \{⟨b, c⟩\} = \{⟨b, c⟩\})$
46		eleq1w	$⊢ x = c \to (x \in A \leftrightarrow c \in A)$
47		opeq2	$⊢ x = c \to ⟨b, x⟩ = ⟨b, c⟩$
48	47	sneqd	$⊢ x = c \to \{⟨b, x⟩\} = \{⟨b, c⟩\}$
49	48	eqeq2d	$⊢ x = c \to (\{⟨b, c⟩\} = \{⟨b, x⟩\} \leftrightarrow \{⟨b, c⟩\} = \{⟨b, c⟩\})$
50	46 49	anbi12d	$⊢ x = c \to ((x \in A \land \{⟨b, c⟩\} = \{⟨b, x⟩\}) \leftrightarrow (c \in A \land \{⟨b, c⟩\} = \{⟨b, c⟩\}))$
51	45 50	syl5ibrcom	$⊢ c \in A \to (x = c \to (x \in A \land \{⟨b, c⟩\} = \{⟨b, x⟩\}))$
52	43 51	biimtrid	$⊢ c \in A \to (x = ⋃ ran \{⟨b, c⟩\} \to (x \in A \land \{⟨b, c⟩\} = \{⟨b, x⟩\}))$
53		rneq	$⊢ a = \{⟨b, c⟩\} \to ran a = ran \{⟨b, c⟩\}$
54	53	unieqd	$⊢ a = \{⟨b, c⟩\} \to ⋃ ran a = ⋃ ran \{⟨b, c⟩\}$
55	54	eqeq2d	$⊢ a = \{⟨b, c⟩\} \to (x = ⋃ ran a \leftrightarrow x = ⋃ ran \{⟨b, c⟩\})$
56		eqeq1	$⊢ a = \{⟨b, c⟩\} \to (a = \{⟨b, x⟩\} \leftrightarrow \{⟨b, c⟩\} = \{⟨b, x⟩\})$
57	56	anbi2d	$⊢ a = \{⟨b, c⟩\} \to ((x \in A \land a = \{⟨b, x⟩\}) \leftrightarrow (x \in A \land \{⟨b, c⟩\} = \{⟨b, x⟩\}))$
58	55 57	imbi12d	$⊢ a = \{⟨b, c⟩\} \to ((x = ⋃ ran a \to (x \in A \land a = \{⟨b, x⟩\})) \leftrightarrow (x = ⋃ ran \{⟨b, c⟩\} \to (x \in A \land \{⟨b, c⟩\} = \{⟨b, x⟩\})))$
59	52 58	syl5ibrcom	$⊢ c \in A \to (a = \{⟨b, c⟩\} \to (x = ⋃ ran a \to (x \in A \land a = \{⟨b, x⟩\})))$
60	59	rexlimiv	$⊢ \exists c \in A a = \{⟨b, c⟩\} \to (x = ⋃ ran a \to (x \in A \land a = \{⟨b, x⟩\}))$
61	60	imp	$⊢ (\exists c \in A a = \{⟨b, c⟩\} \land x = ⋃ ran a) \to (x \in A \land a = \{⟨b, x⟩\})$
62	40 61	impbii	$⊢ (x \in A \land a = \{⟨b, x⟩\}) \leftrightarrow (\exists c \in A a = \{⟨b, c⟩\} \land x = ⋃ ran a)$
63	24 62	bitri	$⊢ (x \in A \land a = \{b\} \times \{x\}) \leftrightarrow (\exists c \in A a = \{⟨b, c⟩\} \land x = ⋃ ran a)$
64	13 19 63	vtoclbg	$⊢ I \in V \to ((x \in A \land a = \{I\} \times \{x\}) \leftrightarrow (a \in \underset{y \in \{I\}}{⨉} A \land x = ⋃ ran a))$
65	1 5 9 64	f1od	$⊢ I \in V \to F : A \underset{1-1 onto}{⟶} \underset{y \in \{I\}}{⨉} A$

Metamath Proof Explorer

Theorem ixpsnf1o

Proof