Theorem supeq1

Description: Equality theorem for supremum. (Contributed by NM, 22-May-1999)

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

Proof

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