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

Metamath Proof Explorer

Theorem unimax

Description: Any member of a class is the largest of those members that it includes. (Contributed by NM, 13-Aug-2002)

Ref Expression
Assertion unimax ( 𝐴 ∈ 𝐵 → ∪ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } = 𝐴 )

Proof

Step Hyp Ref Expression
1 ssid ⊢ 𝐴 ⊆ 𝐴
2 sseq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴 ) )
3 2 elrab3 ⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } ↔ 𝐴 ⊆ 𝐴 ) )
4 1 3 mpbiri ⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } )
5 sseq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴 ) )
6 5 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ⊆ 𝐴 ) )
7 6 simprbi ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } → 𝑦 ⊆ 𝐴 )
8 7 rgen ⊢ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } 𝑦 ⊆ 𝐴
9 ssunieq ⊢ ( ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } 𝑦 ⊆ 𝐴 ) → 𝐴 = ∪ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } )
10 9 eqcomd ⊢ ( ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } 𝑦 ⊆ 𝐴 ) → ∪ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } = 𝐴 )
11 4 8 10 sylancl ⊢ ( 𝐴 ∈ 𝐵 → ∪ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } = 𝐴 )