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	syl5bbr	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 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 )