cantnfvalf

Description: Lemma for cantnf . The function appearing in cantnfval is unconditionally a function. (Contributed by Mario Carneiro, 20-May-2015)

		Ref	Expression
	Hypothesis	cantnfvalf.f	$⊢ F = {seq}_{ω} ((k \in A, z \in B ⟼ C +_{𝑜} D), \emptyset)$
	Assertion	cantnfvalf	$⊢ F : ω ⟶ On$

Proof

Step	Hyp	Ref	Expression
1		cantnfvalf.f	$⊢ F = {seq}_{ω} ((k \in A, z \in B ⟼ C +_{𝑜} D), \emptyset)$
2	1	fnseqom	$⊢ F Fn ω$
3		nn0suc	$⊢ x \in ω \to (x = \emptyset \lor \exists y \in ω x = suc y)$
4		fveq2	$⊢ x = \emptyset \to F (x) = F (\emptyset)$
5		0ex	$⊢ \emptyset \in V$
6	1	seqom0g	$⊢ \emptyset \in V \to F (\emptyset) = \emptyset$
7	5 6	ax-mp	$⊢ F (\emptyset) = \emptyset$
8	4 7	eqtrdi	$⊢ x = \emptyset \to F (x) = \emptyset$
9		0elon	$⊢ \emptyset \in On$
10	8 9	eqeltrdi	$⊢ x = \emptyset \to F (x) \in On$
11	1	seqomsuc	$⊢ y \in ω \to F (suc y) = y (k \in A, z \in B ⟼ C +_{𝑜} D) F (y)$
12		df-ov	$⊢ y (k \in A, z \in B ⟼ C +_{𝑜} D) F (y) = (k \in A, z \in B ⟼ C +_{𝑜} D) (⟨y, F (y)⟩)$
13	11 12	eqtrdi	$⊢ y \in ω \to F (suc y) = (k \in A, z \in B ⟼ C +_{𝑜} D) (⟨y, F (y)⟩)$
14		df-ov	$⊢ C +_{𝑜} D = +_{𝑜} (⟨C, D⟩)$
15		fnoa	$⊢ +_{𝑜} Fn (On \times On)$
16		oacl	$⊢ (x \in On \land y \in On) \to x +_{𝑜} y \in On$
17	16	rgen2	$⊢ \forall x \in On \forall y \in On x +_{𝑜} y \in On$
18		ffnov	$⊢ +_{𝑜} : On \times On ⟶ On \leftrightarrow (+_{𝑜} Fn (On \times On) \land \forall x \in On \forall y \in On x +_{𝑜} y \in On)$
19	15 17 18	mpbir2an	$⊢ +_{𝑜} : On \times On ⟶ On$
20	19 9	f0cli	$⊢ +_{𝑜} (⟨C, D⟩) \in On$
21	14 20	eqeltri	$⊢ C +_{𝑜} D \in On$
22	21	rgen2w	$⊢ \forall k \in A \forall z \in B C +_{𝑜} D \in On$
23		eqid	$⊢ (k \in A, z \in B ⟼ C +_{𝑜} D) = (k \in A, z \in B ⟼ C +_{𝑜} D)$
24	23	fmpo	$⊢ \forall k \in A \forall z \in B C +_{𝑜} D \in On \leftrightarrow (k \in A, z \in B ⟼ C +_{𝑜} D) : A \times B ⟶ On$
25	22 24	mpbi	$⊢ (k \in A, z \in B ⟼ C +_{𝑜} D) : A \times B ⟶ On$
26	25 9	f0cli	$⊢ (k \in A, z \in B ⟼ C +_{𝑜} D) (⟨y, F (y)⟩) \in On$
27	13 26	eqeltrdi	$⊢ y \in ω \to F (suc y) \in On$
28		fveq2	$⊢ x = suc y \to F (x) = F (suc y)$
29	28	eleq1d	$⊢ x = suc y \to (F (x) \in On \leftrightarrow F (suc y) \in On)$
30	27 29	syl5ibrcom	$⊢ y \in ω \to (x = suc y \to F (x) \in On)$
31	30	rexlimiv	$⊢ \exists y \in ω x = suc y \to F (x) \in On$
32	10 31	jaoi	$⊢ (x = \emptyset \lor \exists y \in ω x = suc y) \to F (x) \in On$
33	3 32	syl	$⊢ x \in ω \to F (x) \in On$
34	33	rgen	$⊢ \forall x \in ω F (x) \in On$
35		ffnfv	$⊢ F : ω ⟶ On \leftrightarrow (F Fn ω \land \forall x \in ω F (x) \in On)$
36	2 34 35	mpbir2an	$⊢ F : ω ⟶ On$

Metamath Proof Explorer

Theorem cantnfvalf

Proof