Theorem madess

Description: If ordinal 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, 7-Aug-2024)

	Ref	Expression
Assertion	madess	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) → ( M ‘ 𝐴 ) ⊆ ( M ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		imass2	⊢ ( 𝐴 ⊆ 𝐵 → ( M “ 𝐴 ) ⊆ ( M “ 𝐵 ) )
2	1	3ad2ant3	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) → ( M “ 𝐴 ) ⊆ ( M “ 𝐵 ) )
3	2	adantr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ No ) → ( M “ 𝐴 ) ⊆ ( M “ 𝐵 ) )
4	3	unissd	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ No ) → ∪ ( M “ 𝐴 ) ⊆ ∪ ( M “ 𝐵 ) )
5	4	sspwd	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ No ) → 𝒫 ∪ ( M “ 𝐴 ) ⊆ 𝒫 ∪ ( M “ 𝐵 ) )
6		ssrexv	⊢ ( 𝒫 ∪ ( M “ 𝐴 ) ⊆ 𝒫 ∪ ( M “ 𝐵 ) → ( ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) → ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐵 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ) )
7	5 6	syl	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ No ) → ( ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) → ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐵 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ) )
8		ssrexv	⊢ ( 𝒫 ∪ ( M “ 𝐴 ) ⊆ 𝒫 ∪ ( M “ 𝐵 ) → ( ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) → ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐵 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ) )
9	5 8	syl	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ No ) → ( ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) → ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐵 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ) )
10	9	reximdv	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ No ) → ( ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐵 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) → ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐵 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐵 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ) )
11	7 10	syld	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ No ) → ( ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) → ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐵 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐵 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ) )
12	11	ralrimiva	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) → ∀ 𝑥 ∈ No ( ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) → ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐵 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐵 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ) )
13		ss2rab	⊢ ( { 𝑥 ∈ No ∣ ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) } ⊆ { 𝑥 ∈ No ∣ ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐵 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐵 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) } ↔ ∀ 𝑥 ∈ No ( ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) → ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐵 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐵 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ) )
14	12 13	sylibr	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) → { 𝑥 ∈ No ∣ ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) } ⊆ { 𝑥 ∈ No ∣ ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐵 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐵 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) } )
15		madeval2	⊢ ( 𝐴 ∈ On → ( M ‘ 𝐴 ) = { 𝑥 ∈ No ∣ ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) } )
16	15	3ad2ant1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) → ( M ‘ 𝐴 ) = { 𝑥 ∈ No ∣ ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) } )
17		madeval2	⊢ ( 𝐵 ∈ On → ( M ‘ 𝐵 ) = { 𝑥 ∈ No ∣ ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐵 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐵 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) } )
18	17	3ad2ant2	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) → ( M ‘ 𝐵 ) = { 𝑥 ∈ No ∣ ∃ 𝑙 ∈ 𝒫 ∪ ( M “ 𝐵 ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ 𝐵 ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) } )
19	14 16 18	3sstr4d	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) → ( M ‘ 𝐴 ) ⊆ ( M ‘ 𝐵 ) )