Step |
Hyp |
Ref |
Expression |
1 |
|
df-mpo |
⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) } |
2 |
|
df-oprab |
⊢ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) } |
3 |
1 2
|
eqtri |
⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) } |
4 |
|
nel02 |
⊢ ( 𝐴 = ∅ → ¬ 𝑥 ∈ 𝐴 ) |
5 |
|
nel02 |
⊢ ( 𝐵 = ∅ → ¬ 𝑦 ∈ 𝐵 ) |
6 |
4 5
|
orim12i |
⊢ ( ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) → ( ¬ 𝑥 ∈ 𝐴 ∨ ¬ 𝑦 ∈ 𝐵 ) ) |
7 |
|
ianor |
⊢ ( ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( ¬ 𝑥 ∈ 𝐴 ∨ ¬ 𝑦 ∈ 𝐵 ) ) |
8 |
6 7
|
sylibr |
⊢ ( ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) → ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) |
9 |
|
simprl |
⊢ ( ( 𝑤 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) |
10 |
8 9
|
nsyl |
⊢ ( ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) → ¬ ( 𝑤 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) |
11 |
10
|
nexdv |
⊢ ( ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) → ¬ ∃ 𝑧 ( 𝑤 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) |
12 |
11
|
nexdv |
⊢ ( ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) → ¬ ∃ 𝑦 ∃ 𝑧 ( 𝑤 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) |
13 |
12
|
nexdv |
⊢ ( ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) → ¬ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) |
14 |
13
|
alrimiv |
⊢ ( ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) → ∀ 𝑤 ¬ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) |
15 |
|
ab0 |
⊢ ( { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) } = ∅ ↔ ∀ 𝑤 ¬ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) |
16 |
14 15
|
sylibr |
⊢ ( ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) → { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) } = ∅ ) |
17 |
3 16
|
syl5eq |
⊢ ( ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ∅ ) |