unirnmapsn

Description: Equality theorem for a subset of a set exponentiation, where the exponent is a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	unirnmapsn.A	$⊢ φ \to A \in V$
	unirnmapsn.b	$⊢ φ \to B \in W$
	unirnmapsn.C	$⊢ C = \{A\}$
	unirnmapsn.x	$⊢ φ \to X \subseteq B^{C}$
Assertion	unirnmapsn	$⊢ φ \to X = {ran ⋃ X}^{C}$

Proof

Step	Hyp	Ref	Expression
1		unirnmapsn.A	$⊢ φ \to A \in V$
2		unirnmapsn.b	$⊢ φ \to B \in W$
3		unirnmapsn.C	$⊢ C = \{A\}$
4		unirnmapsn.x	$⊢ φ \to X \subseteq B^{C}$
5		snex	$⊢ \{A\} \in V$
6	3 5	eqeltri	$⊢ C \in V$
7	6	a1i	$⊢ φ \to C \in V$
8	7 4	unirnmap	$⊢ φ \to X \subseteq {ran ⋃ X}^{C}$
9		simpl	$⊢ (φ \land g \in ({ran ⋃ X}^{C})) \to φ$
10		equid	$⊢ g = g$
11		rnuni	$⊢ ran ⋃ X = ⋃_{f \in X} ran f$
12	11	oveq1i	$⊢ {ran ⋃ X}^{C} = {⋃_{f \in X} ran f}^{C}$
13	10 12	eleq12i	$⊢ g \in ({ran ⋃ X}^{C}) \leftrightarrow g \in ({⋃_{f \in X} ran f}^{C})$
14	13	bilani	$⊢ (φ \land g \in ({ran ⋃ X}^{C})) \to g \in ({⋃_{f \in X} ran f}^{C})$
15		ovexd	$⊢ φ \to B^{C} \in V$
16	15 4	ssexd	$⊢ φ \to X \in V$
17		rnexg	$⊢ f \in X \to ran f \in V$
18	17	rgen	$⊢ \forall f \in X ran f \in V$
19	18	a1i	$⊢ φ \to \forall f \in X ran f \in V$
20		iunexg	$⊢ (X \in V \land \forall f \in X ran f \in V) \to ⋃_{f \in X} ran f \in V$
21	16 19 20	syl2anc	$⊢ φ \to ⋃_{f \in X} ran f \in V$
22	21 7	elmapd	$⊢ φ \to (g \in ({⋃_{f \in X} ran f}^{C}) \leftrightarrow g : C ⟶ ⋃_{f \in X} ran f)$
23	22	biimpa	$⊢ (φ \land g \in ({⋃_{f \in X} ran f}^{C})) \to g : C ⟶ ⋃_{f \in X} ran f$
24		snidg	$⊢ A \in V \to A \in \{A\}$
25	1 24	syl	$⊢ φ \to A \in \{A\}$
26	25 3	eleqtrrdi	$⊢ φ \to A \in C$
27	26	adantr	$⊢ (φ \land g \in ({⋃_{f \in X} ran f}^{C})) \to A \in C$
28	23 27	ffvelcdmd	$⊢ (φ \land g \in ({⋃_{f \in X} ran f}^{C})) \to g (A) \in ⋃_{f \in X} ran f$
29		eliun	$⊢ g (A) \in ⋃_{f \in X} ran f \leftrightarrow \exists f \in X g (A) \in ran f$
30	28 29	sylib	$⊢ (φ \land g \in ({⋃_{f \in X} ran f}^{C})) \to \exists f \in X g (A) \in ran f$
31	9 14 30	syl2anc	$⊢ (φ \land g \in ({ran ⋃ X}^{C})) \to \exists f \in X g (A) \in ran f$
32		elmapfn	$⊢ g \in ({ran ⋃ X}^{C}) \to g Fn C$
33	32	adantl	$⊢ (φ \land g \in ({ran ⋃ X}^{C})) \to g Fn C$
34		simp3	$⊢ (φ \land f \in X \land g (A) \in ran f) \to g (A) \in ran f$
35	1	3ad2ant1	$⊢ (φ \land f \in X \land g (A) \in ran f) \to A \in V$
36	3	oveq2i	$⊢ B^{C} = B^{\{A\}}$
37	4 36	sseqtrdi	$⊢ φ \to X \subseteq B^{\{A\}}$
38	37	adantr	$⊢ (φ \land f \in X) \to X \subseteq B^{\{A\}}$
39		simpr	$⊢ (φ \land f \in X) \to f \in X$
40	38 39	sseldd	$⊢ (φ \land f \in X) \to f \in (B^{\{A\}})$
41	2	adantr	$⊢ (φ \land f \in X) \to B \in W$
42	5	a1i	$⊢ (φ \land f \in X) \to \{A\} \in V$
43	41 42	elmapd	$⊢ (φ \land f \in X) \to (f \in (B^{\{A\}}) \leftrightarrow f : \{A\} ⟶ B)$
44	40 43	mpbid	$⊢ (φ \land f \in X) \to f : \{A\} ⟶ B$
45	44	3adant3	$⊢ (φ \land f \in X \land g (A) \in ran f) \to f : \{A\} ⟶ B$
46	35 45	rnsnf	$⊢ (φ \land f \in X \land g (A) \in ran f) \to ran f = \{f (A)\}$
47	34 46	eleqtrd	$⊢ (φ \land f \in X \land g (A) \in ran f) \to g (A) \in \{f (A)\}$
48		fvex	$⊢ g (A) \in V$
49	48	elsn	$⊢ g (A) \in \{f (A)\} \leftrightarrow g (A) = f (A)$
50	47 49	sylib	$⊢ (φ \land f \in X \land g (A) \in ran f) \to g (A) = f (A)$
51	50	3adant1r	$⊢ ((φ \land g Fn C) \land f \in X \land g (A) \in ran f) \to g (A) = f (A)$
52	1	adantr	$⊢ (φ \land g Fn C) \to A \in V$
53	52	3ad2ant1	$⊢ ((φ \land g Fn C) \land f \in X \land g (A) \in ran f) \to A \in V$
54		simp1r	$⊢ ((φ \land g Fn C) \land f \in X \land g (A) \in ran f) \to g Fn C$
55	40 36	eleqtrrdi	$⊢ (φ \land f \in X) \to f \in (B^{C})$
56		elmapfn	$⊢ f \in (B^{C}) \to f Fn C$
57	55 56	syl	$⊢ (φ \land f \in X) \to f Fn C$
58	57	adantlr	$⊢ ((φ \land g Fn C) \land f \in X) \to f Fn C$
59	58	3adant3	$⊢ ((φ \land g Fn C) \land f \in X \land g (A) \in ran f) \to f Fn C$
60	53 3 54 59	fsneq	$⊢ ((φ \land g Fn C) \land f \in X \land g (A) \in ran f) \to (g = f \leftrightarrow g (A) = f (A))$
61	51 60	mpbird	$⊢ ((φ \land g Fn C) \land f \in X \land g (A) \in ran f) \to g = f$
62		simp2	$⊢ ((φ \land g Fn C) \land f \in X \land g (A) \in ran f) \to f \in X$
63	61 62	eqeltrd	$⊢ ((φ \land g Fn C) \land f \in X \land g (A) \in ran f) \to g \in X$
64	63	3exp	$⊢ (φ \land g Fn C) \to (f \in X \to (g (A) \in ran f \to g \in X))$
65	9 33 64	syl2anc	$⊢ (φ \land g \in ({ran ⋃ X}^{C})) \to (f \in X \to (g (A) \in ran f \to g \in X))$
66	65	rexlimdv	$⊢ (φ \land g \in ({ran ⋃ X}^{C})) \to (\exists f \in X g (A) \in ran f \to g \in X)$
67	31 66	mpd	$⊢ (φ \land g \in ({ran ⋃ X}^{C})) \to g \in X$
68	8 67	eqelssd	$⊢ φ \to X = {ran ⋃ X}^{C}$

Metamath Proof Explorer

Theorem unirnmapsn

Proof