Theorem finxp0

Description: The value of Cartesian exponentiation at zero. (Contributed by ML, 24-Oct-2020)

	Ref	Expression
Assertion	finxp0	⊢ ( 𝑈 ↑↑ ∅ ) = ∅

Proof

Step	Hyp	Ref	Expression
1		0ex	⊢ ∅ ∈ V
2		vex	⊢ 𝑦 ∈ V
3	1 2	opnzi	⊢ ⟨ ∅ , 𝑦 ⟩ ≠ ∅
4	3	nesymi	⊢ ¬ ∅ = ⟨ ∅ , 𝑦 ⟩
5		peano1	⊢ ∅ ∈ ω
6		df-finxp	⊢ ( 𝑈 ↑↑ ∅ ) = { 𝑦 ∣ ( ∅ ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ ∅ , 𝑦 ⟩ ) ‘ ∅ ) ) }
7	6	abeq2i	⊢ ( 𝑦 ∈ ( 𝑈 ↑↑ ∅ ) ↔ ( ∅ ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ ∅ , 𝑦 ⟩ ) ‘ ∅ ) ) )
8	5 7	mpbiran	⊢ ( 𝑦 ∈ ( 𝑈 ↑↑ ∅ ) ↔ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ ∅ , 𝑦 ⟩ ) ‘ ∅ ) )
9		opex	⊢ ⟨ ∅ , 𝑦 ⟩ ∈ V
10	9	rdg0	⊢ ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ ∅ , 𝑦 ⟩ ) ‘ ∅ ) = ⟨ ∅ , 𝑦 ⟩
11	10	eqeq2i	⊢ ( ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ ∅ , 𝑦 ⟩ ) ‘ ∅ ) ↔ ∅ = ⟨ ∅ , 𝑦 ⟩ )
12	8 11	bitri	⊢ ( 𝑦 ∈ ( 𝑈 ↑↑ ∅ ) ↔ ∅ = ⟨ ∅ , 𝑦 ⟩ )
13	4 12	mtbir	⊢ ¬ 𝑦 ∈ ( 𝑈 ↑↑ ∅ )
14	13	nel0	⊢ ( 𝑈 ↑↑ ∅ ) = ∅