Step |
Hyp |
Ref |
Expression |
1 |
|
nfixpw.1 |
⊢ Ⅎ 𝑦 𝐴 |
2 |
|
nfixpw.2 |
⊢ Ⅎ 𝑦 𝐵 |
3 |
|
df-ixp |
⊢ X 𝑥 ∈ 𝐴 𝐵 = { 𝑧 ∣ ( 𝑧 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ) } |
4 |
|
nfcv |
⊢ Ⅎ 𝑦 𝑧 |
5 |
|
nfcv |
⊢ Ⅎ 𝑦 𝑥 |
6 |
5 1
|
nfel |
⊢ Ⅎ 𝑦 𝑥 ∈ 𝐴 |
7 |
6
|
nfab |
⊢ Ⅎ 𝑦 { 𝑥 ∣ 𝑥 ∈ 𝐴 } |
8 |
7
|
a1i |
⊢ ( ⊤ → Ⅎ 𝑦 { 𝑥 ∣ 𝑥 ∈ 𝐴 } ) |
9 |
8
|
mptru |
⊢ Ⅎ 𝑦 { 𝑥 ∣ 𝑥 ∈ 𝐴 } |
10 |
4 9
|
nffn |
⊢ Ⅎ 𝑦 𝑧 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 } |
11 |
|
df-ral |
⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ) ) |
12 |
|
nftru |
⊢ Ⅎ 𝑥 ⊤ |
13 |
6
|
a1i |
⊢ ( ⊤ → Ⅎ 𝑦 𝑥 ∈ 𝐴 ) |
14 |
4
|
a1i |
⊢ ( ⊤ → Ⅎ 𝑦 𝑧 ) |
15 |
5
|
a1i |
⊢ ( ⊤ → Ⅎ 𝑦 𝑥 ) |
16 |
14 15
|
nffvd |
⊢ ( ⊤ → Ⅎ 𝑦 ( 𝑧 ‘ 𝑥 ) ) |
17 |
2
|
a1i |
⊢ ( ⊤ → Ⅎ 𝑦 𝐵 ) |
18 |
16 17
|
nfeld |
⊢ ( ⊤ → Ⅎ 𝑦 ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ) |
19 |
13 18
|
nfimd |
⊢ ( ⊤ → Ⅎ 𝑦 ( 𝑥 ∈ 𝐴 → ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ) ) |
20 |
12 19
|
nfald |
⊢ ( ⊤ → Ⅎ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ) ) |
21 |
20
|
mptru |
⊢ Ⅎ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ) |
22 |
11 21
|
nfxfr |
⊢ Ⅎ 𝑦 ∀ 𝑥 ∈ 𝐴 ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 |
23 |
10 22
|
nfan |
⊢ Ⅎ 𝑦 ( 𝑧 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ) |
24 |
23
|
nfab |
⊢ Ⅎ 𝑦 { 𝑧 ∣ ( 𝑧 Fn { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ) } |
25 |
3 24
|
nfcxfr |
⊢ Ⅎ 𝑦 X 𝑥 ∈ 𝐴 𝐵 |