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 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{A}$
nfixpw.2 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{B}$
Assertion nfixpw ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\underset{{x}\in {A}}{⨉}{B}$

Proof

Step Hyp Ref Expression
1 nfixpw.1 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{A}$
2 nfixpw.2 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{B}$
3 df-ixp ${⊢}\underset{{x}\in {A}}{⨉}{B}=\left\{{z}|\left({z}Fn\left\{{x}|{x}\in {A}\right\}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {B}\right)\right\}$
4 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{z}$
5 nfcv ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{x}$
6 5 1 nfel ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{x}\in {A}$
7 6 nfab ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left\{{x}|{x}\in {A}\right\}$
8 7 a1i ${⊢}\top \to \underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left\{{x}|{x}\in {A}\right\}$
9 8 mptru ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left\{{x}|{x}\in {A}\right\}$
10 4 9 nffn ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{z}Fn\left\{{x}|{x}\in {A}\right\}$
11 df-ral ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {B}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {z}\left({x}\right)\in {B}\right)$
12 nftru ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\top$
13 6 a1i ${⊢}\top \to Ⅎ{y}\phantom{\rule{.4em}{0ex}}{x}\in {A}$
14 4 a1i ${⊢}\top \to \underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{z}$
15 5 a1i ${⊢}\top \to \underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{x}$
16 14 15 nffvd ${⊢}\top \to \underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)$
17 2 a1i ${⊢}\top \to \underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{B}$
18 16 17 nfeld ${⊢}\top \to Ⅎ{y}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {B}$
19 13 18 nfimd ${⊢}\top \to Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {z}\left({x}\right)\in {B}\right)$
20 12 19 nfald ${⊢}\top \to Ⅎ{y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {z}\left({x}\right)\in {B}\right)$
21 20 mptru ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {z}\left({x}\right)\in {B}\right)$
22 11 21 nfxfr ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {B}$
23 10 22 nfan ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\left({z}Fn\left\{{x}|{x}\in {A}\right\}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {B}\right)$
24 23 nfab ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left\{{z}|\left({z}Fn\left\{{x}|{x}\in {A}\right\}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {B}\right)\right\}$
25 3 24 nfcxfr ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\underset{{x}\in {A}}{⨉}{B}$