Metamath Proof Explorer

Theorem supeq3

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

Ref Expression
Assertion supeq3 ⊢R=S→supABR=supABS

Proof

Step Hyp Ref Expression
1 breq ⊢R=S→xRy↔xSy
2 1 notbid ⊢R=S→¬xRy↔¬xSy
3 2 ralbidv ⊢R=S→∀y∈A¬xRy↔∀y∈A¬xSy
4 breq ⊢R=S→yRx↔ySx
5 breq ⊢R=S→yRz↔ySz
6 5 rexbidv ⊢R=S→∃z∈AyRz↔∃z∈AySz
7 4 6 imbi12d ⊢R=S→yRx→∃z∈AyRz↔ySx→∃z∈AySz
8 7 ralbidv ⊢R=S→∀y∈ByRx→∃z∈AyRz↔∀y∈BySx→∃z∈AySz
9 3 8 anbi12d ⊢R=S→∀y∈A¬xRy∧∀y∈ByRx→∃z∈AyRz↔∀y∈A¬xSy∧∀y∈BySx→∃z∈AySz
10 9 rabbidv ⊢R=S→x∈B|∀y∈A¬xRy∧∀y∈ByRx→∃z∈AyRz=x∈B|∀y∈A¬xSy∧∀y∈BySx→∃z∈AySz
11 10 unieqd ⊢R=S→⋃x∈B|∀y∈A¬xRy∧∀y∈ByRx→∃z∈AyRz=⋃x∈B|∀y∈A¬xSy∧∀y∈BySx→∃z∈AySz
12 df-sup ⊢supABR=⋃x∈B|∀y∈A¬xRy∧∀y∈ByRx→∃z∈AyRz
13 df-sup ⊢supABS=⋃x∈B|∀y∈A¬xSy∧∀y∈BySx→∃z∈AySz
14 11 12 13 3eqtr4g ⊢R=S→supABR=supABS