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	syl5bi	⊢ ( 𝐴 ∈ 𝐵 → ( 𝑦 ∈ ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } → 𝑦 ∈ 𝐴 ) )
10	9	ssrdv	⊢ ( 𝐴 ∈ 𝐵 → ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } ⊆ 𝐴 )
11		ssintub	⊢ 𝐴 ⊆ ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 }
12	11	a1i	⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ⊆ ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } )
13	10 12	eqssd	⊢ ( 𝐴 ∈ 𝐵 → ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } = 𝐴 )