Theorem oldss

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

	Ref	Expression
Assertion	oldss	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) → ( O ‘ 𝐴 ) ⊆ ( O ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		imass2	⊢ ( 𝐴 ⊆ 𝐵 → ( M “ 𝐴 ) ⊆ ( M “ 𝐵 ) )
2	1	unissd	⊢ ( 𝐴 ⊆ 𝐵 → ∪ ( M “ 𝐴 ) ⊆ ∪ ( M “ 𝐵 ) )
3	2	adantl	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ∪ ( M “ 𝐴 ) ⊆ ∪ ( M “ 𝐵 ) )
4		oldval	⊢ ( 𝐴 ∈ On → ( O ‘ 𝐴 ) = ∪ ( M “ 𝐴 ) )
5	4	adantr	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( O ‘ 𝐴 ) = ∪ ( M “ 𝐴 ) )
6	5	adantr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( O ‘ 𝐴 ) = ∪ ( M “ 𝐴 ) )
7		oldval	⊢ ( 𝐵 ∈ On → ( O ‘ 𝐵 ) = ∪ ( M “ 𝐵 ) )
8	7	adantl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( O ‘ 𝐵 ) = ∪ ( M “ 𝐵 ) )
9	8	adantr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( O ‘ 𝐵 ) = ∪ ( M “ 𝐵 ) )
10	3 6 9	3sstr4d	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝐴 ⊆ 𝐵 ) → ( O ‘ 𝐴 ) ⊆ ( O ‘ 𝐵 ) )
11	10	expl	⊢ ( 𝐴 ∈ On → ( ( 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) → ( O ‘ 𝐴 ) ⊆ ( O ‘ 𝐵 ) ) )
12		oldf	⊢ O : On ⟶ 𝒫 No
13	12	fdmi	⊢ dom O = On
14	13	eleq2i	⊢ ( 𝐴 ∈ dom O ↔ 𝐴 ∈ On )
15		ndmfv	⊢ ( ¬ 𝐴 ∈ dom O → ( O ‘ 𝐴 ) = ∅ )
16	14 15	sylnbir	⊢ ( ¬ 𝐴 ∈ On → ( O ‘ 𝐴 ) = ∅ )
17		0ss	⊢ ∅ ⊆ ( O ‘ 𝐵 )
18	16 17	eqsstrdi	⊢ ( ¬ 𝐴 ∈ On → ( O ‘ 𝐴 ) ⊆ ( O ‘ 𝐵 ) )
19	18	a1d	⊢ ( ¬ 𝐴 ∈ On → ( ( 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) → ( O ‘ 𝐴 ) ⊆ ( O ‘ 𝐵 ) ) )
20	11 19	pm2.61i	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ⊆ 𝐵 ) → ( O ‘ 𝐴 ) ⊆ ( O ‘ 𝐵 ) )