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 ( 𝐷 , 𝐸 , 𝐹 ) )