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 ( ( 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) → ( M ‘ 𝐴 ) ⊆ ( M ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 imass2 ⊢ ( 𝐴 ⊆ 𝐵 → ( M “ 𝐴 ) ⊆ ( M “ 𝐵 ) )
2 1 unissd ⊢ ( 𝐴 ⊆ 𝐵 → ∪ ( M “ 𝐴 ) ⊆ ∪ ( M “ 𝐵 ) )
3 2 sspwd ⊢ ( 𝐴 ⊆ 𝐵 → 𝒫 ∪ ( M “ 𝐴 ) ⊆ 𝒫 ∪ ( M “ 𝐵 ) )
4 3 adantl ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) → 𝒫 ∪ ( M “ 𝐴 ) ⊆ 𝒫 ∪ ( M “ 𝐵 ) )
5 4 adantl ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) ) → 𝒫 ∪ ( M “ 𝐴 ) ⊆ 𝒫 ∪ ( M “ 𝐵 ) )
6 ssrexv ⊢ ( 𝒫 ∪ ( M “ 𝐴 ) ⊆ 𝒫 ∪ ( M “ 𝐵 ) → ( ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) → ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐵 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) ) )
7 5 6 syl ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) ) → ( ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) → ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐵 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) ) )
8 ssrexv ⊢ ( 𝒫 ∪ ( M “ 𝐴 ) ⊆ 𝒫 ∪ ( M “ 𝐵 ) → ( ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) → ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐵 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) ) )
9 5 8 syl ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) ) → ( ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) → ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐵 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) ) )
10 9 reximdv ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) ) → ( ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐵 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) → ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐵 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐵 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) ) )
11 7 10 syld ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) ) → ( ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) → ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐵 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐵 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) ) )
12 11 adantr ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) ) ∧ 𝑥 ∈ No ) → ( ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) → ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐵 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐵 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) ) )
13 12 ss2rabdv ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) ) → { 𝑥 ∈ No ∣ ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) } ⊆ { 𝑥 ∈ No ∣ ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐵 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐵 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) } )
14 madeval2 ⊢ ( 𝐴 ∈ On → ( M ‘ 𝐴 ) = { 𝑥 ∈ No ∣ ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) } )
15 14 adantr ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) ) → ( M ‘ 𝐴 ) = { 𝑥 ∈ No ∣ ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) } )
16 madeval2 ⊢ ( 𝐵 ∈ On → ( M ‘ 𝐵 ) = { 𝑥 ∈ No ∣ ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐵 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐵 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) } )
17 16 adantr ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) → ( M ‘ 𝐵 ) = { 𝑥 ∈ No ∣ ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐵 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐵 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) } )
18 17 adantl ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) ) → ( M ‘ 𝐵 ) = { 𝑥 ∈ No ∣ ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐵 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐵 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) } )
19 13 15 18 3sstr4d ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) ) → ( M ‘ 𝐴 ) ⊆ ( M ‘ 𝐵 ) )
20 madef ⊢ M : On ⟶ 𝒫 No
21 20 fdmi ⊢ dom M = On
22 21 eleq2i ⊢ ( 𝐴 ∈ dom M ↔ 𝐴 ∈ On )
23 ndmfv ⊢ ( ¬ 𝐴 ∈ dom M → ( M ‘ 𝐴 ) = ∅ )
24 22 23 sylnbir ⊢ ( ¬ 𝐴 ∈ On → ( M ‘ 𝐴 ) = ∅ )
25 0ss ⊢ ∅ ⊆ ( M ‘ 𝐵 )
26 24 25 eqsstrdi ⊢ ( ¬ 𝐴 ∈ On → ( M ‘ 𝐴 ) ⊆ ( M ‘ 𝐵 ) )
27 26 adantr ⊢ ( ( ¬ 𝐴 ∈ On ∧ ( 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) ) → ( M ‘ 𝐴 ) ⊆ ( M ‘ 𝐵 ) )
28 19 27 pm2.61ian ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) → ( M ‘ 𝐴 ) ⊆ ( M ‘ 𝐵 ) )