finxpreclem6

Description: Lemma for ^^ recursion theorems. (Contributed by ML, 24-Oct-2020)

		Ref	Expression
	Hypothesis	finxpreclem5.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	finxpreclem6	$⊢ (N \in ω \land 1_{𝑜} \in N) \to U ↑↑ N \subseteq V \times U$

Proof

Step	Hyp	Ref	Expression
1		finxpreclem5.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		eleq1	$⊢ n = N \to (n \in ω \leftrightarrow N \in ω)$
3		eleq2	$⊢ n = N \to (1_{𝑜} \in n \leftrightarrow 1_{𝑜} \in N)$
4	2 3	anbi12d	$⊢ n = N \to ((n \in ω \land 1_{𝑜} \in n) \leftrightarrow (N \in ω \land 1_{𝑜} \in N))$
5		anass	$⊢ ((n \in ω \land 1_{𝑜} \in n) \land \neg y \in (V \times U)) \leftrightarrow (n \in ω \land (1_{𝑜} \in n \land \neg y \in (V \times U)))$
6		nfv	$⊢ Ⅎ x (n \in ω \land (1_{𝑜} \in n \land \neg y \in (V \times U)))$
7		nfmpo2	$⊢ \underline{Ⅎ} x (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⟩)))$
8	1 7	nfcxfr	$⊢ \underline{Ⅎ} x F$
9		nfcv	$⊢ \underline{Ⅎ} x ⟨n, y⟩$
10	8 9	nfrdg	$⊢ \underline{Ⅎ} x rec (F, ⟨n, y⟩)$
11		nfcv	$⊢ \underline{Ⅎ} x n$
12	10 11	nffv	$⊢ \underline{Ⅎ} x rec (F, ⟨n, y⟩) (n)$
13	12	nfeq2	$⊢ Ⅎ x \emptyset = rec (F, ⟨n, y⟩) (n)$
14	13	nfn	$⊢ Ⅎ x \neg \emptyset = rec (F, ⟨n, y⟩) (n)$
15	6 14	nfim	$⊢ Ⅎ x ((n \in ω \land (1_{𝑜} \in n \land \neg y \in (V \times U))) \to \neg \emptyset = rec (F, ⟨n, y⟩) (n))$
16		eleq1	$⊢ x = y \to (x \in (V \times U) \leftrightarrow y \in (V \times U))$
17	16	notbid	$⊢ x = y \to (\neg x \in (V \times U) \leftrightarrow \neg y \in (V \times U))$
18	17	anbi2d	$⊢ x = y \to ((1_{𝑜} \in n \land \neg x \in (V \times U)) \leftrightarrow (1_{𝑜} \in n \land \neg y \in (V \times U)))$
19	18	anbi2d	$⊢ x = y \to ((n \in ω \land (1_{𝑜} \in n \land \neg x \in (V \times U))) \leftrightarrow (n \in ω \land (1_{𝑜} \in n \land \neg y \in (V \times U))))$
20		opeq2	$⊢ x = y \to ⟨n, x⟩ = ⟨n, y⟩$
21		rdgeq2	$⊢ ⟨n, x⟩ = ⟨n, y⟩ \to rec (F, ⟨n, x⟩) = rec (F, ⟨n, y⟩)$
22	20 21	syl	$⊢ x = y \to rec (F, ⟨n, x⟩) = rec (F, ⟨n, y⟩)$
23	22	fveq1d	$⊢ x = y \to rec (F, ⟨n, x⟩) (n) = rec (F, ⟨n, y⟩) (n)$
24	23	eqeq2d	$⊢ x = y \to (\emptyset = rec (F, ⟨n, x⟩) (n) \leftrightarrow \emptyset = rec (F, ⟨n, y⟩) (n))$
25	24	notbid	$⊢ x = y \to (\neg \emptyset = rec (F, ⟨n, x⟩) (n) \leftrightarrow \neg \emptyset = rec (F, ⟨n, y⟩) (n))$
26	19 25	imbi12d	$⊢ x = y \to (((n \in ω \land (1_{𝑜} \in n \land \neg x \in (V \times U))) \to \neg \emptyset = rec (F, ⟨n, x⟩) (n)) \leftrightarrow ((n \in ω \land (1_{𝑜} \in n \land \neg y \in (V \times U))) \to \neg \emptyset = rec (F, ⟨n, y⟩) (n)))$
27		anass	$⊢ ((n \in ω \land 1_{𝑜} \in n) \land \neg x \in (V \times U)) \leftrightarrow (n \in ω \land (1_{𝑜} \in n \land \neg x \in (V \times U)))$
28		vex	$⊢ n \in V$
29		fveqeq2	$⊢ m = \emptyset \to (rec (F, ⟨n, x⟩) (m) = ⟨n, x⟩ \leftrightarrow rec (F, ⟨n, x⟩) (\emptyset) = ⟨n, x⟩)$
30		fveqeq2	$⊢ m = o \to (rec (F, ⟨n, x⟩) (m) = ⟨n, x⟩ \leftrightarrow rec (F, ⟨n, x⟩) (o) = ⟨n, x⟩)$
31		fveqeq2	$⊢ m = suc o \to (rec (F, ⟨n, x⟩) (m) = ⟨n, x⟩ \leftrightarrow rec (F, ⟨n, x⟩) (suc o) = ⟨n, x⟩)$
32		opex	$⊢ ⟨n, x⟩ \in V$
33	32	rdg0	$⊢ rec (F, ⟨n, x⟩) (\emptyset) = ⟨n, x⟩$
34	33	a1i	$⊢ ((n \in ω \land 1_{𝑜} \in n) \land \neg x \in (V \times U)) \to rec (F, ⟨n, x⟩) (\emptyset) = ⟨n, x⟩$
35		nnon	$⊢ o \in ω \to o \in On$
36		rdgsuc	$⊢ o \in On \to rec (F, ⟨n, x⟩) (suc o) = F (rec (F, ⟨n, x⟩) (o))$
37	35 36	syl	$⊢ o \in ω \to rec (F, ⟨n, x⟩) (suc o) = F (rec (F, ⟨n, x⟩) (o))$
38		fveq2	$⊢ rec (F, ⟨n, x⟩) (o) = ⟨n, x⟩ \to F (rec (F, ⟨n, x⟩) (o)) = F (⟨n, x⟩)$
39	37 38	sylan9eq	$⊢ (o \in ω \land rec (F, ⟨n, x⟩) (o) = ⟨n, x⟩) \to rec (F, ⟨n, x⟩) (suc o) = F (⟨n, x⟩)$
40	1	finxpreclem5	$⊢ (n \in ω \land 1_{𝑜} \in n) \to (\neg x \in (V \times U) \to F (⟨n, x⟩) = ⟨n, x⟩)$
41	40	imp	$⊢ ((n \in ω \land 1_{𝑜} \in n) \land \neg x \in (V \times U)) \to F (⟨n, x⟩) = ⟨n, x⟩$
42	39 41	sylan9eq	$⊢ ((o \in ω \land rec (F, ⟨n, x⟩) (o) = ⟨n, x⟩) \land ((n \in ω \land 1_{𝑜} \in n) \land \neg x \in (V \times U))) \to rec (F, ⟨n, x⟩) (suc o) = ⟨n, x⟩$
43	42	expl	$⊢ o \in ω \to ((rec (F, ⟨n, x⟩) (o) = ⟨n, x⟩ \land ((n \in ω \land 1_{𝑜} \in n) \land \neg x \in (V \times U))) \to rec (F, ⟨n, x⟩) (suc o) = ⟨n, x⟩)$
44	43	expcomd	$⊢ o \in ω \to (((n \in ω \land 1_{𝑜} \in n) \land \neg x \in (V \times U)) \to (rec (F, ⟨n, x⟩) (o) = ⟨n, x⟩ \to rec (F, ⟨n, x⟩) (suc o) = ⟨n, x⟩))$
45	29 30 31 34 44	finds2	$⊢ m \in ω \to (((n \in ω \land 1_{𝑜} \in n) \land \neg x \in (V \times U)) \to rec (F, ⟨n, x⟩) (m) = ⟨n, x⟩)$
46		eleq1	$⊢ n = m \to (n \in ω \leftrightarrow m \in ω)$
47		fveqeq2	$⊢ n = m \to (rec (F, ⟨n, x⟩) (n) = ⟨n, x⟩ \leftrightarrow rec (F, ⟨n, x⟩) (m) = ⟨n, x⟩)$
48	47	imbi2d	$⊢ n = m \to ((((n \in ω \land 1_{𝑜} \in n) \land \neg x \in (V \times U)) \to rec (F, ⟨n, x⟩) (n) = ⟨n, x⟩) \leftrightarrow (((n \in ω \land 1_{𝑜} \in n) \land \neg x \in (V \times U)) \to rec (F, ⟨n, x⟩) (m) = ⟨n, x⟩))$
49	46 48	imbi12d	$⊢ n = m \to ((n \in ω \to (((n \in ω \land 1_{𝑜} \in n) \land \neg x \in (V \times U)) \to rec (F, ⟨n, x⟩) (n) = ⟨n, x⟩)) \leftrightarrow (m \in ω \to (((n \in ω \land 1_{𝑜} \in n) \land \neg x \in (V \times U)) \to rec (F, ⟨n, x⟩) (m) = ⟨n, x⟩)))$
50	45 49	mpbiri	$⊢ n = m \to (n \in ω \to (((n \in ω \land 1_{𝑜} \in n) \land \neg x \in (V \times U)) \to rec (F, ⟨n, x⟩) (n) = ⟨n, x⟩))$
51	50	equcoms	$⊢ m = n \to (n \in ω \to (((n \in ω \land 1_{𝑜} \in n) \land \neg x \in (V \times U)) \to rec (F, ⟨n, x⟩) (n) = ⟨n, x⟩))$
52	28 51	vtocle	$⊢ n \in ω \to (((n \in ω \land 1_{𝑜} \in n) \land \neg x \in (V \times U)) \to rec (F, ⟨n, x⟩) (n) = ⟨n, x⟩)$
53	27 52	syl5bir	$⊢ n \in ω \to ((n \in ω \land (1_{𝑜} \in n \land \neg x \in (V \times U))) \to rec (F, ⟨n, x⟩) (n) = ⟨n, x⟩)$
54	53	anabsi5	$⊢ (n \in ω \land (1_{𝑜} \in n \land \neg x \in (V \times U))) \to rec (F, ⟨n, x⟩) (n) = ⟨n, x⟩$
55		vex	$⊢ x \in V$
56	28 55	opnzi	$⊢ ⟨n, x⟩ \neq \emptyset$
57	56	a1i	$⊢ (n \in ω \land (1_{𝑜} \in n \land \neg x \in (V \times U))) \to ⟨n, x⟩ \neq \emptyset$
58	54 57	eqnetrd	$⊢ (n \in ω \land (1_{𝑜} \in n \land \neg x \in (V \times U))) \to rec (F, ⟨n, x⟩) (n) \neq \emptyset$
59	58	necomd	$⊢ (n \in ω \land (1_{𝑜} \in n \land \neg x \in (V \times U))) \to \emptyset \neq rec (F, ⟨n, x⟩) (n)$
60	59	neneqd	$⊢ (n \in ω \land (1_{𝑜} \in n \land \neg x \in (V \times U))) \to \neg \emptyset = rec (F, ⟨n, x⟩) (n)$
61	15 26 60	chvarfv	$⊢ (n \in ω \land (1_{𝑜} \in n \land \neg y \in (V \times U))) \to \neg \emptyset = rec (F, ⟨n, y⟩) (n)$
62	61	intnand	$⊢ (n \in ω \land (1_{𝑜} \in n \land \neg y \in (V \times U))) \to \neg (n \in ω \land \emptyset = rec (F, ⟨n, y⟩) (n))$
63	62	adantl	$⊢ (n = N \land (n \in ω \land (1_{𝑜} \in n \land \neg y \in (V \times U)))) \to \neg (n \in ω \land \emptyset = rec (F, ⟨n, y⟩) (n))$
64		opeq1	$⊢ n = N \to ⟨n, y⟩ = ⟨N, y⟩$
65		rdgeq2	$⊢ ⟨n, y⟩ = ⟨N, y⟩ \to rec (F, ⟨n, y⟩) = rec (F, ⟨N, y⟩)$
66	64 65	syl	$⊢ n = N \to rec (F, ⟨n, y⟩) = rec (F, ⟨N, y⟩)$
67		id	$⊢ n = N \to n = N$
68	66 67	fveq12d	$⊢ n = N \to rec (F, ⟨n, y⟩) (n) = rec (F, ⟨N, y⟩) (N)$
69	68	eqeq2d	$⊢ n = N \to (\emptyset = rec (F, ⟨n, y⟩) (n) \leftrightarrow \emptyset = rec (F, ⟨N, y⟩) (N))$
70	2 69	anbi12d	$⊢ n = N \to ((n \in ω \land \emptyset = rec (F, ⟨n, y⟩) (n)) \leftrightarrow (N \in ω \land \emptyset = rec (F, ⟨N, y⟩) (N)))$
71	70	abbidv	$⊢ n = N \to \{y \| (n \in ω \land \emptyset = rec (F, ⟨n, y⟩) (n))\} = \{y \| (N \in ω \land \emptyset = rec (F, ⟨N, y⟩) (N))\}$
72	1	dffinxpf	$⊢ U ↑↑ N = \{y \| (N \in ω \land \emptyset = rec (F, ⟨N, y⟩) (N))\}$
73	71 72	eqtr4di	$⊢ n = N \to \{y \| (n \in ω \land \emptyset = rec (F, ⟨n, y⟩) (n))\} = U ↑↑ N$
74	73	eleq2d	$⊢ n = N \to (y \in \{y \| (n \in ω \land \emptyset = rec (F, ⟨n, y⟩) (n))\} \leftrightarrow y \in U ↑↑ N)$
75		abid	$⊢ y \in \{y \| (n \in ω \land \emptyset = rec (F, ⟨n, y⟩) (n))\} \leftrightarrow (n \in ω \land \emptyset = rec (F, ⟨n, y⟩) (n))$
76	74 75	bitr3di	$⊢ n = N \to (y \in U ↑↑ N \leftrightarrow (n \in ω \land \emptyset = rec (F, ⟨n, y⟩) (n)))$
77	76	adantr	$⊢ (n = N \land (n \in ω \land (1_{𝑜} \in n \land \neg y \in (V \times U)))) \to (y \in U ↑↑ N \leftrightarrow (n \in ω \land \emptyset = rec (F, ⟨n, y⟩) (n)))$
78	63 77	mtbird	$⊢ (n = N \land (n \in ω \land (1_{𝑜} \in n \land \neg y \in (V \times U)))) \to \neg y \in U ↑↑ N$
79	78	ex	$⊢ n = N \to ((n \in ω \land (1_{𝑜} \in n \land \neg y \in (V \times U))) \to \neg y \in U ↑↑ N)$
80	5 79	syl5bi	$⊢ n = N \to (((n \in ω \land 1_{𝑜} \in n) \land \neg y \in (V \times U)) \to \neg y \in U ↑↑ N)$
81	80	expdimp	$⊢ (n = N \land (n \in ω \land 1_{𝑜} \in n)) \to (\neg y \in (V \times U) \to \neg y \in U ↑↑ N)$
82	81	con4d	$⊢ (n = N \land (n \in ω \land 1_{𝑜} \in n)) \to (y \in U ↑↑ N \to y \in (V \times U))$
83	82	ssrdv	$⊢ (n = N \land (n \in ω \land 1_{𝑜} \in n)) \to U ↑↑ N \subseteq V \times U$
84	83	ex	$⊢ n = N \to ((n \in ω \land 1_{𝑜} \in n) \to U ↑↑ N \subseteq V \times U)$
85	4 84	sylbird	$⊢ n = N \to ((N \in ω \land 1_{𝑜} \in N) \to U ↑↑ N \subseteq V \times U)$
86	85	vtocleg	$⊢ N \in ω \to ((N \in ω \land 1_{𝑜} \in N) \to U ↑↑ N \subseteq V \times U)$
87	86	anabsi5	$⊢ (N \in ω \land 1_{𝑜} \in N) \to U ↑↑ N \subseteq V \times U$

Metamath Proof Explorer

Theorem finxpreclem6

Proof