Metamath Proof Explorer

Theorem dffinxpf

Description: This theorem is the same as Definition df-finxp , except that the large function is replaced by a class variable for brevity. (Contributed by ML, 24-Oct-2020)

Ref Expression
Hypothesis dffinxpf.1 ⊢F=n∈ω,x∈V⟼ifn=1𝑜∧x∈U∅ifx∈V×U⋃n1st⁡xnx
Assertion dffinxpf ⊢U↑↑N=y|N∈ω∧∅=rec⁡FNy⁡N

Proof

Step Hyp Ref Expression
1 dffinxpf.1 ⊢F=n∈ω,x∈V⟼ifn=1𝑜∧x∈U∅ifx∈V×U⋃n1st⁡xnx
2 df-finxp ⊢U↑↑N=y|N∈ω∧∅=rec⁡n∈ω,x∈V⟼ifn=1𝑜∧x∈U∅ifx∈V×U⋃n1st⁡xnxNy⁡N
3 rdgeq1 ⊢F=n∈ω,x∈V⟼ifn=1𝑜∧x∈U∅ifx∈V×U⋃n1st⁡xnx→rec⁡FNy=rec⁡n∈ω,x∈V⟼ifn=1𝑜∧x∈U∅ifx∈V×U⋃n1st⁡xnxNy
4 1 3 ax-mp ⊢rec⁡FNy=rec⁡n∈ω,x∈V⟼ifn=1𝑜∧x∈U∅ifx∈V×U⋃n1st⁡xnxNy
5 4 fveq1i ⊢rec⁡FNy⁡N=rec⁡n∈ω,x∈V⟼ifn=1𝑜∧x∈U∅ifx∈V×U⋃n1st⁡xnxNy⁡N
6 5 eqeq2i ⊢∅=rec⁡FNy⁡N↔∅=rec⁡n∈ω,x∈V⟼ifn=1𝑜∧x∈U∅ifx∈V×U⋃n1st⁡xnxNy⁡N
7 6 anbi2i ⊢N∈ω∧∅=rec⁡FNy⁡N↔N∈ω∧∅=rec⁡n∈ω,x∈V⟼ifn=1𝑜∧x∈U∅ifx∈V×U⋃n1st⁡xnxNy⁡N
8 7 abbii ⊢y|N∈ω∧∅=rec⁡FNy⁡N=y|N∈ω∧∅=rec⁡n∈ω,x∈V⟼ifn=1𝑜∧x∈U∅ifx∈V×U⋃n1st⁡xnxNy⁡N
9 2 8 eqtr4i ⊢U↑↑N=y|N∈ω∧∅=rec⁡FNy⁡N