finxp1o

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

		Ref	Expression
	Assertion	finxp1o	$⊢ U ↑↑ 1_{𝑜} = U$

Proof

Step	Hyp	Ref	Expression
1		1onn	$⊢ 1_{𝑜} \in ω$
2	1	a1i	$⊢ y \in U \to 1_{𝑜} \in ω$
3		finxpreclem1	$⊢ y \in U \to \emptyset = (n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))) (⟨1_{𝑜}, y⟩)$
4		1on	$⊢ 1_{𝑜} \in On$
5		1n0	$⊢ 1_{𝑜} \neq \emptyset$
6		nnlim	$⊢ 1_{𝑜} \in ω \to \neg Lim 1_{𝑜}$
7	1 6	ax-mp	$⊢ \neg Lim 1_{𝑜}$
8		rdgsucuni	$⊢ (1_{𝑜} \in On \land 1_{𝑜} \neq \emptyset \land \neg Lim 1_{𝑜}) \to rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨1_{𝑜}, y⟩) (1_{𝑜}) = (n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))) (rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨1_{𝑜}, y⟩) (⋃ 1_{𝑜}))$
9	4 5 7 8	mp3an	$⊢ rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨1_{𝑜}, y⟩) (1_{𝑜}) = (n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))) (rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨1_{𝑜}, y⟩) (⋃ 1_{𝑜}))$
10		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
11	10	unieqi	$⊢ ⋃ 1_{𝑜} = ⋃ suc \emptyset$
12		0elon	$⊢ \emptyset \in On$
13	12	onunisuci	$⊢ ⋃ suc \emptyset = \emptyset$
14	11 13	eqtri	$⊢ ⋃ 1_{𝑜} = \emptyset$
15	14	fveq2i	$⊢ rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨1_{𝑜}, y⟩) (⋃ 1_{𝑜}) = rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨1_{𝑜}, y⟩) (\emptyset)$
16		opex	$⊢ ⟨1_{𝑜}, y⟩ \in V$
17	16	rdg0	$⊢ rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨1_{𝑜}, y⟩) (\emptyset) = ⟨1_{𝑜}, y⟩$
18	15 17	eqtri	$⊢ rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨1_{𝑜}, y⟩) (⋃ 1_{𝑜}) = ⟨1_{𝑜}, y⟩$
19	18	fveq2i	$⊢ (n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))) (rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨1_{𝑜}, y⟩) (⋃ 1_{𝑜})) = (n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))) (⟨1_{𝑜}, y⟩)$
20	9 19	eqtri	$⊢ rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨1_{𝑜}, y⟩) (1_{𝑜}) = (n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))) (⟨1_{𝑜}, y⟩)$
21	3 20	eqtr4di	$⊢ y \in U \to \emptyset = rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨1_{𝑜}, y⟩) (1_{𝑜})$
22		df-finxp	$⊢ U ↑↑ 1_{𝑜} = \{y \| (1_{𝑜} \in ω \land \emptyset = rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨1_{𝑜}, y⟩) (1_{𝑜}))\}$
23	22	eqabri	$⊢ y \in U ↑↑ 1_{𝑜} \leftrightarrow (1_{𝑜} \in ω \land \emptyset = rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨1_{𝑜}, y⟩) (1_{𝑜}))$
24	2 21 23	sylanbrc	$⊢ y \in U \to y \in U ↑↑ 1_{𝑜}$
25	1 23	mpbiran	$⊢ y \in U ↑↑ 1_{𝑜} \leftrightarrow \emptyset = rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨1_{𝑜}, y⟩) (1_{𝑜})$
26		vex	$⊢ y \in V$
27	20	eqcomi	$⊢ (n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))) (⟨1_{𝑜}, y⟩) = rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨1_{𝑜}, y⟩) (1_{𝑜})$
28		finxpreclem2	$⊢ (y \in V \land \neg y \in U) \to \neg \emptyset = (n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))) (⟨1_{𝑜}, y⟩)$
29	28	neqned	$⊢ (y \in V \land \neg y \in U) \to \emptyset \neq (n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))) (⟨1_{𝑜}, y⟩)$
30	29	necomd	$⊢ (y \in V \land \neg y \in U) \to (n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))) (⟨1_{𝑜}, y⟩) \neq \emptyset$
31	27 30	eqnetrrid	$⊢ (y \in V \land \neg y \in U) \to rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨1_{𝑜}, y⟩) (1_{𝑜}) \neq \emptyset$
32	31	necomd	$⊢ (y \in V \land \neg y \in U) \to \emptyset \neq rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨1_{𝑜}, y⟩) (1_{𝑜})$
33	32	neneqd	$⊢ (y \in V \land \neg y \in U) \to \neg \emptyset = rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨1_{𝑜}, y⟩) (1_{𝑜})$
34	26 33	mpan	$⊢ \neg y \in U \to \neg \emptyset = rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨1_{𝑜}, y⟩) (1_{𝑜})$
35	34	con4i	$⊢ \emptyset = rec ((n \in ω, x \in V ⟼ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))), ⟨1_{𝑜}, y⟩) (1_{𝑜}) \to y \in U$
36	25 35	sylbi	$⊢ y \in U ↑↑ 1_{𝑜} \to y \in U$
37	24 36	impbii	$⊢ y \in U \leftrightarrow y \in U ↑↑ 1_{𝑜}$
38	37	eqriv	$⊢ U = U ↑↑ 1_{𝑜}$
39	38	eqcomi	$⊢ U ↑↑ 1_{𝑜} = U$

Metamath Proof Explorer

Theorem finxp1o

Proof