Metamath Proof Explorer


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 ( 𝐶 , 𝐴 , 𝑅 ) )