Metamath Proof Explorer


Theorem nfixpw

Description: Bound-variable hypothesis builder for indexed Cartesian product. Version of nfixp with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 15-Oct-2016) (Revised by Gino Giotto, 26-Jan-2024)

Ref Expression
Hypotheses nfixpw.1 𝑦 𝐴
nfixpw.2 𝑦 𝐵
Assertion nfixpw 𝑦 X 𝑥𝐴 𝐵

Proof

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 𝑥𝐴 𝐵