Metamath Proof Explorer


Theorem supexd

Description: A supremum is a set. (Contributed by NM, 22-May-1999) (Revised by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypothesis supmo.1 ( 𝜑𝑅 Or 𝐴 )
Assertion supexd ( 𝜑 → sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ V )

Proof

Step Hyp Ref Expression
1 supmo.1 ( 𝜑𝑅 Or 𝐴 )
2 df-sup sup ( 𝐵 , 𝐴 , 𝑅 ) = { 𝑥𝐴 ∣ ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) }
3 1 supmo ( 𝜑 → ∃* 𝑥𝐴 ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) )
4 rmorabex ( ∃* 𝑥𝐴 ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) → { 𝑥𝐴 ∣ ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) } ∈ V )
5 uniexg ( { 𝑥𝐴 ∣ ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) } ∈ V → { 𝑥𝐴 ∣ ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) } ∈ V )
6 3 4 5 3syl ( 𝜑 { 𝑥𝐴 ∣ ( ∀ 𝑦𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧𝐵 𝑦 𝑅 𝑧 ) ) } ∈ V )
7 2 6 eqeltrid ( 𝜑 → sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ V )