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

Metamath Proof Explorer

Theorem supeq123d

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

Ref Expression
Hypotheses supeq123d.a ⊢ ( 𝜑 → 𝐴 = 𝐷 )
supeq123d.b ⊢ ( 𝜑 → 𝐵 = 𝐸 )
supeq123d.c ⊢ ( 𝜑 → 𝐶 = 𝐹 )
Assertion supeq123d ( 𝜑 → sup ( 𝐴 , 𝐵 , 𝐶 ) = sup ( 𝐷 , 𝐸 , 𝐹 ) )

Proof

Step Hyp Ref Expression
1 supeq123d.a ⊢ ( 𝜑 → 𝐴 = 𝐷 )
2 supeq123d.b ⊢ ( 𝜑 → 𝐵 = 𝐸 )
3 supeq123d.c ⊢ ( 𝜑 → 𝐶 = 𝐹 )
4 3 breqd ⊢ ( 𝜑 → ( 𝑥 𝐶 𝑦 ↔ 𝑥 𝐹 𝑦 ) )
5 4 notbid ⊢ ( 𝜑 → ( ¬ 𝑥 𝐶 𝑦 ↔ ¬ 𝑥 𝐹 𝑦 ) )
6 1 5 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝐶 𝑦 ↔ ∀ 𝑦 ∈ 𝐷 ¬ 𝑥 𝐹 𝑦 ) )
7 3 breqd ⊢ ( 𝜑 → ( 𝑦 𝐶 𝑥 ↔ 𝑦 𝐹 𝑥 ) )
8 3 breqd ⊢ ( 𝜑 → ( 𝑦 𝐶 𝑧 ↔ 𝑦 𝐹 𝑧 ) )
9 1 8 rexeqbidv ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ 𝐴 𝑦 𝐶 𝑧 ↔ ∃ 𝑧 ∈ 𝐷 𝑦 𝐹 𝑧 ) )
10 7 9 imbi12d ⊢ ( 𝜑 → ( ( 𝑦 𝐶 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝐶 𝑧 ) ↔ ( 𝑦 𝐹 𝑥 → ∃ 𝑧 ∈ 𝐷 𝑦 𝐹 𝑧 ) ) )
11 2 10 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝐶 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝐶 𝑧 ) ↔ ∀ 𝑦 ∈ 𝐸 ( 𝑦 𝐹 𝑥 → ∃ 𝑧 ∈ 𝐷 𝑦 𝐹 𝑧 ) ) )
12 6 11 anbi12d ⊢ ( 𝜑 → ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝐶 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝐶 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝐶 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝐷 ¬ 𝑥 𝐹 𝑦 ∧ ∀ 𝑦 ∈ 𝐸 ( 𝑦 𝐹 𝑥 → ∃ 𝑧 ∈ 𝐷 𝑦 𝐹 𝑧 ) ) ) )
13 2 12 rabeqbidv ⊢ ( 𝜑 → { 𝑥 ∈ 𝐵 ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝐶 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝐶 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝐶 𝑧 ) ) } = { 𝑥 ∈ 𝐸 ∣ ( ∀ 𝑦 ∈ 𝐷 ¬ 𝑥 𝐹 𝑦 ∧ ∀ 𝑦 ∈ 𝐸 ( 𝑦 𝐹 𝑥 → ∃ 𝑧 ∈ 𝐷 𝑦 𝐹 𝑧 ) ) } )
14 13 unieqd ⊢ ( 𝜑 → ∪ { 𝑥 ∈ 𝐵 ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝐶 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝐶 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝐶 𝑧 ) ) } = ∪ { 𝑥 ∈ 𝐸 ∣ ( ∀ 𝑦 ∈ 𝐷 ¬ 𝑥 𝐹 𝑦 ∧ ∀ 𝑦 ∈ 𝐸 ( 𝑦 𝐹 𝑥 → ∃ 𝑧 ∈ 𝐷 𝑦 𝐹 𝑧 ) ) } )
15 df-sup ⊢ sup ( 𝐴 , 𝐵 , 𝐶 ) = ∪ { 𝑥 ∈ 𝐵 ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 𝐶 𝑦 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝐶 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 𝐶 𝑧 ) ) }
16 df-sup ⊢ sup ( 𝐷 , 𝐸 , 𝐹 ) = ∪ { 𝑥 ∈ 𝐸 ∣ ( ∀ 𝑦 ∈ 𝐷 ¬ 𝑥 𝐹 𝑦 ∧ ∀ 𝑦 ∈ 𝐸 ( 𝑦 𝐹 𝑥 → ∃ 𝑧 ∈ 𝐷 𝑦 𝐹 𝑧 ) ) }
17 14 15 16 3eqtr4g ⊢ ( 𝜑 → sup ( 𝐴 , 𝐵 , 𝐶 ) = sup ( 𝐷 , 𝐸 , 𝐹 ) )