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

Metamath Proof Explorer

Theorem onmindif2

Description: The minimum of a class of ordinal numbers is less than the minimum of that class with its minimum removed. (Contributed by NM, 20-Nov-2003)

Ref Expression
Assertion onmindif2 ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ ∩ ( 𝐴 ∖ { ∩ 𝐴 } ) )

Proof

Step Hyp Ref Expression
1 eldifsn ⊢ ( 𝑥 ∈ ( 𝐴 ∖ { ∩ 𝐴 } ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ≠ ∩ 𝐴 ) )
2 onnmin ⊢ ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑥 ∈ ∩ 𝐴 )
3 2 adantlr ⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑥 ∈ ∩ 𝐴 )
4 oninton ⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ On )
5 ssel2 ⊢ ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ On )
6 5 adantlr ⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ On )
7 ontri1 ⊢ ( ( ∩ 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( ∩ 𝐴 ⊆ 𝑥 ↔ ¬ 𝑥 ∈ ∩ 𝐴 ) )
8 onsseleq ⊢ ( ( ∩ 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( ∩ 𝐴 ⊆ 𝑥 ↔ ( ∩ 𝐴 ∈ 𝑥 ∨ ∩ 𝐴 = 𝑥 ) ) )
9 7 8 bitr3d ⊢ ( ( ∩ 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( ¬ 𝑥 ∈ ∩ 𝐴 ↔ ( ∩ 𝐴 ∈ 𝑥 ∨ ∩ 𝐴 = 𝑥 ) ) )
10 4 6 9 syl2an2r ⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ 𝐴 ) → ( ¬ 𝑥 ∈ ∩ 𝐴 ↔ ( ∩ 𝐴 ∈ 𝑥 ∨ ∩ 𝐴 = 𝑥 ) ) )
11 3 10 mpbid ⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ 𝐴 ) → ( ∩ 𝐴 ∈ 𝑥 ∨ ∩ 𝐴 = 𝑥 ) )
12 11 ord ⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ 𝐴 ) → ( ¬ ∩ 𝐴 ∈ 𝑥 → ∩ 𝐴 = 𝑥 ) )
13 eqcom ⊢ ( ∩ 𝐴 = 𝑥 ↔ 𝑥 = ∩ 𝐴 )
14 12 13 imbitrdi ⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ 𝐴 ) → ( ¬ ∩ 𝐴 ∈ 𝑥 → 𝑥 = ∩ 𝐴 ) )
15 14 necon1ad ⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ≠ ∩ 𝐴 → ∩ 𝐴 ∈ 𝑥 ) )
16 15 expimpd ⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ≠ ∩ 𝐴 ) → ∩ 𝐴 ∈ 𝑥 ) )
17 1 16 biimtrid ⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ( 𝑥 ∈ ( 𝐴 ∖ { ∩ 𝐴 } ) → ∩ 𝐴 ∈ 𝑥 ) )
18 17 ralrimiv ⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∀ 𝑥 ∈ ( 𝐴 ∖ { ∩ 𝐴 } ) ∩ 𝐴 ∈ 𝑥 )
19 intex ⊢ ( 𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V )
20 elintg ⊢ ( ∩ 𝐴 ∈ V → ( ∩ 𝐴 ∈ ∩ ( 𝐴 ∖ { ∩ 𝐴 } ) ↔ ∀ 𝑥 ∈ ( 𝐴 ∖ { ∩ 𝐴 } ) ∩ 𝐴 ∈ 𝑥 ) )
21 19 20 sylbi ⊢ ( 𝐴 ≠ ∅ → ( ∩ 𝐴 ∈ ∩ ( 𝐴 ∖ { ∩ 𝐴 } ) ↔ ∀ 𝑥 ∈ ( 𝐴 ∖ { ∩ 𝐴 } ) ∩ 𝐴 ∈ 𝑥 ) )
22 21 adantl ⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ( ∩ 𝐴 ∈ ∩ ( 𝐴 ∖ { ∩ 𝐴 } ) ↔ ∀ 𝑥 ∈ ( 𝐴 ∖ { ∩ 𝐴 } ) ∩ 𝐴 ∈ 𝑥 ) )
23 18 22 mpbird ⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ ∩ ( 𝐴 ∖ { ∩ 𝐴 } ) )