nfixp

Description: Bound-variable hypothesis builder for indexed Cartesian product. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfixpw when possible. (Contributed by Mario Carneiro, 15-Oct-2016) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nfixp.1	$⊢ \underline{Ⅎ} y A$
	nfixp.2	$⊢ \underline{Ⅎ} y B$
Assertion	nfixp	$⊢ \underline{Ⅎ} y \underset{x \in A}{⨉} B$

Proof

Step	Hyp	Ref	Expression
1		nfixp.1	$⊢ \underline{Ⅎ} y A$
2		nfixp.2	$⊢ \underline{Ⅎ} y B$
3		df-ixp	$⊢ \underset{x \in A}{⨉} B = \{z \| (z Fn \{x \| x \in A\} \land \forall x \in A z (x) \in B)\}$
4		nfcv	$⊢ \underline{Ⅎ} y z$
5		nftru	$⊢ Ⅎ x ⊤$
6		nfcvf	$⊢ \neg \forall y y = x \to \underline{Ⅎ} y x$
7	6	adantl	$⊢ (⊤ \land \neg \forall y y = x) \to \underline{Ⅎ} y x$
8	1	a1i	$⊢ (⊤ \land \neg \forall y y = x) \to \underline{Ⅎ} y A$
9	7 8	nfeld	$⊢ (⊤ \land \neg \forall y y = x) \to Ⅎ y x \in A$
10	5 9	nfabd2	$⊢ ⊤ \to \underline{Ⅎ} y \{x \| x \in A\}$
11	10	mptru	$⊢ \underline{Ⅎ} y \{x \| x \in A\}$
12	4 11	nffn	$⊢ Ⅎ y z Fn \{x \| x \in A\}$
13		df-ral	$⊢ \forall x \in A z (x) \in B \leftrightarrow \forall x (x \in A \to z (x) \in B)$
14	4	a1i	$⊢ (⊤ \land \neg \forall y y = x) \to \underline{Ⅎ} y z$
15	14 7	nffvd	$⊢ (⊤ \land \neg \forall y y = x) \to \underline{Ⅎ} y z (x)$
16	2	a1i	$⊢ (⊤ \land \neg \forall y y = x) \to \underline{Ⅎ} y B$
17	15 16	nfeld	$⊢ (⊤ \land \neg \forall y y = x) \to Ⅎ y z (x) \in B$
18	9 17	nfimd	$⊢ (⊤ \land \neg \forall y y = x) \to Ⅎ y (x \in A \to z (x) \in B)$
19	5 18	nfald2	$⊢ ⊤ \to Ⅎ y \forall x (x \in A \to z (x) \in B)$
20	19	mptru	$⊢ Ⅎ y \forall x (x \in A \to z (x) \in B)$
21	13 20	nfxfr	$⊢ Ⅎ y \forall x \in A z (x) \in B$
22	12 21	nfan	$⊢ Ⅎ y (z Fn \{x \| x \in A\} \land \forall x \in A z (x) \in B)$
23	22	nfab	$⊢ \underline{Ⅎ} y \{z \| (z Fn \{x \| x \in A\} \land \forall x \in A z (x) \in B)\}$
24	3 23	nfcxfr	$⊢ \underline{Ⅎ} y \underset{x \in A}{⨉} B$

Metamath Proof Explorer

Theorem nfixp

Proof