finxpreclem2

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

		Ref	Expression
	Assertion	finxpreclem2	$⊢ (X \in V \land \neg X \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_{𝑜}, X⟩)$

Proof

Step	Hyp	Ref	Expression
1		nfv	$⊢ Ⅎ x (X \in V \land \neg X \in U)$
2		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⟩)))$
3		nfcv	$⊢ \underline{Ⅎ} x ⟨1_{𝑜}, X⟩$
4	2 3	nffv	$⊢ \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⟩))) (⟨1_{𝑜}, X⟩)$
5		nfcv	$⊢ \underline{Ⅎ} x \emptyset$
6	4 5	nfne	$⊢ Ⅎ 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⟩))) (⟨1_{𝑜}, X⟩) \neq \emptyset$
7	1 6	nfim	$⊢ Ⅎ x ((X \in V \land \neg X \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_{𝑜}, X⟩) \neq \emptyset)$
8		nfv	$⊢ Ⅎ n x = X$
9		nfv	$⊢ Ⅎ n (X \in V \land \neg X \in U)$
10		nfmpo1	$⊢ \underline{Ⅎ} n (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⟩)))$
11		nfcv	$⊢ \underline{Ⅎ} n ⟨1_{𝑜}, X⟩$
12	10 11	nffv	$⊢ \underline{Ⅎ} n (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_{𝑜}, X⟩)$
13		nfcv	$⊢ \underline{Ⅎ} n \emptyset$
14	12 13	nfne	$⊢ Ⅎ n (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_{𝑜}, X⟩) \neq \emptyset$
15	9 14	nfim	$⊢ Ⅎ n ((X \in V \land \neg X \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_{𝑜}, X⟩) \neq \emptyset)$
16	8 15	nfim	$⊢ Ⅎ n (x = X \to ((X \in V \land \neg X \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_{𝑜}, X⟩) \neq \emptyset))$
17		1onn	$⊢ 1_{𝑜} \in ω$
18	17	elexi	$⊢ 1_{𝑜} \in V$
19		df-ov	$⊢ 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⟩))) 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⟩))) (⟨1_{𝑜}, X⟩)$
20		0ex	$⊢ \emptyset \in V$
21		opex	$⊢ ⟨⋃ n, 1^{st} (x)⟩ \in V$
22		opex	$⊢ ⟨n, x⟩ \in V$
23	21 22	ifex	$⊢ if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩) \in V$
24	20 23	ifex	$⊢ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)) \in V$
25	24	csbex	$⊢ ⦋ X / x ⦌ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)) \in V$
26	25	csbex	$⊢ ⦋ 1_{𝑜} / n ⦌ ⦋ X / x ⦌ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)) \in V$
27		eqid	$⊢ (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⟩))) = (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⟩)))$
28	27	ovmpos	$⊢ (1_{𝑜} \in ω \land X \in V \land ⦋ 1_{𝑜} / n ⦌ ⦋ X / x ⦌ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)) \in V) \to 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⟩))) X = ⦋ 1_{𝑜} / n ⦌ ⦋ X / x ⦌ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))$
29	17 26 28	mp3an13	$⊢ X \in V \to 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⟩))) X = ⦋ 1_{𝑜} / n ⦌ ⦋ X / x ⦌ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))$
30	29	adantr	$⊢ (X \in V \land (\neg X \in U \land (n = 1_{𝑜} \land x = X))) \to 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⟩))) X = ⦋ 1_{𝑜} / n ⦌ ⦋ X / x ⦌ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))$
31		csbeq1a	$⊢ x = X \to if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)) = ⦋ X / x ⦌ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))$
32		csbeq1a	$⊢ n = 1_{𝑜} \to ⦋ X / x ⦌ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)) = ⦋ 1_{𝑜} / n ⦌ ⦋ X / x ⦌ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))$
33	31 32	sylan9eqr	$⊢ (n = 1_{𝑜} \land x = X) \to if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)) = ⦋ 1_{𝑜} / n ⦌ ⦋ X / x ⦌ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))$
34	33	adantl	$⊢ (\neg X \in U \land (n = 1_{𝑜} \land x = X)) \to if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)) = ⦋ 1_{𝑜} / n ⦌ ⦋ X / x ⦌ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))$
35		eleq1	$⊢ x = X \to (x \in U \leftrightarrow X \in U)$
36	35	notbid	$⊢ x = X \to (\neg x \in U \leftrightarrow \neg X \in U)$
37	36	biimprcd	$⊢ \neg X \in U \to (x = X \to \neg x \in U)$
38		pm3.14	$⊢ (\neg n = 1_{𝑜} \lor \neg x \in U) \to \neg (n = 1_{𝑜} \land x \in U)$
39	38	olcs	$⊢ \neg x \in U \to \neg (n = 1_{𝑜} \land x \in U)$
40	37 39	syl6	$⊢ \neg X \in U \to (x = X \to \neg (n = 1_{𝑜} \land x \in U))$
41		iffalse	$⊢ \neg (n = 1_{𝑜} \land x \in U) \to if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)) = if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)$
42	40 41	syl6	$⊢ \neg X \in U \to (x = X \to if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)) = if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))$
43	42	imp	$⊢ (\neg X \in U \land x = X) \to if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)) = if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)$
44		ifeqor	$⊢ (if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩) = ⟨⋃ n, 1^{st} (x)⟩ \lor if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩) = ⟨n, x⟩)$
45		vuniex	$⊢ ⋃ n \in V$
46		fvex	$⊢ 1^{st} (x) \in V$
47	45 46	opnzi	$⊢ ⟨⋃ n, 1^{st} (x)⟩ \neq \emptyset$
48	47	neii	$⊢ \neg ⟨⋃ n, 1^{st} (x)⟩ = \emptyset$
49		eqeq1	$⊢ if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩) = ⟨⋃ n, 1^{st} (x)⟩ \to (if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩) = \emptyset \leftrightarrow ⟨⋃ n, 1^{st} (x)⟩ = \emptyset)$
50	48 49	mtbiri	$⊢ if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩) = ⟨⋃ n, 1^{st} (x)⟩ \to \neg if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩) = \emptyset$
51		vex	$⊢ n \in V$
52		vex	$⊢ x \in V$
53	51 52	opnzi	$⊢ ⟨n, x⟩ \neq \emptyset$
54	53	neii	$⊢ \neg ⟨n, x⟩ = \emptyset$
55		eqeq1	$⊢ if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩) = ⟨n, x⟩ \to (if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩) = \emptyset \leftrightarrow ⟨n, x⟩ = \emptyset)$
56	54 55	mtbiri	$⊢ if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩) = ⟨n, x⟩ \to \neg if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩) = \emptyset$
57	50 56	jaoi	$⊢ (if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩) = ⟨⋃ n, 1^{st} (x)⟩ \lor if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩) = ⟨n, x⟩) \to \neg if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩) = \emptyset$
58	44 57	mp1i	$⊢ (\neg X \in U \land x = X) \to \neg if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩) = \emptyset$
59	58	neqned	$⊢ (\neg X \in U \land x = X) \to if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩) \neq \emptyset$
60	43 59	eqnetrd	$⊢ (\neg X \in U \land x = X) \to if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)) \neq \emptyset$
61	60	adantrl	$⊢ (\neg X \in U \land (n = 1_{𝑜} \land x = X)) \to if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)) \neq \emptyset$
62	34 61	eqnetrrd	$⊢ (\neg X \in U \land (n = 1_{𝑜} \land x = X)) \to ⦋ 1_{𝑜} / n ⦌ ⦋ X / x ⦌ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)) \neq \emptyset$
63	62	adantl	$⊢ (X \in V \land (\neg X \in U \land (n = 1_{𝑜} \land x = X))) \to ⦋ 1_{𝑜} / n ⦌ ⦋ X / x ⦌ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)) \neq \emptyset$
64	30 63	eqnetrd	$⊢ (X \in V \land (\neg X \in U \land (n = 1_{𝑜} \land x = X))) \to 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⟩))) X \neq \emptyset$
65	19 64	eqnetrrid	$⊢ (X \in V \land (\neg X \in U \land (n = 1_{𝑜} \land x = X))) \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_{𝑜}, X⟩) \neq \emptyset$
66	65	ancom2s	$⊢ (X \in V \land ((n = 1_{𝑜} \land x = X) \land \neg X \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_{𝑜}, X⟩) \neq \emptyset$
67	66	an12s	$⊢ ((n = 1_{𝑜} \land x = X) \land (X \in V \land \neg X \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_{𝑜}, X⟩) \neq \emptyset$
68	67	exp31	$⊢ n = 1_{𝑜} \to (x = X \to ((X \in V \land \neg X \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_{𝑜}, X⟩) \neq \emptyset))$
69	16 18 68	vtoclef	$⊢ x = X \to ((X \in V \land \neg X \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_{𝑜}, X⟩) \neq \emptyset)$
70	7 69	vtoclefex	$⊢ X \in V \to ((X \in V \land \neg X \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_{𝑜}, X⟩) \neq \emptyset)$
71	70	anabsi5	$⊢ (X \in V \land \neg X \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_{𝑜}, X⟩) \neq \emptyset$
72	71	necomd	$⊢ (X \in V \land \neg X \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_{𝑜}, X⟩)$
73	72	neneqd	$⊢ (X \in V \land \neg X \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_{𝑜}, X⟩)$

Metamath Proof Explorer

Theorem finxpreclem2

Proof