Step |
Hyp |
Ref |
Expression |
1 |
|
fvconst0ci.1 |
⊢ 𝐵 ∈ V |
2 |
|
fvconst0ci.2 |
⊢ 𝑌 = ( ( 𝐴 × { 𝐵 } ) ‘ 𝑋 ) |
3 |
|
dmxpss |
⊢ dom ( 𝐴 × { 𝐵 } ) ⊆ 𝐴 |
4 |
3
|
sseli |
⊢ ( 𝑋 ∈ dom ( 𝐴 × { 𝐵 } ) → 𝑋 ∈ 𝐴 ) |
5 |
1
|
fvconst2 |
⊢ ( 𝑋 ∈ 𝐴 → ( ( 𝐴 × { 𝐵 } ) ‘ 𝑋 ) = 𝐵 ) |
6 |
4 5
|
syl |
⊢ ( 𝑋 ∈ dom ( 𝐴 × { 𝐵 } ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝑋 ) = 𝐵 ) |
7 |
2 6
|
eqtrid |
⊢ ( 𝑋 ∈ dom ( 𝐴 × { 𝐵 } ) → 𝑌 = 𝐵 ) |
8 |
7
|
olcd |
⊢ ( 𝑋 ∈ dom ( 𝐴 × { 𝐵 } ) → ( 𝑌 = ∅ ∨ 𝑌 = 𝐵 ) ) |
9 |
|
ndmfv |
⊢ ( ¬ 𝑋 ∈ dom ( 𝐴 × { 𝐵 } ) → ( ( 𝐴 × { 𝐵 } ) ‘ 𝑋 ) = ∅ ) |
10 |
2 9
|
eqtrid |
⊢ ( ¬ 𝑋 ∈ dom ( 𝐴 × { 𝐵 } ) → 𝑌 = ∅ ) |
11 |
10
|
orcd |
⊢ ( ¬ 𝑋 ∈ dom ( 𝐴 × { 𝐵 } ) → ( 𝑌 = ∅ ∨ 𝑌 = 𝐵 ) ) |
12 |
8 11
|
pm2.61i |
⊢ ( 𝑌 = ∅ ∨ 𝑌 = 𝐵 ) |