Metamath Proof Explorer

Theorem finxpreclem1

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

		Ref	Expression
	Assertion	finxpreclem1	$⊢ X \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_{𝑜}, X⟩)$

Proof

Step	Hyp	Ref	Expression
1		eqidd	$⊢ 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⟩))) = (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		eleq1a	$⊢ X \in U \to (x = X \to x \in U)$
3	2	anim2d	$⊢ X \in U \to ((n = 1_{𝑜} \land x = X) \to (n = 1_{𝑜} \land x \in U))$
4		iftrue	$⊢ (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⟩)) = \emptyset$
5	3 4	syl6	$⊢ X \in U \to ((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⟩)) = \emptyset)$
6	5	imp	$⊢ (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⟩)) = \emptyset$
7		1onn	$⊢ 1_{𝑜} \in ω$
8	7	a1i	$⊢ X \in U \to 1_{𝑜} \in ω$
9		elex	$⊢ X \in U \to X \in V$
10		0ex	$⊢ \emptyset \in V$
11	10	a1i	$⊢ X \in U \to \emptyset \in V$
12	1 6 8 9 11	ovmpod	$⊢ X \in U \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 = \emptyset$
13		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⟩)$
14	12 13	eqtr3di	$⊢ X \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_{𝑜}, X⟩)$