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

Metamath Proof Explorer

Theorem supeq2

Description: Equality theorem for supremum. (Contributed by Jeff Madsen, 2-Sep-2009)

		Ref	Expression
	Assertion	supeq2	⊢ ( 𝐵 = 𝐶 → sup ( 𝐴 , 𝐵 , 𝑅 ) = sup ( 𝐴 , 𝐶 , 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		rabeq	⊢ ( 𝐵 = 𝐶 → { 𝑥 ∈ 𝐵 ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ) } = { 𝑥 ∈ 𝐶 ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ) } )
2		raleq	⊢ ( 𝐵 = 𝐶 → ( ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ↔ ∀ 𝑦 ∈ 𝐶 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ) )
3	2	anbi2d	⊢ ( 𝐵 = 𝐶 → ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ) ) )
4	3	rabbidv	⊢ ( 𝐵 = 𝐶 → { 𝑥 ∈ 𝐶 ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ) } = { 𝑥 ∈ 𝐶 ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ) } )
5	1 4	eqtrd	⊢ ( 𝐵 = 𝐶 → { 𝑥 ∈ 𝐵 ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ) } = { 𝑥 ∈ 𝐶 ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ) } )
6	5	unieqd	⊢ ( 𝐵 = 𝐶 → ∪ { 𝑥 ∈ 𝐵 ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ) } = ∪ { 𝑥 ∈ 𝐶 ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ) } )
7		df-sup	⊢ sup ( 𝐴 , 𝐵 , 𝑅 ) = ∪ { 𝑥 ∈ 𝐵 ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ) }
8		df-sup	⊢ sup ( 𝐴 , 𝐶 , 𝑅 ) = ∪ { 𝑥 ∈ 𝐶 ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐶 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ) }
9	6 7 8	3eqtr4g	⊢ ( 𝐵 = 𝐶 → sup ( 𝐴 , 𝐵 , 𝑅 ) = sup ( 𝐴 , 𝐶 , 𝑅 ) )