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