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