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

Metamath Proof Explorer

Theorem unirnmapsn

Proof