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

Metamath Proof Explorer

Theorem intmin

Description: Any member of a class is the smallest of those members that include it. (Contributed by NM, 13-Aug-2002) (Proof shortened by Andrew Salmon, 9-Jul-2011)

Ref Expression
Assertion intmin ( 𝐴 ∈ 𝐵 → ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } = 𝐴 )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑦 ∈ V
2 1 elintrab ⊢ ( 𝑦 ∈ ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐴 ⊆ 𝑥 → 𝑦 ∈ 𝑥 ) )
3 ssid ⊢ 𝐴 ⊆ 𝐴
4 sseq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐴 ) )
5 eleq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝐴 ) )
6 4 5 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐴 ⊆ 𝑥 → 𝑦 ∈ 𝑥 ) ↔ ( 𝐴 ⊆ 𝐴 → 𝑦 ∈ 𝐴 ) ) )
7 6 rspcv ⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ( 𝐴 ⊆ 𝑥 → 𝑦 ∈ 𝑥 ) → ( 𝐴 ⊆ 𝐴 → 𝑦 ∈ 𝐴 ) ) )
8 3 7 mpii ⊢ ( 𝐴 ∈ 𝐵 → ( ∀ 𝑥 ∈ 𝐵 ( 𝐴 ⊆ 𝑥 → 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝐴 ) )
9 2 8 biimtrid ⊢ ( 𝐴 ∈ 𝐵 → ( 𝑦 ∈ ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } → 𝑦 ∈ 𝐴 ) )
10 9 ssrdv ⊢ ( 𝐴 ∈ 𝐵 → ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } ⊆ 𝐴 )
11 ssintub ⊢ 𝐴 ⊆ ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 }
12 11 a1i ⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ⊆ ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } )
13 10 12 eqssd ⊢ ( 𝐴 ∈ 𝐵 → ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } = 𝐴 )