Theorem onadju

Description: The cardinal and ordinal sums are always equinumerous. (Contributed by Mario Carneiro, 6-Feb-2013) (Revised by Jim Kingdon, 7-Sep-2023)

	Ref	Expression
Assertion	onadju	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) ≈ ( 𝐴 ⊔ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		enrefg	⊢ ( 𝐴 ∈ On → 𝐴 ≈ 𝐴 )
2	1	adantr	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐴 ≈ 𝐴 )
3		simpr	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐵 ∈ On )
4		eqid	⊢ ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) )
5	4	oacomf1olem	⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) ) : 𝐵 –1-1-onto→ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ∧ ( ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ∩ 𝐴 ) = ∅ ) )
6	5	ancoms	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) ) : 𝐵 –1-1-onto→ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ∧ ( ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ∩ 𝐴 ) = ∅ ) )
7	6	simpld	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) ) : 𝐵 –1-1-onto→ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) ) )
8		f1oeng	⊢ ( ( 𝐵 ∈ On ∧ ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) ) : 𝐵 –1-1-onto→ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ) → 𝐵 ≈ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) ) )
9	3 7 8	syl2anc	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐵 ≈ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) ) )
10		incom	⊢ ( 𝐴 ∩ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ) = ( ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ∩ 𝐴 )
11	6	simprd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ∩ 𝐴 ) = ∅ )
12	10 11	syl5eq	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∩ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ) = ∅ )
13		djuenun	⊢ ( ( 𝐴 ≈ 𝐴 ∧ 𝐵 ≈ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ∧ ( 𝐴 ∩ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ) = ∅ ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( 𝐴 ∪ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ) )
14	2 9 12 13	syl3anc	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( 𝐴 ∪ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ) )
15		oarec	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) = ( 𝐴 ∪ ran ( 𝑥 ∈ 𝐵 ↦ ( 𝐴 +o 𝑥 ) ) ) )
16	14 15	breqtrrd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( 𝐴 +o 𝐵 ) )
17	16	ensymd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) ≈ ( 𝐴 ⊔ 𝐵 ) )