finxpreclem5

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	finxpreclem5	$⊢ (n \in ω \land 1_{𝑜} \in n) \to (\neg x \in (V \times U) \to F (⟨n, x⟩) = ⟨n, x⟩)$

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		df-ov	$⊢ n F x = F (⟨n, x⟩)$
3		vex	$⊢ x \in V$
4		0ex	$⊢ \emptyset \in V$
5		opex	$⊢ ⟨⋃ n, 1^{st} (x)⟩ \in V$
6		opex	$⊢ ⟨n, x⟩ \in V$
7	5 6	ifex	$⊢ if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩) \in V$
8	4 7	ifex	$⊢ if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)) \in V$
9	1	ovmpt4g	$⊢ (n \in ω \land x \in V \land if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)) \in V) \to n F x = if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))$
10	3 8 9	mp3an23	$⊢ n \in ω \to n F x = if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))$
11	10	ad2antrr	$⊢ ((n \in ω \land 1_{𝑜} \in n) \land \neg x \in (V \times U)) \to n F x = if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩))$
12		1on	$⊢ 1_{𝑜} \in On$
13	12	onirri	$⊢ \neg 1_{𝑜} \in 1_{𝑜}$
14		eleq2	$⊢ n = 1_{𝑜} \to (1_{𝑜} \in n \leftrightarrow 1_{𝑜} \in 1_{𝑜})$
15	13 14	mtbiri	$⊢ n = 1_{𝑜} \to \neg 1_{𝑜} \in n$
16	15	con2i	$⊢ 1_{𝑜} \in n \to \neg n = 1_{𝑜}$
17	16	intnanrd	$⊢ 1_{𝑜} \in n \to \neg (n = 1_{𝑜} \land x \in U)$
18	17	iffalsed	$⊢ 1_{𝑜} \in n \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⟩)$
19	18	adantl	$⊢ (n \in ω \land 1_{𝑜} \in n) \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⟩)$
20		iffalse	$⊢ \neg x \in (V \times U) \to if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩) = ⟨n, x⟩$
21	19 20	sylan9eq	$⊢ ((n \in ω \land 1_{𝑜} \in n) \land \neg x \in (V \times U)) \to if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)) = ⟨n, x⟩$
22	11 21	eqtrd	$⊢ ((n \in ω \land 1_{𝑜} \in n) \land \neg x \in (V \times U)) \to n F x = ⟨n, x⟩$
23	2 22	syl5eqr	$⊢ ((n \in ω \land 1_{𝑜} \in n) \land \neg x \in (V \times U)) \to F (⟨n, x⟩) = ⟨n, x⟩$
24	23	ex	$⊢ (n \in ω \land 1_{𝑜} \in n) \to (\neg x \in (V \times U) \to F (⟨n, x⟩) = ⟨n, x⟩)$

Metamath Proof Explorer

Theorem finxpreclem5

Proof