Metamath Proof Explorer

Theorem madeoldsuc

Description: The made set is the old set of its successor. (Contributed by Scott Fenton, 8-Aug-2024)

Ref Expression
Assertion madeoldsuc Could not format assertion : No typesetting found for |- ( A e. On -> ( _Made ` A ) = ( _Old ` suc A ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 df-suc ⊢suc⁡A=A∪A
2 1 imaeq2i Could not format ( _Made " suc A ) = ( _Made " ( A u. { A } ) ) : No typesetting found for |- ( _Made " suc A ) = ( _Made " ( A u. { A } ) ) with typecode |-
3 imaundi Could not format ( _Made " ( A u. { A } ) ) = ( ( _Made " A ) u. ( _Made " { A } ) ) : No typesetting found for |- ( _Made " ( A u. { A } ) ) = ( ( _Made " A ) u. ( _Made " { A } ) ) with typecode |-
4 2 3 eqtri Could not format ( _Made " suc A ) = ( ( _Made " A ) u. ( _Made " { A } ) ) : No typesetting found for |- ( _Made " suc A ) = ( ( _Made " A ) u. ( _Made " { A } ) ) with typecode |-
5 4 unieqi Could not format U. ( _Made " suc A ) = U. ( ( _Made " A ) u. ( _Made " { A } ) ) : No typesetting found for |- U. ( _Made " suc A ) = U. ( ( _Made " A ) u. ( _Made " { A } ) ) with typecode |-
6 uniun Could not format U. ( ( _Made " A ) u. ( _Made " { A } ) ) = ( U. ( _Made " A ) u. U. ( _Made " { A } ) ) : No typesetting found for |- U. ( ( _Made " A ) u. ( _Made " { A } ) ) = ( U. ( _Made " A ) u. U. ( _Made " { A } ) ) with typecode |-
7 5 6 eqtri Could not format U. ( _Made " suc A ) = ( U. ( _Made " A ) u. U. ( _Made " { A } ) ) : No typesetting found for |- U. ( _Made " suc A ) = ( U. ( _Made " A ) u. U. ( _Made " { A } ) ) with typecode |-
8 7 a1i Could not format ( A e. On -> U. ( _Made " suc A ) = ( U. ( _Made " A ) u. U. ( _Made " { A } ) ) ) : No typesetting found for |- ( A e. On -> U. ( _Made " suc A ) = ( U. ( _Made " A ) u. U. ( _Made " { A } ) ) ) with typecode |-
9 oldval Could not format ( A e. On -> ( _Old ` A ) = U. ( _Made " A ) ) : No typesetting found for |- ( A e. On -> ( _Old ` A ) = U. ( _Made " A ) ) with typecode |-
10 9 eqcomd Could not format ( A e. On -> U. ( _Made " A ) = ( _Old ` A ) ) : No typesetting found for |- ( A e. On -> U. ( _Made " A ) = ( _Old ` A ) ) with typecode |-
11 madef Could not format _Made : On --> ~P No : No typesetting found for |- _Made : On --> ~P No with typecode |-
12 ffn Could not format ( _Made : On --> ~P No -> _Made Fn On ) : No typesetting found for |- ( _Made : On --> ~P No -> _Made Fn On ) with typecode |-
13 11 12 ax-mp Could not format _Made Fn On : No typesetting found for |- _Made Fn On with typecode |-
14 fnsnfv Could not format ( ( _Made Fn On /\ A e. On ) -> { ( _Made ` A ) } = ( _Made " { A } ) ) : No typesetting found for |- ( ( _Made Fn On /\ A e. On ) -> { ( _Made ` A ) } = ( _Made " { A } ) ) with typecode |-
15 14 eqcomd Could not format ( ( _Made Fn On /\ A e. On ) -> ( _Made " { A } ) = { ( _Made ` A ) } ) : No typesetting found for |- ( ( _Made Fn On /\ A e. On ) -> ( _Made " { A } ) = { ( _Made ` A ) } ) with typecode |-
16 13 15 mpan Could not format ( A e. On -> ( _Made " { A } ) = { ( _Made ` A ) } ) : No typesetting found for |- ( A e. On -> ( _Made " { A } ) = { ( _Made ` A ) } ) with typecode |-
17 16 unieqd Could not format ( A e. On -> U. ( _Made " { A } ) = U. { ( _Made ` A ) } ) : No typesetting found for |- ( A e. On -> U. ( _Made " { A } ) = U. { ( _Made ` A ) } ) with typecode |-
18 fvex Could not format ( _Made ` A ) e. _V : No typesetting found for |- ( _Made ` A ) e. _V with typecode |-
19 18 unisn Could not format U. { ( _Made ` A ) } = ( _Made ` A ) : No typesetting found for |- U. { ( _Made ` A ) } = ( _Made ` A ) with typecode |-
20 17 19 eqtrdi Could not format ( A e. On -> U. ( _Made " { A } ) = ( _Made ` A ) ) : No typesetting found for |- ( A e. On -> U. ( _Made " { A } ) = ( _Made ` A ) ) with typecode |-
21 10 20 uneq12d Could not format ( A e. On -> ( U. ( _Made " A ) u. U. ( _Made " { A } ) ) = ( ( _Old ` A ) u. ( _Made ` A ) ) ) : No typesetting found for |- ( A e. On -> ( U. ( _Made " A ) u. U. ( _Made " { A } ) ) = ( ( _Old ` A ) u. ( _Made ` A ) ) ) with typecode |-
22 oldssmade Could not format ( _Old ` A ) C_ ( _Made ` A ) : No typesetting found for |- ( _Old ` A ) C_ ( _Made ` A ) with typecode |-
23 22 a1i Could not format ( A e. On -> ( _Old ` A ) C_ ( _Made ` A ) ) : No typesetting found for |- ( A e. On -> ( _Old ` A ) C_ ( _Made ` A ) ) with typecode |-
24 ssequn1 Could not format ( ( _Old ` A ) C_ ( _Made ` A ) <-> ( ( _Old ` A ) u. ( _Made ` A ) ) = ( _Made ` A ) ) : No typesetting found for |- ( ( _Old ` A ) C_ ( _Made ` A ) <-> ( ( _Old ` A ) u. ( _Made ` A ) ) = ( _Made ` A ) ) with typecode |-
25 23 24 sylib Could not format ( A e. On -> ( ( _Old ` A ) u. ( _Made ` A ) ) = ( _Made ` A ) ) : No typesetting found for |- ( A e. On -> ( ( _Old ` A ) u. ( _Made ` A ) ) = ( _Made ` A ) ) with typecode |-
26 8 21 25 3eqtrrd Could not format ( A e. On -> ( _Made ` A ) = U. ( _Made " suc A ) ) : No typesetting found for |- ( A e. On -> ( _Made ` A ) = U. ( _Made " suc A ) ) with typecode |-
27 onsuc ⊢A∈On→suc⁡A∈On
28 oldval Could not format ( suc A e. On -> ( _Old ` suc A ) = U. ( _Made " suc A ) ) : No typesetting found for |- ( suc A e. On -> ( _Old ` suc A ) = U. ( _Made " suc A ) ) with typecode |-
29 27 28 syl Could not format ( A e. On -> ( _Old ` suc A ) = U. ( _Made " suc A ) ) : No typesetting found for |- ( A e. On -> ( _Old ` suc A ) = U. ( _Made " suc A ) ) with typecode |-
30 26 29 eqtr4d Could not format ( A e. On -> ( _Made ` A ) = ( _Old ` suc A ) ) : No typesetting found for |- ( A e. On -> ( _Made ` A ) = ( _Old ` suc A ) ) with typecode |-