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	syl6ib	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ 𝐴 ) → ( ¬ ∩ 𝐴 ∈ 𝑥 → 𝑥 = ∩ 𝐴 ) )
15	14	necon1ad	⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ≠ ∩ 𝐴 → ∩ 𝐴 ∈ 𝑥 ) )
16	15	expimpd	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ≠ ∩ 𝐴 ) → ∩ 𝐴 ∈ 𝑥 ) )
17	1 16	syl5bi	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ( 𝑥 ∈ ( 𝐴 ∖ { ∩ 𝐴 } ) → ∩ 𝐴 ∈ 𝑥 ) )
18	17	ralrimiv	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∀ 𝑥 ∈ ( 𝐴 ∖ { ∩ 𝐴 } ) ∩ 𝐴 ∈ 𝑥 )
19		intex	⊢ ( 𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V )
20		elintg	⊢ ( ∩ 𝐴 ∈ V → ( ∩ 𝐴 ∈ ∩ ( 𝐴 ∖ { ∩ 𝐴 } ) ↔ ∀ 𝑥 ∈ ( 𝐴 ∖ { ∩ 𝐴 } ) ∩ 𝐴 ∈ 𝑥 ) )
21	19 20	sylbi	⊢ ( 𝐴 ≠ ∅ → ( ∩ 𝐴 ∈ ∩ ( 𝐴 ∖ { ∩ 𝐴 } ) ↔ ∀ 𝑥 ∈ ( 𝐴 ∖ { ∩ 𝐴 } ) ∩ 𝐴 ∈ 𝑥 ) )
22	21	adantl	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ( ∩ 𝐴 ∈ ∩ ( 𝐴 ∖ { ∩ 𝐴 } ) ↔ ∀ 𝑥 ∈ ( 𝐴 ∖ { ∩ 𝐴 } ) ∩ 𝐴 ∈ 𝑥 ) )
23	18 22	mpbird	⊢ ( ( 𝐴 ⊆ On ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ ∩ ( 𝐴 ∖ { ∩ 𝐴 } ) )