This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ On )

Proof

Step Hyp Ref Expression
1 dfiin3g ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ On → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
2 1 adantr ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
3 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
4 3 rnmptss ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ On → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ On )
5 dm0rn0 ⊢ ( dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ∅ ↔ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ∅ )
6 dmmptg ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ On → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
7 6 eqeq1d ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ On → ( dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ∅ ↔ 𝐴 = ∅ ) )
8 5 7 bitr3id ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ On → ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ∅ ↔ 𝐴 = ∅ ) )
9 8 necon3bid ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ On → ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≠ ∅ ↔ 𝐴 ≠ ∅ ) )
10 9 biimpar ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≠ ∅ )
11 oninton ⊢ ( ( ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ On ∧ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ≠ ∅ ) → ∩ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ On )
12 4 10 11 syl2an2r ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) → ∩ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ On )
13 2 12 eqeltrd ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ On )