This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 𝐶 ) )