Step |
Hyp |
Ref |
Expression |
1 |
|
df-supp |
⊢ supp = ( 𝑥 ∈ V , 𝑧 ∈ V ↦ { 𝑖 ∈ dom 𝑥 ∣ ( 𝑥 “ { 𝑖 } ) ≠ { 𝑧 } } ) |
2 |
1
|
a1i |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → supp = ( 𝑥 ∈ V , 𝑧 ∈ V ↦ { 𝑖 ∈ dom 𝑥 ∣ ( 𝑥 “ { 𝑖 } ) ≠ { 𝑧 } } ) ) |
3 |
|
dmeq |
⊢ ( 𝑥 = 𝑋 → dom 𝑥 = dom 𝑋 ) |
4 |
3
|
adantr |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑧 = 𝑍 ) → dom 𝑥 = dom 𝑋 ) |
5 |
|
imaeq1 |
⊢ ( 𝑥 = 𝑋 → ( 𝑥 “ { 𝑖 } ) = ( 𝑋 “ { 𝑖 } ) ) |
6 |
5
|
adantr |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑧 = 𝑍 ) → ( 𝑥 “ { 𝑖 } ) = ( 𝑋 “ { 𝑖 } ) ) |
7 |
|
sneq |
⊢ ( 𝑧 = 𝑍 → { 𝑧 } = { 𝑍 } ) |
8 |
7
|
adantl |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑧 = 𝑍 ) → { 𝑧 } = { 𝑍 } ) |
9 |
6 8
|
neeq12d |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑧 = 𝑍 ) → ( ( 𝑥 “ { 𝑖 } ) ≠ { 𝑧 } ↔ ( 𝑋 “ { 𝑖 } ) ≠ { 𝑍 } ) ) |
10 |
4 9
|
rabeqbidv |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑧 = 𝑍 ) → { 𝑖 ∈ dom 𝑥 ∣ ( 𝑥 “ { 𝑖 } ) ≠ { 𝑧 } } = { 𝑖 ∈ dom 𝑋 ∣ ( 𝑋 “ { 𝑖 } ) ≠ { 𝑍 } } ) |
11 |
10
|
adantl |
⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) ∧ ( 𝑥 = 𝑋 ∧ 𝑧 = 𝑍 ) ) → { 𝑖 ∈ dom 𝑥 ∣ ( 𝑥 “ { 𝑖 } ) ≠ { 𝑧 } } = { 𝑖 ∈ dom 𝑋 ∣ ( 𝑋 “ { 𝑖 } ) ≠ { 𝑍 } } ) |
12 |
|
elex |
⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ V ) |
13 |
12
|
adantr |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → 𝑋 ∈ V ) |
14 |
|
elex |
⊢ ( 𝑍 ∈ 𝑊 → 𝑍 ∈ V ) |
15 |
14
|
adantl |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → 𝑍 ∈ V ) |
16 |
|
dmexg |
⊢ ( 𝑋 ∈ 𝑉 → dom 𝑋 ∈ V ) |
17 |
16
|
adantr |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → dom 𝑋 ∈ V ) |
18 |
|
rabexg |
⊢ ( dom 𝑋 ∈ V → { 𝑖 ∈ dom 𝑋 ∣ ( 𝑋 “ { 𝑖 } ) ≠ { 𝑍 } } ∈ V ) |
19 |
17 18
|
syl |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → { 𝑖 ∈ dom 𝑋 ∣ ( 𝑋 “ { 𝑖 } ) ≠ { 𝑍 } } ∈ V ) |
20 |
2 11 13 15 19
|
ovmpod |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊 ) → ( 𝑋 supp 𝑍 ) = { 𝑖 ∈ dom 𝑋 ∣ ( 𝑋 “ { 𝑖 } ) ≠ { 𝑍 } } ) |