Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  madeval Structured version   Visualization version   GIF version

 Description: The value of the made by function. (Contributed by Scott Fenton, 17-Dec-2021.)
Assertion
Ref Expression
madeval (𝐴 ∈ On → ( M ‘𝐴) = ( |s “ (𝒫 ( M “ 𝐴) × 𝒫 ( M “ 𝐴))))

Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 df-made 32228 . . 3 M = recs((𝑥 ∈ V ↦ ( |s “ (𝒫 ran 𝑥 × 𝒫 ran 𝑥))))
21tfr2 7655 . 2 (𝐴 ∈ On → ( M ‘𝐴) = ((𝑥 ∈ V ↦ ( |s “ (𝒫 ran 𝑥 × 𝒫 ran 𝑥)))‘( M ↾ 𝐴)))
31tfr1 7654 . . . . 5 M Fn On
4 fnfun 6141 . . . . 5 ( M Fn On → Fun M )
53, 4ax-mp 5 . . . 4 Fun M
6 resfunexg 6635 . . . 4 ((Fun M ∧ 𝐴 ∈ On) → ( M ↾ 𝐴) ∈ V)
75, 6mpan 708 . . 3 (𝐴 ∈ On → ( M ↾ 𝐴) ∈ V)
8 scutf 32217 . . . . 5 |s : <<s ⟶ No
9 ffun 6201 . . . . 5 ( |s : <<s ⟶ No → Fun |s )
108, 9ax-mp 5 . . . 4 Fun |s
11 funimaexg 6128 . . . . . . 7 ((Fun M ∧ 𝐴 ∈ On) → ( M “ 𝐴) ∈ V)
125, 11mpan 708 . . . . . 6 (𝐴 ∈ On → ( M “ 𝐴) ∈ V)
13 uniexg 7112 . . . . . 6 (( M “ 𝐴) ∈ V → ( M “ 𝐴) ∈ V)
14 pwexg 4991 . . . . . 6 ( ( M “ 𝐴) ∈ V → 𝒫 ( M “ 𝐴) ∈ V)
1512, 13, 143syl 18 . . . . 5 (𝐴 ∈ On → 𝒫 ( M “ 𝐴) ∈ V)
16 xpexg 7117 . . . . 5 ((𝒫 ( M “ 𝐴) ∈ V ∧ 𝒫 ( M “ 𝐴) ∈ V) → (𝒫 ( M “ 𝐴) × 𝒫 ( M “ 𝐴)) ∈ V)
1715, 15, 16syl2anc 696 . . . 4 (𝐴 ∈ On → (𝒫 ( M “ 𝐴) × 𝒫 ( M “ 𝐴)) ∈ V)
18 funimaexg 6128 . . . 4 ((Fun |s ∧ (𝒫 ( M “ 𝐴) × 𝒫 ( M “ 𝐴)) ∈ V) → ( |s “ (𝒫 ( M “ 𝐴) × 𝒫 ( M “ 𝐴))) ∈ V)
1910, 17, 18sylancr 698 . . 3 (𝐴 ∈ On → ( |s “ (𝒫 ( M “ 𝐴) × 𝒫 ( M “ 𝐴))) ∈ V)
20 rneq 5498 . . . . . . . . 9 (𝑥 = ( M ↾ 𝐴) → ran 𝑥 = ran ( M ↾ 𝐴))
21 df-ima 5271 . . . . . . . . 9 ( M “ 𝐴) = ran ( M ↾ 𝐴)
2220, 21syl6eqr 2804 . . . . . . . 8 (𝑥 = ( M ↾ 𝐴) → ran 𝑥 = ( M “ 𝐴))
2322unieqd 4590 . . . . . . 7 (𝑥 = ( M ↾ 𝐴) → ran 𝑥 = ( M “ 𝐴))
2423pweqd 4299 . . . . . 6 (𝑥 = ( M ↾ 𝐴) → 𝒫 ran 𝑥 = 𝒫 ( M “ 𝐴))
2524sqxpeqd 5290 . . . . 5 (𝑥 = ( M ↾ 𝐴) → (𝒫 ran 𝑥 × 𝒫 ran 𝑥) = (𝒫 ( M “ 𝐴) × 𝒫 ( M “ 𝐴)))
2625imaeq2d 5616 . . . 4 (𝑥 = ( M ↾ 𝐴) → ( |s “ (𝒫 ran 𝑥 × 𝒫 ran 𝑥)) = ( |s “ (𝒫 ( M “ 𝐴) × 𝒫 ( M “ 𝐴))))
27 eqid 2752 . . . 4 (𝑥 ∈ V ↦ ( |s “ (𝒫 ran 𝑥 × 𝒫 ran 𝑥))) = (𝑥 ∈ V ↦ ( |s “ (𝒫 ran 𝑥 × 𝒫 ran 𝑥)))
2826, 27fvmptg 6434 . . 3 ((( M ↾ 𝐴) ∈ V ∧ ( |s “ (𝒫 ( M “ 𝐴) × 𝒫 ( M “ 𝐴))) ∈ V) → ((𝑥 ∈ V ↦ ( |s “ (𝒫 ran 𝑥 × 𝒫 ran 𝑥)))‘( M ↾ 𝐴)) = ( |s “ (𝒫 ( M “ 𝐴) × 𝒫 ( M “ 𝐴))))
297, 19, 28syl2anc 696 . 2 (𝐴 ∈ On → ((𝑥 ∈ V ↦ ( |s “ (𝒫 ran 𝑥 × 𝒫 ran 𝑥)))‘( M ↾ 𝐴)) = ( |s “ (𝒫 ( M “ 𝐴) × 𝒫 ( M “ 𝐴))))
302, 29eqtrd 2786 1 (𝐴 ∈ On → ( M ‘𝐴) = ( |s “ (𝒫 ( M “ 𝐴) × 𝒫 ( M “ 𝐴))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1624   ∈ wcel 2131  Vcvv 3332  𝒫 cpw 4294  ∪ cuni 4580   ↦ cmpt 4873   × cxp 5256  ran crn 5259   ↾ cres 5260   “ cima 5261  Oncon0 5876  Fun wfun 6035   Fn wfn 6036  ⟶wf 6037  ‘cfv 6041   No csur 32091   <
 Copyright terms: Public domain W3C validator