Theorem supex2g

Description: Existence of supremum. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Assertion	supex2g	⊢ ( 𝐴 ∈ 𝐶 → sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		df-sup	⊢ sup ( 𝐵 , 𝐴 , 𝑅 ) = ∪ { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) }
2		rabexg	⊢ ( 𝐴 ∈ 𝐶 → { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } ∈ V )
3	2	uniexd	⊢ ( 𝐴 ∈ 𝐶 → ∪ { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } ∈ V )
4	1 3	eqeltrid	⊢ ( 𝐴 ∈ 𝐶 → sup ( 𝐵 , 𝐴 , 𝑅 ) ∈ V )