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∈AB∈On∧A≠∅→⋂x∈AB∈On

Proof

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