Metamath Proof Explorer


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 ffvelrnd ( ( 𝜑𝑔 ∈ ( 𝑓𝑋 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 𝐶 ) )