Theorem onelssex

Description: Ordinal less than is equivalent to having an ordinal between them. (Contributed by Scott Fenton, 8-Aug-2024)

	Ref	Expression
Assertion	onelssex	⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ 𝐶 ↔ ∃ 𝑏 ∈ 𝐶 𝐴 ⊆ 𝑏 ) )

Proof

Step	Hyp	Ref	Expression
1		ssid	⊢ 𝐴 ⊆ 𝐴
2		sseq2	⊢ ( 𝑏 = 𝐴 → ( 𝐴 ⊆ 𝑏 ↔ 𝐴 ⊆ 𝐴 ) )
3	2	rspcev	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐴 ⊆ 𝐴 ) → ∃ 𝑏 ∈ 𝐶 𝐴 ⊆ 𝑏 )
4	1 3	mpan2	⊢ ( 𝐴 ∈ 𝐶 → ∃ 𝑏 ∈ 𝐶 𝐴 ⊆ 𝑏 )
5		ontr2	⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐴 ⊆ 𝑏 ∧ 𝑏 ∈ 𝐶 ) → 𝐴 ∈ 𝐶 ) )
6	5	expcomd	⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( 𝑏 ∈ 𝐶 → ( 𝐴 ⊆ 𝑏 → 𝐴 ∈ 𝐶 ) ) )
7	6	rexlimdv	⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( ∃ 𝑏 ∈ 𝐶 𝐴 ⊆ 𝑏 → 𝐴 ∈ 𝐶 ) )
8	4 7	impbid2	⊢ ( ( 𝐴 ∈ On ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ 𝐶 ↔ ∃ 𝑏 ∈ 𝐶 𝐴 ⊆ 𝑏 ) )