This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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) Avoid ax-13 . (Revised by GG, 26-Jan-2024)

Ref Expression
Hypotheses nfixpw.1 ⊢ Ⅎ _ y A
nfixpw.2 ⊢ Ⅎ _ y B
Assertion nfixpw ⊢ Ⅎ _ y ⨉ x ∈ A B

Proof

Step Hyp Ref Expression
1 nfixpw.1 ⊢ Ⅎ _ y A
2 nfixpw.2 ⊢ Ⅎ _ y B
3 df-ixp ⊢ ⨉ x ∈ A B = z | z Fn x | x ∈ A ∧ ∀ x ∈ A z ⁡ x ∈ B
4 nfcv ⊢ Ⅎ _ y z
5 nfcv ⊢ Ⅎ _ y x
6 5 1 nfel ⊢ Ⅎ y x ∈ A
7 6 nfab ⊢ Ⅎ _ y x | x ∈ A
8 7 a1i ⊢ ⊤ → Ⅎ _ y x | x ∈ A
9 8 mptru ⊢ Ⅎ _ y x | x ∈ A
10 4 9 nffn ⊢ Ⅎ y z Fn x | x ∈ A
11 df-ral ⊢ ∀ x ∈ A z ⁡ x ∈ B ↔ ∀ x x ∈ A → z ⁡ x ∈ B
12 nftru ⊢ Ⅎ x ⊤
13 6 a1i ⊢ ⊤ → Ⅎ y x ∈ A
14 4 a1i ⊢ ⊤ → Ⅎ _ y z
15 5 a1i ⊢ ⊤ → Ⅎ _ y x
16 14 15 nffvd ⊢ ⊤ → Ⅎ _ y z ⁡ x
17 2 a1i ⊢ ⊤ → Ⅎ _ y B
18 16 17 nfeld ⊢ ⊤ → Ⅎ y z ⁡ x ∈ B
19 13 18 nfimd ⊢ ⊤ → Ⅎ y x ∈ A → z ⁡ x ∈ B
20 12 19 nfald ⊢ ⊤ → Ⅎ y ∀ x x ∈ A → z ⁡ x ∈ B
21 20 mptru ⊢ Ⅎ y ∀ x x ∈ A → z ⁡ x ∈ B
22 11 21 nfxfr ⊢ Ⅎ y ∀ x ∈ A z ⁡ x ∈ B
23 10 22 nfan ⊢ Ⅎ y z Fn x | x ∈ A ∧ ∀ x ∈ A z ⁡ x ∈ B
24 23 nfab ⊢ Ⅎ _ y z | z Fn x | x ∈ A ∧ ∀ x ∈ A z ⁡ x ∈ B
25 3 24 nfcxfr ⊢ Ⅎ _ y ⨉ x ∈ A B