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	⊢ 𝐹 = ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) )
Assertion	dffinxpf	⊢ ( 𝑈 ↑↑ 𝑁 ) = { 𝑦 ∣ ( 𝑁 ∈ ω ∧ ∅ = ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) }

Proof

Step	Hyp	Ref	Expression
1		dffinxpf.1	⊢ 𝐹 = ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) )
2		df-finxp	⊢ ( 𝑈 ↑↑ 𝑁 ) = { 𝑦 ∣ ( 𝑁 ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) }
3		rdgeq1	⊢ ( 𝐹 = ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) → rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) = rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) )
4	1 3	ax-mp	⊢ rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) = rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ )
5	4	fveq1i	⊢ ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 )
6	5	eqeq2i	⊢ ( ∅ = ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ↔ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) )
7	6	anbi2i	⊢ ( ( 𝑁 ∈ ω ∧ ∅ = ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) ↔ ( 𝑁 ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) )
8	7	abbii	⊢ { 𝑦 ∣ ( 𝑁 ∈ ω ∧ ∅ = ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) } = { 𝑦 ∣ ( 𝑁 ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) }
9	2 8	eqtr4i	⊢ ( 𝑈 ↑↑ 𝑁 ) = { 𝑦 ∣ ( 𝑁 ∈ ω ∧ ∅ = ( rec ( 𝐹 , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) }