Theorem 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	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	unirnmapsn.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
	unirnmapsn.C	⊢ 𝐶 = { 𝐴 }
	unirnmapsn.x	⊢ ( 𝜑 → 𝑋 ⊆ ( 𝐵 ↑m 𝐶 ) )
Assertion	unirnmapsn	⊢ ( 𝜑 → 𝑋 = ( ran ∪ 𝑋 ↑m 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		unirnmapsn.A	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		unirnmapsn.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		unirnmapsn.C	⊢ 𝐶 = { 𝐴 }
4		unirnmapsn.x	⊢ ( 𝜑 → 𝑋 ⊆ ( 𝐵 ↑m 𝐶 ) )
5		snex	⊢ { 𝐴 } ∈ V
6	3 5	eqeltri	⊢ 𝐶 ∈ V
7	6	a1i	⊢ ( 𝜑 → 𝐶 ∈ V )
8	7 4	unirnmap	⊢ ( 𝜑 → 𝑋 ⊆ ( ran ∪ 𝑋 ↑m 𝐶 ) )
9		simpl	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ran ∪ 𝑋 ↑m 𝐶 ) ) → 𝜑 )
10		equid	⊢ 𝑔 = 𝑔
11		rnuni	⊢ ran ∪ 𝑋 = ∪ 𝑓 ∈ 𝑋 ran 𝑓
12	11	oveq1i	⊢ ( ran ∪ 𝑋 ↑m 𝐶 ) = ( ∪ 𝑓 ∈ 𝑋 ran 𝑓 ↑m 𝐶 )
13	10 12	eleq12i	⊢ ( 𝑔 ∈ ( ran ∪ 𝑋 ↑m 𝐶 ) ↔ 𝑔 ∈ ( ∪ 𝑓 ∈ 𝑋 ran 𝑓 ↑m 𝐶 ) )
14	13	bilani	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ran ∪ 𝑋 ↑m 𝐶 ) ) → 𝑔 ∈ ( ∪ 𝑓 ∈ 𝑋 ran 𝑓 ↑m 𝐶 ) )
15		ovexd	⊢ ( 𝜑 → ( 𝐵 ↑m 𝐶 ) ∈ V )
16	15 4	ssexd	⊢ ( 𝜑 → 𝑋 ∈ V )
17		rnexg	⊢ ( 𝑓 ∈ 𝑋 → ran 𝑓 ∈ V )
18	17	rgen	⊢ ∀ 𝑓 ∈ 𝑋 ran 𝑓 ∈ V
19	18	a1i	⊢ ( 𝜑 → ∀ 𝑓 ∈ 𝑋 ran 𝑓 ∈ V )
20		iunexg	⊢ ( ( 𝑋 ∈ V ∧ ∀ 𝑓 ∈ 𝑋 ran 𝑓 ∈ V ) → ∪ 𝑓 ∈ 𝑋 ran 𝑓 ∈ V )
21	16 19 20	syl2anc	⊢ ( 𝜑 → ∪ 𝑓 ∈ 𝑋 ran 𝑓 ∈ V )
22	21 7	elmapd	⊢ ( 𝜑 → ( 𝑔 ∈ ( ∪ 𝑓 ∈ 𝑋 ran 𝑓 ↑m 𝐶 ) ↔ 𝑔 : 𝐶 ⟶ ∪ 𝑓 ∈ 𝑋 ran 𝑓 ) )
23	22	biimpa	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ∪ 𝑓 ∈ 𝑋 ran 𝑓 ↑m 𝐶 ) ) → 𝑔 : 𝐶 ⟶ ∪ 𝑓 ∈ 𝑋 ran 𝑓 )
24		snidg	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 } )
25	1 24	syl	⊢ ( 𝜑 → 𝐴 ∈ { 𝐴 } )
26	25 3	eleqtrrdi	⊢ ( 𝜑 → 𝐴 ∈ 𝐶 )
27	26	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ∪ 𝑓 ∈ 𝑋 ran 𝑓 ↑m 𝐶 ) ) → 𝐴 ∈ 𝐶 )
28	23 27	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ∪ 𝑓 ∈ 𝑋 ran 𝑓 ↑m 𝐶 ) ) → ( 𝑔 ‘ 𝐴 ) ∈ ∪ 𝑓 ∈ 𝑋 ran 𝑓 )
29		eliun	⊢ ( ( 𝑔 ‘ 𝐴 ) ∈ ∪ 𝑓 ∈ 𝑋 ran 𝑓 ↔ ∃ 𝑓 ∈ 𝑋 ( 𝑔 ‘ 𝐴 ) ∈ ran 𝑓 )
30	28 29	sylib	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ∪ 𝑓 ∈ 𝑋 ran 𝑓 ↑m 𝐶 ) ) → ∃ 𝑓 ∈ 𝑋 ( 𝑔 ‘ 𝐴 ) ∈ ran 𝑓 )
31	9 14 30	syl2anc	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ran ∪ 𝑋 ↑m 𝐶 ) ) → ∃ 𝑓 ∈ 𝑋 ( 𝑔 ‘ 𝐴 ) ∈ ran 𝑓 )
32		elmapfn	⊢ ( 𝑔 ∈ ( ran ∪ 𝑋 ↑m 𝐶 ) → 𝑔 Fn 𝐶 )
33	32	adantl	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ran ∪ 𝑋 ↑m 𝐶 ) ) → 𝑔 Fn 𝐶 )
34		simp3	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ∧ ( 𝑔 ‘ 𝐴 ) ∈ ran 𝑓 ) → ( 𝑔 ‘ 𝐴 ) ∈ ran 𝑓 )
35	1	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ∧ ( 𝑔 ‘ 𝐴 ) ∈ ran 𝑓 ) → 𝐴 ∈ 𝑉 )
36	3	oveq2i	⊢ ( 𝐵 ↑m 𝐶 ) = ( 𝐵 ↑m { 𝐴 } )
37	4 36	sseqtrdi	⊢ ( 𝜑 → 𝑋 ⊆ ( 𝐵 ↑m { 𝐴 } ) )
38	37	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝑋 ⊆ ( 𝐵 ↑m { 𝐴 } ) )
39		simpr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝑓 ∈ 𝑋 )
40	38 39	sseldd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝑓 ∈ ( 𝐵 ↑m { 𝐴 } ) )
41	2	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝐵 ∈ 𝑊 )
42	5	a1i	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → { 𝐴 } ∈ V )
43	41 42	elmapd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ( 𝑓 ∈ ( 𝐵 ↑m { 𝐴 } ) ↔ 𝑓 : { 𝐴 } ⟶ 𝐵 ) )
44	40 43	mpbid	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝑓 : { 𝐴 } ⟶ 𝐵 )
45	44	3adant3	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ∧ ( 𝑔 ‘ 𝐴 ) ∈ ran 𝑓 ) → 𝑓 : { 𝐴 } ⟶ 𝐵 )
46	35 45	rnsnf	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ∧ ( 𝑔 ‘ 𝐴 ) ∈ ran 𝑓 ) → ran 𝑓 = { ( 𝑓 ‘ 𝐴 ) } )
47	34 46	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ∧ ( 𝑔 ‘ 𝐴 ) ∈ ran 𝑓 ) → ( 𝑔 ‘ 𝐴 ) ∈ { ( 𝑓 ‘ 𝐴 ) } )
48		fvex	⊢ ( 𝑔 ‘ 𝐴 ) ∈ V
49	48	elsn	⊢ ( ( 𝑔 ‘ 𝐴 ) ∈ { ( 𝑓 ‘ 𝐴 ) } ↔ ( 𝑔 ‘ 𝐴 ) = ( 𝑓 ‘ 𝐴 ) )
50	47 49	sylib	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ∧ ( 𝑔 ‘ 𝐴 ) ∈ ran 𝑓 ) → ( 𝑔 ‘ 𝐴 ) = ( 𝑓 ‘ 𝐴 ) )
51	50	3adant1r	⊢ ( ( ( 𝜑 ∧ 𝑔 Fn 𝐶 ) ∧ 𝑓 ∈ 𝑋 ∧ ( 𝑔 ‘ 𝐴 ) ∈ ran 𝑓 ) → ( 𝑔 ‘ 𝐴 ) = ( 𝑓 ‘ 𝐴 ) )
52	1	adantr	⊢ ( ( 𝜑 ∧ 𝑔 Fn 𝐶 ) → 𝐴 ∈ 𝑉 )
53	52	3ad2ant1	⊢ ( ( ( 𝜑 ∧ 𝑔 Fn 𝐶 ) ∧ 𝑓 ∈ 𝑋 ∧ ( 𝑔 ‘ 𝐴 ) ∈ ran 𝑓 ) → 𝐴 ∈ 𝑉 )
54		simp1r	⊢ ( ( ( 𝜑 ∧ 𝑔 Fn 𝐶 ) ∧ 𝑓 ∈ 𝑋 ∧ ( 𝑔 ‘ 𝐴 ) ∈ ran 𝑓 ) → 𝑔 Fn 𝐶 )
55	40 36	eleqtrrdi	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝑓 ∈ ( 𝐵 ↑m 𝐶 ) )
56		elmapfn	⊢ ( 𝑓 ∈ ( 𝐵 ↑m 𝐶 ) → 𝑓 Fn 𝐶 )
57	55 56	syl	⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝑓 Fn 𝐶 )
58	57	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑔 Fn 𝐶 ) ∧ 𝑓 ∈ 𝑋 ) → 𝑓 Fn 𝐶 )
59	58	3adant3	⊢ ( ( ( 𝜑 ∧ 𝑔 Fn 𝐶 ) ∧ 𝑓 ∈ 𝑋 ∧ ( 𝑔 ‘ 𝐴 ) ∈ ran 𝑓 ) → 𝑓 Fn 𝐶 )
60	53 3 54 59	fsneq	⊢ ( ( ( 𝜑 ∧ 𝑔 Fn 𝐶 ) ∧ 𝑓 ∈ 𝑋 ∧ ( 𝑔 ‘ 𝐴 ) ∈ ran 𝑓 ) → ( 𝑔 = 𝑓 ↔ ( 𝑔 ‘ 𝐴 ) = ( 𝑓 ‘ 𝐴 ) ) )
61	51 60	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑔 Fn 𝐶 ) ∧ 𝑓 ∈ 𝑋 ∧ ( 𝑔 ‘ 𝐴 ) ∈ ran 𝑓 ) → 𝑔 = 𝑓 )
62		simp2	⊢ ( ( ( 𝜑 ∧ 𝑔 Fn 𝐶 ) ∧ 𝑓 ∈ 𝑋 ∧ ( 𝑔 ‘ 𝐴 ) ∈ ran 𝑓 ) → 𝑓 ∈ 𝑋 )
63	61 62	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑔 Fn 𝐶 ) ∧ 𝑓 ∈ 𝑋 ∧ ( 𝑔 ‘ 𝐴 ) ∈ ran 𝑓 ) → 𝑔 ∈ 𝑋 )
64	63	3exp	⊢ ( ( 𝜑 ∧ 𝑔 Fn 𝐶 ) → ( 𝑓 ∈ 𝑋 → ( ( 𝑔 ‘ 𝐴 ) ∈ ran 𝑓 → 𝑔 ∈ 𝑋 ) ) )
65	9 33 64	syl2anc	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ran ∪ 𝑋 ↑m 𝐶 ) ) → ( 𝑓 ∈ 𝑋 → ( ( 𝑔 ‘ 𝐴 ) ∈ ran 𝑓 → 𝑔 ∈ 𝑋 ) ) )
66	65	rexlimdv	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ran ∪ 𝑋 ↑m 𝐶 ) ) → ( ∃ 𝑓 ∈ 𝑋 ( 𝑔 ‘ 𝐴 ) ∈ ran 𝑓 → 𝑔 ∈ 𝑋 ) )
67	31 66	mpd	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( ran ∪ 𝑋 ↑m 𝐶 ) ) → 𝑔 ∈ 𝑋 )
68	8 67	eqelssd	⊢ ( 𝜑 → 𝑋 = ( ran ∪ 𝑋 ↑m 𝐶 ) )