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

Metamath Proof Explorer

Theorem supeq3

Description: Equality theorem for supremum. (Contributed by Scott Fenton, 13-Jun-2018)

Ref Expression
Assertion supeq3 ( 𝑅 = 𝑆 → sup ( 𝐴 , 𝐵 , 𝑅 ) = sup ( 𝐴 , 𝐵 , 𝑆 ) )

Proof

Step Hyp Ref Expression
1 breq ⊢ ( 𝑅 = 𝑆 → ( 𝑥 𝑅 𝑦 ↔ 𝑥 𝑆 𝑦 ) )
2 1 notbid ⊢ ( 𝑅 = 𝑆 → ( ¬ 𝑥 𝑅 𝑦 ↔ ¬ 𝑥 𝑆 𝑦 ) )
3 2 ralbidv ⊢ ( 𝑅 = 𝑆 → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑆 𝑦 ) )
4 breq ⊢ ( 𝑅 = 𝑆 → ( 𝑦 𝑅 𝑥 ↔ 𝑦 𝑆 𝑥 ) )
5 breq ⊢ ( 𝑅 = 𝑆 → ( 𝑦 𝑅 𝑧 ↔ 𝑦 𝑆 𝑧 ) )
6 5 rexbidv ⊢ ( 𝑅 = 𝑆 → ( ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ↔ ∃ 𝑧 ∈ 𝐴 𝑦 𝑆 𝑧 ) )
7 4 6 imbi12d ⊢ ( 𝑅 = 𝑆 → ( ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ↔ ( 𝑦 𝑆 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑆 𝑧 ) ) )
8 7 ralbidv ⊢ ( 𝑅 = 𝑆 → ( ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑆 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑆 𝑧 ) ) )
9 3 8 anbi12d ⊢ ( 𝑅 = 𝑆 → ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑆 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑆 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑆 𝑧 ) ) ) )
10 9 rabbidv ⊢ ( 𝑅 = 𝑆 → { 𝑥 ∈ 𝐵 ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ) } = { 𝑥 ∈ 𝐵 ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑆 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑆 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑆 𝑧 ) ) } )
11 10 unieqd ⊢ ( 𝑅 = 𝑆 → ∪ { 𝑥 ∈ 𝐵 ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ) } = ∪ { 𝑥 ∈ 𝐵 ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑆 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑆 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑆 𝑧 ) ) } )
12 df-sup ⊢ sup ( 𝐴 , 𝐵 , 𝑅 ) = ∪ { 𝑥 ∈ 𝐵 ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑅 𝑧 ) ) }
13 df-sup ⊢ sup ( 𝐴 , 𝐵 , 𝑆 ) = ∪ { 𝑥 ∈ 𝐵 ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝑆 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑆 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝑆 𝑧 ) ) }
14 11 12 13 3eqtr4g ⊢ ( 𝑅 = 𝑆 → sup ( 𝐴 , 𝐵 , 𝑅 ) = sup ( 𝐴 , 𝐵 , 𝑆 ) )