Metamath Proof Explorer

Theorem iinon

Description: The nonempty indexed intersection of a class of ordinal numbers B ( x ) is an ordinal number. (Contributed by NM, 13-Oct-2003) (Proof shortened by Mario Carneiro, 5-Dec-2016)

Ref Expression
Assertion iinon ⊢ ∀ x ∈ A B ∈ On ∧ A ≠ ∅ → ⋂ x ∈ A B ∈ On

Proof

Step Hyp Ref Expression
1 dfiin3g ⊢ ∀ x ∈ A B ∈ On → ⋂ x ∈ A B = ⋂ ran ⁡ x ∈ A ⟼ B
2 1 adantr ⊢ ∀ x ∈ A B ∈ On ∧ A ≠ ∅ → ⋂ x ∈ A B = ⋂ ran ⁡ x ∈ A ⟼ B
3 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
4 3 rnmptss ⊢ ∀ x ∈ A B ∈ On → ran ⁡ x ∈ A ⟼ B ⊆ On
5 dm0rn0 ⊢ dom ⁡ x ∈ A ⟼ B = ∅ ↔ ran ⁡ x ∈ A ⟼ B = ∅
6 dmmptg ⊢ ∀ x ∈ A B ∈ On → dom ⁡ x ∈ A ⟼ B = A
7 6 eqeq1d ⊢ ∀ x ∈ A B ∈ On → dom ⁡ x ∈ A ⟼ B = ∅ ↔ A = ∅
8 5 7 bitr3id ⊢ ∀ x ∈ A B ∈ On → ran ⁡ x ∈ A ⟼ B = ∅ ↔ A = ∅
9 8 necon3bid ⊢ ∀ x ∈ A B ∈ On → ran ⁡ x ∈ A ⟼ B ≠ ∅ ↔ A ≠ ∅
10 9 biimpar ⊢ ∀ x ∈ A B ∈ On ∧ A ≠ ∅ → ran ⁡ x ∈ A ⟼ B ≠ ∅
11 oninton ⊢ ran ⁡ x ∈ A ⟼ B ⊆ On ∧ ran ⁡ x ∈ A ⟼ B ≠ ∅ → ⋂ ran ⁡ x ∈ A ⟼ B ∈ On
12 4 10 11 syl2an2r ⊢ ∀ x ∈ A B ∈ On ∧ A ≠ ∅ → ⋂ ran ⁡ x ∈ A ⟼ B ∈ On
13 2 12 eqeltrd ⊢ ∀ x ∈ A B ∈ On ∧ A ≠ ∅ → ⋂ x ∈ A B ∈ On