finxpsuclem

		Ref	Expression
	Hypothesis	finxpsuclem.1	$⊢ F = (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⟩)))$
	Assertion	finxpsuclem	$⊢ (N \in ω \land 1_{𝑜} \subseteq N) \to U ↑↑ suc N = U ↑↑ N \times U$

Proof

Step	Hyp	Ref	Expression
1		finxpsuclem.1	$⊢ F = (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⟩)))$
2		peano2	$⊢ N \in ω \to suc N \in ω$
3	2	adantr	$⊢ (N \in ω \land 1_{𝑜} \subseteq N) \to suc N \in ω$
4		1on	$⊢ 1_{𝑜} \in On$
5	4	onordi	$⊢ Ord 1_{𝑜}$
6		nnord	$⊢ N \in ω \to Ord N$
7		ordsseleq	$⊢ (Ord 1_{𝑜} \land Ord N) \to (1_{𝑜} \subseteq N \leftrightarrow (1_{𝑜} \in N \lor 1_{𝑜} = N))$
8	5 6 7	sylancr	$⊢ N \in ω \to (1_{𝑜} \subseteq N \leftrightarrow (1_{𝑜} \in N \lor 1_{𝑜} = N))$
9	8	biimpa	$⊢ (N \in ω \land 1_{𝑜} \subseteq N) \to (1_{𝑜} \in N \lor 1_{𝑜} = N)$
10		elelsuc	$⊢ 1_{𝑜} \in N \to 1_{𝑜} \in suc N$
11	10	a1i	$⊢ N \in ω \to (1_{𝑜} \in N \to 1_{𝑜} \in suc N)$
12		sucidg	$⊢ N \in ω \to N \in suc N$
13		eleq1	$⊢ 1_{𝑜} = N \to (1_{𝑜} \in suc N \leftrightarrow N \in suc N)$
14	12 13	syl5ibrcom	$⊢ N \in ω \to (1_{𝑜} = N \to 1_{𝑜} \in suc N)$
15	11 14	jaod	$⊢ N \in ω \to ((1_{𝑜} \in N \lor 1_{𝑜} = N) \to 1_{𝑜} \in suc N)$
16	15	adantr	$⊢ (N \in ω \land 1_{𝑜} \subseteq N) \to ((1_{𝑜} \in N \lor 1_{𝑜} = N) \to 1_{𝑜} \in suc N)$
17	9 16	mpd	$⊢ (N \in ω \land 1_{𝑜} \subseteq N) \to 1_{𝑜} \in suc N$
18	1	finxpreclem6	$⊢ (suc N \in ω \land 1_{𝑜} \in suc N) \to U ↑↑ suc N \subseteq V \times U$
19	3 17 18	syl2anc	$⊢ (N \in ω \land 1_{𝑜} \subseteq N) \to U ↑↑ suc N \subseteq V \times U$
20	19	sselda	$⊢ ((N \in ω \land 1_{𝑜} \subseteq N) \land y \in U ↑↑ suc N) \to y \in (V \times U)$
21	2	ad2antrr	$⊢ ((N \in ω \land 1_{𝑜} \subseteq N) \land y \in (V \times U)) \to suc N \in ω$
22		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
23		ordsucsssuc	$⊢ (Ord 1_{𝑜} \land Ord N) \to (1_{𝑜} \subseteq N \leftrightarrow suc 1_{𝑜} \subseteq suc N)$
24	5 6 23	sylancr	$⊢ N \in ω \to (1_{𝑜} \subseteq N \leftrightarrow suc 1_{𝑜} \subseteq suc N)$
25	24	biimpa	$⊢ (N \in ω \land 1_{𝑜} \subseteq N) \to suc 1_{𝑜} \subseteq suc N$
26	22 25	eqsstrid	$⊢ (N \in ω \land 1_{𝑜} \subseteq N) \to 2_{𝑜} \subseteq suc N$
27	26	adantr	$⊢ ((N \in ω \land 1_{𝑜} \subseteq N) \land y \in (V \times U)) \to 2_{𝑜} \subseteq suc N$
28		simpr	$⊢ ((N \in ω \land 1_{𝑜} \subseteq N) \land y \in (V \times U)) \to y \in (V \times U)$
29	1	finxpreclem4	$⊢ ((suc N \in ω \land 2_{𝑜} \subseteq suc N) \land y \in (V \times U)) \to rec (F, ⟨suc N, y⟩) (suc N) = rec (F, ⟨⋃ suc N, 1^{st} (y)⟩) (⋃ suc N)$
30	21 27 28 29	syl21anc	$⊢ ((N \in ω \land 1_{𝑜} \subseteq N) \land y \in (V \times U)) \to rec (F, ⟨suc N, y⟩) (suc N) = rec (F, ⟨⋃ suc N, 1^{st} (y)⟩) (⋃ suc N)$
31		ordunisuc	$⊢ Ord N \to ⋃ suc N = N$
32	6 31	syl	$⊢ N \in ω \to ⋃ suc N = N$
33		opeq1	$⊢ ⋃ suc N = N \to ⟨⋃ suc N, 1^{st} (y)⟩ = ⟨N, 1^{st} (y)⟩$
34		rdgeq2	$⊢ ⟨⋃ suc N, 1^{st} (y)⟩ = ⟨N, 1^{st} (y)⟩ \to rec (F, ⟨⋃ suc N, 1^{st} (y)⟩) = rec (F, ⟨N, 1^{st} (y)⟩)$
35	33 34	syl	$⊢ ⋃ suc N = N \to rec (F, ⟨⋃ suc N, 1^{st} (y)⟩) = rec (F, ⟨N, 1^{st} (y)⟩)$
36	32 35	syl	$⊢ N \in ω \to rec (F, ⟨⋃ suc N, 1^{st} (y)⟩) = rec (F, ⟨N, 1^{st} (y)⟩)$
37	36 32	fveq12d	$⊢ N \in ω \to rec (F, ⟨⋃ suc N, 1^{st} (y)⟩) (⋃ suc N) = rec (F, ⟨N, 1^{st} (y)⟩) (N)$
38	37	ad2antrr	$⊢ ((N \in ω \land 1_{𝑜} \subseteq N) \land y \in (V \times U)) \to rec (F, ⟨⋃ suc N, 1^{st} (y)⟩) (⋃ suc N) = rec (F, ⟨N, 1^{st} (y)⟩) (N)$
39	30 38	eqtrd	$⊢ ((N \in ω \land 1_{𝑜} \subseteq N) \land y \in (V \times U)) \to rec (F, ⟨suc N, y⟩) (suc N) = rec (F, ⟨N, 1^{st} (y)⟩) (N)$
40	39	eqeq2d	$⊢ ((N \in ω \land 1_{𝑜} \subseteq N) \land y \in (V \times U)) \to (\emptyset = rec (F, ⟨suc N, y⟩) (suc N) \leftrightarrow \emptyset = rec (F, ⟨N, 1^{st} (y)⟩) (N))$
41	1	dffinxpf	$⊢ U ↑↑ suc N = \{y \| (suc N \in ω \land \emptyset = rec (F, ⟨suc N, y⟩) (suc N))\}$
42	41	abeq2i	$⊢ y \in U ↑↑ suc N \leftrightarrow (suc N \in ω \land \emptyset = rec (F, ⟨suc N, y⟩) (suc N))$
43	2	biantrurd	$⊢ N \in ω \to (\emptyset = rec (F, ⟨suc N, y⟩) (suc N) \leftrightarrow (suc N \in ω \land \emptyset = rec (F, ⟨suc N, y⟩) (suc N)))$
44	42 43	bitr4id	$⊢ N \in ω \to (y \in U ↑↑ suc N \leftrightarrow \emptyset = rec (F, ⟨suc N, y⟩) (suc N))$
45	44	ad2antrr	$⊢ ((N \in ω \land 1_{𝑜} \subseteq N) \land y \in (V \times U)) \to (y \in U ↑↑ suc N \leftrightarrow \emptyset = rec (F, ⟨suc N, y⟩) (suc N))$
46		fvex	$⊢ 1^{st} (y) \in V$
47		opeq2	$⊢ z = 1^{st} (y) \to ⟨N, z⟩ = ⟨N, 1^{st} (y)⟩$
48		rdgeq2	$⊢ ⟨N, z⟩ = ⟨N, 1^{st} (y)⟩ \to rec (F, ⟨N, z⟩) = rec (F, ⟨N, 1^{st} (y)⟩)$
49	47 48	syl	$⊢ z = 1^{st} (y) \to rec (F, ⟨N, z⟩) = rec (F, ⟨N, 1^{st} (y)⟩)$
50	49	fveq1d	$⊢ z = 1^{st} (y) \to rec (F, ⟨N, z⟩) (N) = rec (F, ⟨N, 1^{st} (y)⟩) (N)$
51	50	eqeq2d	$⊢ z = 1^{st} (y) \to (\emptyset = rec (F, ⟨N, z⟩) (N) \leftrightarrow \emptyset = rec (F, ⟨N, 1^{st} (y)⟩) (N))$
52	51	anbi2d	$⊢ z = 1^{st} (y) \to ((N \in ω \land \emptyset = rec (F, ⟨N, z⟩) (N)) \leftrightarrow (N \in ω \land \emptyset = rec (F, ⟨N, 1^{st} (y)⟩) (N)))$
53	1	dffinxpf	$⊢ U ↑↑ N = \{z \| (N \in ω \land \emptyset = rec (F, ⟨N, z⟩) (N))\}$
54	46 52 53	elab2	$⊢ 1^{st} (y) \in U ↑↑ N \leftrightarrow (N \in ω \land \emptyset = rec (F, ⟨N, 1^{st} (y)⟩) (N))$
55	54	baib	$⊢ N \in ω \to (1^{st} (y) \in U ↑↑ N \leftrightarrow \emptyset = rec (F, ⟨N, 1^{st} (y)⟩) (N))$
56	55	ad2antrr	$⊢ ((N \in ω \land 1_{𝑜} \subseteq N) \land y \in (V \times U)) \to (1^{st} (y) \in U ↑↑ N \leftrightarrow \emptyset = rec (F, ⟨N, 1^{st} (y)⟩) (N))$
57	40 45 56	3bitr4d	$⊢ ((N \in ω \land 1_{𝑜} \subseteq N) \land y \in (V \times U)) \to (y \in U ↑↑ suc N \leftrightarrow 1^{st} (y) \in U ↑↑ N)$
58	57	biimpd	$⊢ ((N \in ω \land 1_{𝑜} \subseteq N) \land y \in (V \times U)) \to (y \in U ↑↑ suc N \to 1^{st} (y) \in U ↑↑ N)$
59	58	impancom	$⊢ ((N \in ω \land 1_{𝑜} \subseteq N) \land y \in U ↑↑ suc N) \to (y \in (V \times U) \to 1^{st} (y) \in U ↑↑ N)$
60	20 59	mpd	$⊢ ((N \in ω \land 1_{𝑜} \subseteq N) \land y \in U ↑↑ suc N) \to 1^{st} (y) \in U ↑↑ N$
61	60	ex	$⊢ (N \in ω \land 1_{𝑜} \subseteq N) \to (y \in U ↑↑ suc N \to 1^{st} (y) \in U ↑↑ N)$
62	20	ex	$⊢ (N \in ω \land 1_{𝑜} \subseteq N) \to (y \in U ↑↑ suc N \to y \in (V \times U))$
63	61 62	jcad	$⊢ (N \in ω \land 1_{𝑜} \subseteq N) \to (y \in U ↑↑ suc N \to (1^{st} (y) \in U ↑↑ N \land y \in (V \times U)))$
64	57	exbiri	$⊢ (N \in ω \land 1_{𝑜} \subseteq N) \to (y \in (V \times U) \to (1^{st} (y) \in U ↑↑ N \to y \in U ↑↑ suc N))$
65	64	impd	$⊢ (N \in ω \land 1_{𝑜} \subseteq N) \to ((y \in (V \times U) \land 1^{st} (y) \in U ↑↑ N) \to y \in U ↑↑ suc N)$
66	65	ancomsd	$⊢ (N \in ω \land 1_{𝑜} \subseteq N) \to ((1^{st} (y) \in U ↑↑ N \land y \in (V \times U)) \to y \in U ↑↑ suc N)$
67	63 66	impbid	$⊢ (N \in ω \land 1_{𝑜} \subseteq N) \to (y \in U ↑↑ suc N \leftrightarrow (1^{st} (y) \in U ↑↑ N \land y \in (V \times U)))$
68		elxp8	$⊢ y \in (U ↑↑ N \times U) \leftrightarrow (1^{st} (y) \in U ↑↑ N \land y \in (V \times U))$
69	67 68	bitr4di	$⊢ (N \in ω \land 1_{𝑜} \subseteq N) \to (y \in U ↑↑ suc N \leftrightarrow y \in (U ↑↑ N \times U))$
70	69	eqrdv	$⊢ (N \in ω \land 1_{𝑜} \subseteq N) \to U ↑↑ suc N = U ↑↑ N \times U$

Metamath Proof Explorer

Theorem finxpsuclem

Proof