Step |
Hyp |
Ref |
Expression |
1 |
|
raleq |
⊢ ( 𝐵 = 𝐶 → ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ↔ ∀ 𝑦 ∈ 𝐶 ¬ 𝑥 𝑅 𝑦 ) ) |
2 |
|
rexeq |
⊢ ( 𝐵 = 𝐶 → ( ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ↔ ∃ 𝑧 ∈ 𝐶 𝑦 𝑅 𝑧 ) ) |
3 |
2
|
imbi2d |
⊢ ( 𝐵 = 𝐶 → ( ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ↔ ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐶 𝑦 𝑅 𝑧 ) ) ) |
4 |
3
|
ralbidv |
⊢ ( 𝐵 = 𝐶 → ( ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐶 𝑦 𝑅 𝑧 ) ) ) |
5 |
1 4
|
anbi12d |
⊢ ( 𝐵 = 𝐶 → ( ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝐶 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐶 𝑦 𝑅 𝑧 ) ) ) ) |
6 |
5
|
rabbidv |
⊢ ( 𝐵 = 𝐶 → { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } = { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐶 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐶 𝑦 𝑅 𝑧 ) ) } ) |
7 |
6
|
unieqd |
⊢ ( 𝐵 = 𝐶 → ∪ { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } = ∪ { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐶 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐶 𝑦 𝑅 𝑧 ) ) } ) |
8 |
|
df-sup |
⊢ sup ( 𝐵 , 𝐴 , 𝑅 ) = ∪ { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 𝑅 𝑧 ) ) } |
9 |
|
df-sup |
⊢ sup ( 𝐶 , 𝐴 , 𝑅 ) = ∪ { 𝑥 ∈ 𝐴 ∣ ( ∀ 𝑦 ∈ 𝐶 ¬ 𝑥 𝑅 𝑦 ∧ ∀ 𝑦 ∈ 𝐴 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ∈ 𝐶 𝑦 𝑅 𝑧 ) ) } |
10 |
7 8 9
|
3eqtr4g |
⊢ ( 𝐵 = 𝐶 → sup ( 𝐵 , 𝐴 , 𝑅 ) = sup ( 𝐶 , 𝐴 , 𝑅 ) ) |