Theorem finxp1o

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

	Ref	Expression
Assertion	finxp1o	⊢ ( 𝑈 ↑↑ 1o ) = 𝑈

Proof

Step	Hyp	Ref	Expression
1		1onn	⊢ 1o ∈ ω
2	1	a1i	⊢ ( 𝑦 ∈ 𝑈 → 1o ∈ ω )
3		finxpreclem1	⊢ ( 𝑦 ∈ 𝑈 → ∅ = ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1o , 𝑦 ⟩ ) )
4		1on	⊢ 1o ∈ On
5		1n0	⊢ 1o ≠ ∅
6		nnlim	⊢ ( 1o ∈ ω → ¬ Lim 1o )
7	1 6	ax-mp	⊢ ¬ Lim 1o
8		rdgsucuni	⊢ ( ( 1o ∈ On ∧ 1o ≠ ∅ ∧ ¬ Lim 1o ) → ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 1o , 𝑦 ⟩ ) ‘ 1o ) = ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 1o , 𝑦 ⟩ ) ‘ ∪ 1o ) ) )
9	4 5 7 8	mp3an	⊢ ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 1o , 𝑦 ⟩ ) ‘ 1o ) = ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 1o , 𝑦 ⟩ ) ‘ ∪ 1o ) )
10		df-1o	⊢ 1o = suc ∅
11	10	unieqi	⊢ ∪ 1o = ∪ suc ∅
12		0elon	⊢ ∅ ∈ On
13	12	onunisuci	⊢ ∪ suc ∅ = ∅
14	11 13	eqtri	⊢ ∪ 1o = ∅
15	14	fveq2i	⊢ ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 1o , 𝑦 ⟩ ) ‘ ∪ 1o ) = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 1o , 𝑦 ⟩ ) ‘ ∅ )
16		opex	⊢ ⟨ 1o , 𝑦 ⟩ ∈ V
17	16	rdg0	⊢ ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 1o , 𝑦 ⟩ ) ‘ ∅ ) = ⟨ 1o , 𝑦 ⟩
18	15 17	eqtri	⊢ ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 1o , 𝑦 ⟩ ) ‘ ∪ 1o ) = ⟨ 1o , 𝑦 ⟩
19	18	fveq2i	⊢ ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 1o , 𝑦 ⟩ ) ‘ ∪ 1o ) ) = ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1o , 𝑦 ⟩ )
20	9 19	eqtri	⊢ ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 1o , 𝑦 ⟩ ) ‘ 1o ) = ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1o , 𝑦 ⟩ )
21	3 20	eqtr4di	⊢ ( 𝑦 ∈ 𝑈 → ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 1o , 𝑦 ⟩ ) ‘ 1o ) )
22		df-finxp	⊢ ( 𝑈 ↑↑ 1o ) = { 𝑦 ∣ ( 1o ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 1o , 𝑦 ⟩ ) ‘ 1o ) ) }
23	22	eqabri	⊢ ( 𝑦 ∈ ( 𝑈 ↑↑ 1o ) ↔ ( 1o ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 1o , 𝑦 ⟩ ) ‘ 1o ) ) )
24	2 21 23	sylanbrc	⊢ ( 𝑦 ∈ 𝑈 → 𝑦 ∈ ( 𝑈 ↑↑ 1o ) )
25	1 23	mpbiran	⊢ ( 𝑦 ∈ ( 𝑈 ↑↑ 1o ) ↔ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 1o , 𝑦 ⟩ ) ‘ 1o ) )
26		vex	⊢ 𝑦 ∈ V
27	20	eqcomi	⊢ ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1o , 𝑦 ⟩ ) = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 1o , 𝑦 ⟩ ) ‘ 1o )
28		finxpreclem2	⊢ ( ( 𝑦 ∈ V ∧ ¬ 𝑦 ∈ 𝑈 ) → ¬ ∅ = ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1o , 𝑦 ⟩ ) )
29	28	neqned	⊢ ( ( 𝑦 ∈ V ∧ ¬ 𝑦 ∈ 𝑈 ) → ∅ ≠ ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1o , 𝑦 ⟩ ) )
30	29	necomd	⊢ ( ( 𝑦 ∈ V ∧ ¬ 𝑦 ∈ 𝑈 ) → ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) ‘ ⟨ 1o , 𝑦 ⟩ ) ≠ ∅ )
31	27 30	eqnetrrid	⊢ ( ( 𝑦 ∈ V ∧ ¬ 𝑦 ∈ 𝑈 ) → ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 1o , 𝑦 ⟩ ) ‘ 1o ) ≠ ∅ )
32	31	necomd	⊢ ( ( 𝑦 ∈ V ∧ ¬ 𝑦 ∈ 𝑈 ) → ∅ ≠ ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 1o , 𝑦 ⟩ ) ‘ 1o ) )
33	32	neneqd	⊢ ( ( 𝑦 ∈ V ∧ ¬ 𝑦 ∈ 𝑈 ) → ¬ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 1o , 𝑦 ⟩ ) ‘ 1o ) )
34	26 33	mpan	⊢ ( ¬ 𝑦 ∈ 𝑈 → ¬ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 1o , 𝑦 ⟩ ) ‘ 1o ) )
35	34	con4i	⊢ ( ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 1o , 𝑦 ⟩ ) ‘ 1o ) → 𝑦 ∈ 𝑈 )
36	25 35	sylbi	⊢ ( 𝑦 ∈ ( 𝑈 ↑↑ 1o ) → 𝑦 ∈ 𝑈 )
37	24 36	impbii	⊢ ( 𝑦 ∈ 𝑈 ↔ 𝑦 ∈ ( 𝑈 ↑↑ 1o ) )
38	37	eqriv	⊢ 𝑈 = ( 𝑈 ↑↑ 1o )
39	38	eqcomi	⊢ ( 𝑈 ↑↑ 1o ) = 𝑈