Metamath Proof Explorer

Theorem supeq123d

Description: Equality deduction for supremum. (Contributed by Stefan O'Rear, 20-Jan-2015)

Ref Expression
Hypotheses supeq123d.a ⊢ φ → A = D
supeq123d.b ⊢ φ → B = E
supeq123d.c ⊢ φ → C = F
Assertion supeq123d ⊢ φ → sup A B C = sup D E F

Proof

Step Hyp Ref Expression
1 supeq123d.a ⊢ φ → A = D
2 supeq123d.b ⊢ φ → B = E
3 supeq123d.c ⊢ φ → C = F
4 3 breqd ⊢ φ → x C y ↔ x F y
5 4 notbid ⊢ φ → ¬ x C y ↔ ¬ x F y
6 1 5 raleqbidv ⊢ φ → ∀ y ∈ A ¬ x C y ↔ ∀ y ∈ D ¬ x F y
7 3 breqd ⊢ φ → y C x ↔ y F x
8 3 breqd ⊢ φ → y C z ↔ y F z
9 1 8 rexeqbidv ⊢ φ → ∃ z ∈ A y C z ↔ ∃ z ∈ D y F z
10 7 9 imbi12d ⊢ φ → y C x → ∃ z ∈ A y C z ↔ y F x → ∃ z ∈ D y F z
11 2 10 raleqbidv ⊢ φ → ∀ y ∈ B y C x → ∃ z ∈ A y C z ↔ ∀ y ∈ E y F x → ∃ z ∈ D y F z
12 6 11 anbi12d ⊢ φ → ∀ y ∈ A ¬ x C y ∧ ∀ y ∈ B y C x → ∃ z ∈ A y C z ↔ ∀ y ∈ D ¬ x F y ∧ ∀ y ∈ E y F x → ∃ z ∈ D y F z
13 2 12 rabeqbidv ⊢ φ → x ∈ B | ∀ y ∈ A ¬ x C y ∧ ∀ y ∈ B y C x → ∃ z ∈ A y C z = x ∈ E | ∀ y ∈ D ¬ x F y ∧ ∀ y ∈ E y F x → ∃ z ∈ D y F z
14 13 unieqd ⊢ φ → ⋃ x ∈ B | ∀ y ∈ A ¬ x C y ∧ ∀ y ∈ B y C x → ∃ z ∈ A y C z = ⋃ x ∈ E | ∀ y ∈ D ¬ x F y ∧ ∀ y ∈ E y F x → ∃ z ∈ D y F z
15 df-sup ⊢ sup A B C = ⋃ x ∈ B | ∀ y ∈ A ¬ x C y ∧ ∀ y ∈ B y C x → ∃ z ∈ A y C z
16 df-sup ⊢ sup D E F = ⋃ x ∈ E | ∀ y ∈ D ¬ x F y ∧ ∀ y ∈ E y F x → ∃ z ∈ D y F z
17 14 15 16 3eqtr4g ⊢ φ → sup A B C = sup D E F