Metamath Proof Explorer

Theorem onmindif

Description: When its successor is subtracted from a class of ordinal numbers, an ordinal number is less than the minimum of the resulting subclass. (Contributed by NM, 1-Dec-2003)

Ref Expression
Assertion onmindif ⊢ A ⊆ On ∧ B ∈ On → B ∈ ⋂ A ∖ suc ⁡ B

Proof

Step Hyp Ref Expression
1 eldif ⊢ x ∈ A ∖ suc ⁡ B ↔ x ∈ A ∧ ¬ x ∈ suc ⁡ B
2 ssel2 ⊢ A ⊆ On ∧ x ∈ A → x ∈ On
3 ontri1 ⊢ x ∈ On ∧ B ∈ On → x ⊆ B ↔ ¬ B ∈ x
4 onsssuc ⊢ x ∈ On ∧ B ∈ On → x ⊆ B ↔ x ∈ suc ⁡ B
5 3 4 bitr3d ⊢ x ∈ On ∧ B ∈ On → ¬ B ∈ x ↔ x ∈ suc ⁡ B
6 5 con1bid ⊢ x ∈ On ∧ B ∈ On → ¬ x ∈ suc ⁡ B ↔ B ∈ x
7 2 6 sylan ⊢ A ⊆ On ∧ x ∈ A ∧ B ∈ On → ¬ x ∈ suc ⁡ B ↔ B ∈ x
8 7 biimpd ⊢ A ⊆ On ∧ x ∈ A ∧ B ∈ On → ¬ x ∈ suc ⁡ B → B ∈ x
9 8 exp31 ⊢ A ⊆ On → x ∈ A → B ∈ On → ¬ x ∈ suc ⁡ B → B ∈ x
10 9 com23 ⊢ A ⊆ On → B ∈ On → x ∈ A → ¬ x ∈ suc ⁡ B → B ∈ x
11 10 imp4b ⊢ A ⊆ On ∧ B ∈ On → x ∈ A ∧ ¬ x ∈ suc ⁡ B → B ∈ x
12 1 11 syl5bi ⊢ A ⊆ On ∧ B ∈ On → x ∈ A ∖ suc ⁡ B → B ∈ x
13 12 ralrimiv ⊢ A ⊆ On ∧ B ∈ On → ∀ x ∈ A ∖ suc ⁡ B B ∈ x
14 elintg ⊢ B ∈ On → B ∈ ⋂ A ∖ suc ⁡ B ↔ ∀ x ∈ A ∖ suc ⁡ B B ∈ x
15 14 adantl ⊢ A ⊆ On ∧ B ∈ On → B ∈ ⋂ A ∖ suc ⁡ B ↔ ∀ x ∈ A ∖ suc ⁡ B B ∈ x
16 13 15 mpbird ⊢ A ⊆ On ∧ B ∈ On → B ∈ ⋂ A ∖ suc ⁡ B