Metamath Proof Explorer

Theorem madess

Description: If A is less than or equal to ordinal B , then the made set of A is included in the made set of B . (Contributed by Scott Fenton, 9-Oct-2024)

Ref Expression
Assertion madess Could not format assertion : No typesetting found for |- ( ( B e. On /\ A C_ B ) -> ( _Made ` A ) C_ ( _Made ` B ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 imass2 Could not format ( A C_ B -> ( _Made " A ) C_ ( _Made " B ) ) : No typesetting found for |- ( A C_ B -> ( _Made " A ) C_ ( _Made " B ) ) with typecode |-
2 1 unissd Could not format ( A C_ B -> U. ( _Made " A ) C_ U. ( _Made " B ) ) : No typesetting found for |- ( A C_ B -> U. ( _Made " A ) C_ U. ( _Made " B ) ) with typecode |-
3 2 sspwd Could not format ( A C_ B -> ~P U. ( _Made " A ) C_ ~P U. ( _Made " B ) ) : No typesetting found for |- ( A C_ B -> ~P U. ( _Made " A ) C_ ~P U. ( _Made " B ) ) with typecode |-
4 3 adantl Could not format ( ( B e. On /\ A C_ B ) -> ~P U. ( _Made " A ) C_ ~P U. ( _Made " B ) ) : No typesetting found for |- ( ( B e. On /\ A C_ B ) -> ~P U. ( _Made " A ) C_ ~P U. ( _Made " B ) ) with typecode |-
5 4 adantl Could not format ( ( A e. On /\ ( B e. On /\ A C_ B ) ) -> ~P U. ( _Made " A ) C_ ~P U. ( _Made " B ) ) : No typesetting found for |- ( ( A e. On /\ ( B e. On /\ A C_ B ) ) -> ~P U. ( _Made " A ) C_ ~P U. ( _Made " B ) ) with typecode |-
6 ssrexv Could not format ( ~P U. ( _Made " A ) C_ ~P U. ( _Made " B ) -> ( E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a < E. a e. ~P U. ( _Made " B ) E. b e. ~P U. ( _Made " A ) ( a < ( E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a < E. a e. ~P U. ( _Made " B ) E. b e. ~P U. ( _Made " A ) ( a <
7 5 6 syl Could not format ( ( A e. On /\ ( B e. On /\ A C_ B ) ) -> ( E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a < E. a e. ~P U. ( _Made " B ) E. b e. ~P U. ( _Made " A ) ( a < ( E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a < E. a e. ~P U. ( _Made " B ) E. b e. ~P U. ( _Made " A ) ( a <
8 ssrexv Could not format ( ~P U. ( _Made " A ) C_ ~P U. ( _Made " B ) -> ( E. b e. ~P U. ( _Made " A ) ( a < E. b e. ~P U. ( _Made " B ) ( a < ( E. b e. ~P U. ( _Made " A ) ( a < E. b e. ~P U. ( _Made " B ) ( a <
9 5 8 syl Could not format ( ( A e. On /\ ( B e. On /\ A C_ B ) ) -> ( E. b e. ~P U. ( _Made " A ) ( a < E. b e. ~P U. ( _Made " B ) ( a < ( E. b e. ~P U. ( _Made " A ) ( a < E. b e. ~P U. ( _Made " B ) ( a <
10 9 reximdv Could not format ( ( A e. On /\ ( B e. On /\ A C_ B ) ) -> ( E. a e. ~P U. ( _Made " B ) E. b e. ~P U. ( _Made " A ) ( a < E. a e. ~P U. ( _Made " B ) E. b e. ~P U. ( _Made " B ) ( a < ( E. a e. ~P U. ( _Made " B ) E. b e. ~P U. ( _Made " A ) ( a < E. a e. ~P U. ( _Made " B ) E. b e. ~P U. ( _Made " B ) ( a <
11 7 10 syld Could not format ( ( A e. On /\ ( B e. On /\ A C_ B ) ) -> ( E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a < E. a e. ~P U. ( _Made " B ) E. b e. ~P U. ( _Made " B ) ( a < ( E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a < E. a e. ~P U. ( _Made " B ) E. b e. ~P U. ( _Made " B ) ( a <
12 11 adantr Could not format ( ( ( A e. On /\ ( B e. On /\ A C_ B ) ) /\ x e. No ) -> ( E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a < E. a e. ~P U. ( _Made " B ) E. b e. ~P U. ( _Made " B ) ( a < ( E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a < E. a e. ~P U. ( _Made " B ) E. b e. ~P U. ( _Made " B ) ( a <
13 12 ss2rabdv Could not format ( ( A e. On /\ ( B e. On /\ A C_ B ) ) -> { x e. No | E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a < { x e. No | E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a <
14 madeval2 Could not format ( A e. On -> ( _Made ` A ) = { x e. No | E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a < ( _Made ` A ) = { x e. No | E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a <
15 14 adantr Could not format ( ( A e. On /\ ( B e. On /\ A C_ B ) ) -> ( _Made ` A ) = { x e. No | E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a < ( _Made ` A ) = { x e. No | E. a e. ~P U. ( _Made " A ) E. b e. ~P U. ( _Made " A ) ( a <
16 madeval2 Could not format ( B e. On -> ( _Made ` B ) = { x e. No | E. a e. ~P U. ( _Made " B ) E. b e. ~P U. ( _Made " B ) ( a < ( _Made ` B ) = { x e. No | E. a e. ~P U. ( _Made " B ) E. b e. ~P U. ( _Made " B ) ( a <
17 16 adantr Could not format ( ( B e. On /\ A C_ B ) -> ( _Made ` B ) = { x e. No | E. a e. ~P U. ( _Made " B ) E. b e. ~P U. ( _Made " B ) ( a < ( _Made ` B ) = { x e. No | E. a e. ~P U. ( _Made " B ) E. b e. ~P U. ( _Made " B ) ( a <
18 17 adantl Could not format ( ( A e. On /\ ( B e. On /\ A C_ B ) ) -> ( _Made ` B ) = { x e. No | E. a e. ~P U. ( _Made " B ) E. b e. ~P U. ( _Made " B ) ( a < ( _Made ` B ) = { x e. No | E. a e. ~P U. ( _Made " B ) E. b e. ~P U. ( _Made " B ) ( a <
19 13 15 18 3sstr4d Could not format ( ( A e. On /\ ( B e. On /\ A C_ B ) ) -> ( _Made ` A ) C_ ( _Made ` B ) ) : No typesetting found for |- ( ( A e. On /\ ( B e. On /\ A C_ B ) ) -> ( _Made ` A ) C_ ( _Made ` B ) ) with typecode |-
20 madef Could not format _Made : On --> ~P No : No typesetting found for |- _Made : On --> ~P No with typecode |-
21 20 fdmi Could not format dom _Made = On : No typesetting found for |- dom _Made = On with typecode |-
22 21 eleq2i Could not format ( A e. dom _Made <-> A e. On ) : No typesetting found for |- ( A e. dom _Made <-> A e. On ) with typecode |-
23 ndmfv Could not format ( -. A e. dom _Made -> ( _Made ` A ) = (/) ) : No typesetting found for |- ( -. A e. dom _Made -> ( _Made ` A ) = (/) ) with typecode |-
24 22 23 sylnbir Could not format ( -. A e. On -> ( _Made ` A ) = (/) ) : No typesetting found for |- ( -. A e. On -> ( _Made ` A ) = (/) ) with typecode |-
25 0ss Could not format (/) C_ ( _Made ` B ) : No typesetting found for |- (/) C_ ( _Made ` B ) with typecode |-
26 24 25 eqsstrdi Could not format ( -. A e. On -> ( _Made ` A ) C_ ( _Made ` B ) ) : No typesetting found for |- ( -. A e. On -> ( _Made ` A ) C_ ( _Made ` B ) ) with typecode |-
27 26 adantr Could not format ( ( -. A e. On /\ ( B e. On /\ A C_ B ) ) -> ( _Made ` A ) C_ ( _Made ` B ) ) : No typesetting found for |- ( ( -. A e. On /\ ( B e. On /\ A C_ B ) ) -> ( _Made ` A ) C_ ( _Made ` B ) ) with typecode |-
28 19 27 pm2.61ian Could not format ( ( B e. On /\ A C_ B ) -> ( _Made ` A ) C_ ( _Made ` B ) ) : No typesetting found for |- ( ( B e. On /\ A C_ B ) -> ( _Made ` A ) C_ ( _Made ` B ) ) with typecode |-