finxpreclem3

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

		Ref	Expression
	Hypothesis	finxpreclem3.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	finxpreclem3	$⊢ ((N \in ω \land 2_{𝑜} \subseteq N) \land X \in (V \times U)) \to ⟨⋃ N, 1^{st} (X)⟩ = F (⟨N, X⟩)$

Proof

Step	Hyp	Ref	Expression
1		finxpreclem3.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	1	a1i	$⊢ ((N \in ω \land 2_{𝑜} \subseteq N) \land X \in (V \times U)) \to 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⟩)))$
3		eqeq1	$⊢ n = N \to (n = 1_{𝑜} \leftrightarrow N = 1_{𝑜})$
4		eleq1	$⊢ x = X \to (x \in U \leftrightarrow X \in U)$
5	3 4	bi2anan9	$⊢ (n = N \land x = X) \to ((n = 1_{𝑜} \land x \in U) \leftrightarrow (N = 1_{𝑜} \land X \in U))$
6		eleq1	$⊢ x = X \to (x \in (V \times U) \leftrightarrow X \in (V \times U))$
7	6	adantl	$⊢ (n = N \land x = X) \to (x \in (V \times U) \leftrightarrow X \in (V \times U))$
8		unieq	$⊢ n = N \to ⋃ n = ⋃ N$
9	8	adantr	$⊢ (n = N \land x = X) \to ⋃ n = ⋃ N$
10		fveq2	$⊢ x = X \to 1^{st} (x) = 1^{st} (X)$
11	10	adantl	$⊢ (n = N \land x = X) \to 1^{st} (x) = 1^{st} (X)$
12	9 11	opeq12d	$⊢ (n = N \land x = X) \to ⟨⋃ n, 1^{st} (x)⟩ = ⟨⋃ N, 1^{st} (X)⟩$
13		opeq12	$⊢ (n = N \land x = X) \to ⟨n, x⟩ = ⟨N, X⟩$
14	7 12 13	ifbieq12d	$⊢ (n = N \land x = X) \to if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩) = if (X \in (V \times U), ⟨⋃ N, 1^{st} (X)⟩, ⟨N, X⟩)$
15	5 14	ifbieq2d	$⊢ (n = N \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 ((N = 1_{𝑜} \land X \in U), \emptyset, if (X \in (V \times U), ⟨⋃ N, 1^{st} (X)⟩, ⟨N, X⟩))$
16		sssucid	$⊢ 1_{𝑜} \subseteq suc 1_{𝑜}$
17		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
18	16 17	sseqtrri	$⊢ 1_{𝑜} \subseteq 2_{𝑜}$
19		1on	$⊢ 1_{𝑜} \in On$
20	17 19	sucneqoni	$⊢ 2_{𝑜} \neq 1_{𝑜}$
21	20	necomi	$⊢ 1_{𝑜} \neq 2_{𝑜}$
22		df-pss	$⊢ 1_{𝑜} \subset 2_{𝑜} \leftrightarrow (1_{𝑜} \subseteq 2_{𝑜} \land 1_{𝑜} \neq 2_{𝑜})$
23	18 21 22	mpbir2an	$⊢ 1_{𝑜} \subset 2_{𝑜}$
24		ssnpss	$⊢ 2_{𝑜} \subseteq 1_{𝑜} \to \neg 1_{𝑜} \subset 2_{𝑜}$
25	23 24	mt2	$⊢ \neg 2_{𝑜} \subseteq 1_{𝑜}$
26		sseq2	$⊢ N = 1_{𝑜} \to (2_{𝑜} \subseteq N \leftrightarrow 2_{𝑜} \subseteq 1_{𝑜})$
27	25 26	mtbiri	$⊢ N = 1_{𝑜} \to \neg 2_{𝑜} \subseteq N$
28	27	con2i	$⊢ 2_{𝑜} \subseteq N \to \neg N = 1_{𝑜}$
29	28	intnanrd	$⊢ 2_{𝑜} \subseteq N \to \neg (N = 1_{𝑜} \land X \in U)$
30	29	iffalsed	$⊢ 2_{𝑜} \subseteq 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⟩)$
31		iftrue	$⊢ X \in (V \times U) \to if (X \in (V \times U), ⟨⋃ N, 1^{st} (X)⟩, ⟨N, X⟩) = ⟨⋃ N, 1^{st} (X)⟩$
32	30 31	sylan9eq	$⊢ (2_{𝑜} \subseteq N \land 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, 1^{st} (X)⟩$
33	15 32	sylan9eqr	$⊢ ((2_{𝑜} \subseteq N \land X \in (V \times U)) \land (n = N \land x = X)) \to if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)) = ⟨⋃ N, 1^{st} (X)⟩$
34	33	adantlll	$⊢ (((N \in ω \land 2_{𝑜} \subseteq N) \land X \in (V \times U)) \land (n = N \land x = X)) \to if ((n = 1_{𝑜} \land x \in U), \emptyset, if (x \in (V \times U), ⟨⋃ n, 1^{st} (x)⟩, ⟨n, x⟩)) = ⟨⋃ N, 1^{st} (X)⟩$
35		simpll	$⊢ ((N \in ω \land 2_{𝑜} \subseteq N) \land X \in (V \times U)) \to N \in ω$
36		elex	$⊢ X \in (V \times U) \to X \in V$
37	36	adantl	$⊢ ((N \in ω \land 2_{𝑜} \subseteq N) \land X \in (V \times U)) \to X \in V$
38		opex	$⊢ ⟨⋃ N, 1^{st} (X)⟩ \in V$
39	38	a1i	$⊢ ((N \in ω \land 2_{𝑜} \subseteq N) \land X \in (V \times U)) \to ⟨⋃ N, 1^{st} (X)⟩ \in V$
40	2 34 35 37 39	ovmpod	$⊢ ((N \in ω \land 2_{𝑜} \subseteq N) \land X \in (V \times U)) \to N F X = ⟨⋃ N, 1^{st} (X)⟩$
41		df-ov	$⊢ N F X = F (⟨N, X⟩)$
42	40 41	eqtr3di	$⊢ ((N \in ω \land 2_{𝑜} \subseteq N) \land X \in (V \times U)) \to ⟨⋃ N, 1^{st} (X)⟩ = F (⟨N, X⟩)$

Metamath Proof Explorer

Theorem finxpreclem3

Proof