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