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

Metamath Proof Explorer

Theorem onint

Description: The intersection (infimum) of a nonempty class of ordinal numbers belongs to the class. Compare Exercise 4 of TakeutiZaring p. 45. (Contributed by NM, 31-Jan-1997)

Ref Expression
Assertion onint ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 ordon ⊢ Ord On
2 tz7.5 ⊢ ( ( Ord On ∧ 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ( 𝐴 ∩ 𝑥 ) = ∅ )
3 1 2 mp3an1 ⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ( 𝐴 ∩ 𝑥 ) = ∅ )
4 ssel ⊢ ( 𝐴 ⊆ On → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ On ) )
5 4 imdistani ⊢ ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) → ( 𝐴 ⊆ On ∧ 𝑥 ∈ On ) )
6 ssel ⊢ ( 𝐴 ⊆ On → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ On ) )
7 ontri1 ⊢ ( ( 𝑥 ∈ On ∧ 𝑧 ∈ On ) → ( 𝑥 ⊆ 𝑧 ↔ ¬ 𝑧 ∈ 𝑥 ) )
8 ssel ⊢ ( 𝑥 ⊆ 𝑧 → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) )
9 7 8 biimtrrdi ⊢ ( ( 𝑥 ∈ On ∧ 𝑧 ∈ On ) → ( ¬ 𝑧 ∈ 𝑥 → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ) )
10 9 ex ⊢ ( 𝑥 ∈ On → ( 𝑧 ∈ On → ( ¬ 𝑧 ∈ 𝑥 → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ) ) )
11 6 10 sylan9 ⊢ ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ On ) → ( 𝑧 ∈ 𝐴 → ( ¬ 𝑧 ∈ 𝑥 → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ) ) )
12 11 com4r ⊢ ( 𝑦 ∈ 𝑥 → ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ On ) → ( 𝑧 ∈ 𝐴 → ( ¬ 𝑧 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) ) ) )
13 12 imp31 ⊢ ( ( ( 𝑦 ∈ 𝑥 ∧ ( 𝐴 ⊆ On ∧ 𝑥 ∈ On ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ¬ 𝑧 ∈ 𝑥 → 𝑦 ∈ 𝑧 ) )
14 13 ralimdva ⊢ ( ( 𝑦 ∈ 𝑥 ∧ ( 𝐴 ⊆ On ∧ 𝑥 ∈ On ) ) → ( ∀ 𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑥 → ∀ 𝑧 ∈ 𝐴 𝑦 ∈ 𝑧 ) )
15 disj ⊢ ( ( 𝐴 ∩ 𝑥 ) = ∅ ↔ ∀ 𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑥 )
16 vex ⊢ 𝑦 ∈ V
17 16 elint2 ⊢ ( 𝑦 ∈ ∩ 𝐴 ↔ ∀ 𝑧 ∈ 𝐴 𝑦 ∈ 𝑧 )
18 14 15 17 3imtr4g ⊢ ( ( 𝑦 ∈ 𝑥 ∧ ( 𝐴 ⊆ On ∧ 𝑥 ∈ On ) ) → ( ( 𝐴 ∩ 𝑥 ) = ∅ → 𝑦 ∈ ∩ 𝐴 ) )
19 5 18 sylan2 ⊢ ( ( 𝑦 ∈ 𝑥 ∧ ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) ) → ( ( 𝐴 ∩ 𝑥 ) = ∅ → 𝑦 ∈ ∩ 𝐴 ) )
20 19 exp32 ⊢ ( 𝑦 ∈ 𝑥 → ( 𝐴 ⊆ On → ( 𝑥 ∈ 𝐴 → ( ( 𝐴 ∩ 𝑥 ) = ∅ → 𝑦 ∈ ∩ 𝐴 ) ) ) )
21 20 com4l ⊢ ( 𝐴 ⊆ On → ( 𝑥 ∈ 𝐴 → ( ( 𝐴 ∩ 𝑥 ) = ∅ → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ ∩ 𝐴 ) ) ) )
22 21 imp32 ⊢ ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐴 ∩ 𝑥 ) = ∅ ) ) → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ ∩ 𝐴 ) )
23 22 ssrdv ⊢ ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐴 ∩ 𝑥 ) = ∅ ) ) → 𝑥 ⊆ ∩ 𝐴 )
24 intss1 ⊢ ( 𝑥 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑥 )
25 24 ad2antrl ⊢ ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐴 ∩ 𝑥 ) = ∅ ) ) → ∩ 𝐴 ⊆ 𝑥 )
26 23 25 eqssd ⊢ ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐴 ∩ 𝑥 ) = ∅ ) ) → 𝑥 = ∩ 𝐴 )
27 26 eleq1d ⊢ ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐴 ∩ 𝑥 ) = ∅ ) ) → ( 𝑥 ∈ 𝐴 ↔ ∩ 𝐴 ∈ 𝐴 ) )
28 27 biimpd ⊢ ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐴 ∩ 𝑥 ) = ∅ ) ) → ( 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ 𝐴 ) )
29 28 exp32 ⊢ ( 𝐴 ⊆ On → ( 𝑥 ∈ 𝐴 → ( ( 𝐴 ∩ 𝑥 ) = ∅ → ( 𝑥 ∈ 𝐴 → ∩ 𝐴 ∈ 𝐴 ) ) ) )
30 29 com34 ⊢ ( 𝐴 ⊆ On → ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → ( ( 𝐴 ∩ 𝑥 ) = ∅ → ∩ 𝐴 ∈ 𝐴 ) ) ) )
31 30 pm2.43d ⊢ ( 𝐴 ⊆ On → ( 𝑥 ∈ 𝐴 → ( ( 𝐴 ∩ 𝑥 ) = ∅ → ∩ 𝐴 ∈ 𝐴 ) ) )
32 31 rexlimdv ⊢ ( 𝐴 ⊆ On → ( ∃ 𝑥 ∈ 𝐴 ( 𝐴 ∩ 𝑥 ) = ∅ → ∩ 𝐴 ∈ 𝐴 ) )
33 3 32 syl5 ⊢ ( 𝐴 ⊆ On → ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ 𝐴 ) )
34 33 anabsi5 ⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ 𝐴 )