mh-inf3f1

Description: A variant of inf3 . If F is a one-to-one function from A into itself, and B is an element outside its range, then ` ( rec ( F , B ) |`_om ) is a one-to-one function yielding an infinite sequence of distinct elements from A . If A is a set, we can use this theorem to prove _om e. _V via f1dmex . (Contributed by Matthew House, 13-Apr-2026)

	Ref	Expression
Hypotheses	mh-inf3f1.1	$⊢ φ \to F : A \underset{1-1}{⟶} A$
	mh-inf3f1.2	$⊢ φ \to B \in (A ∖ ran F)$
Assertion	mh-inf3f1	$⊢ φ \to ({rec (F, B) ↾}_{ω}) : ω \underset{1-1}{⟶} A$

Proof

Step	Hyp	Ref	Expression
1		mh-inf3f1.1	$⊢ φ \to F : A \underset{1-1}{⟶} A$
2		mh-inf3f1.2	$⊢ φ \to B \in (A ∖ ran F)$
3		fveq2	$⊢ x = \emptyset \to ({rec (F, B) ↾}_{ω}) (x) = ({rec (F, B) ↾}_{ω}) (\emptyset)$
4	3	eleq1d	$⊢ x = \emptyset \to (({rec (F, B) ↾}_{ω}) (x) \in A \leftrightarrow ({rec (F, B) ↾}_{ω}) (\emptyset) \in A)$
5		fveq2	$⊢ x = z \to ({rec (F, B) ↾}_{ω}) (x) = ({rec (F, B) ↾}_{ω}) (z)$
6	5	eleq1d	$⊢ x = z \to (({rec (F, B) ↾}_{ω}) (x) \in A \leftrightarrow ({rec (F, B) ↾}_{ω}) (z) \in A)$
7		fveq2	$⊢ x = suc z \to ({rec (F, B) ↾}_{ω}) (x) = ({rec (F, B) ↾}_{ω}) (suc z)$
8	7	eleq1d	$⊢ x = suc z \to (({rec (F, B) ↾}_{ω}) (x) \in A \leftrightarrow ({rec (F, B) ↾}_{ω}) (suc z) \in A)$
9		fr0g	$⊢ B \in (A ∖ ran F) \to ({rec (F, B) ↾}_{ω}) (\emptyset) = B$
10	2 9	syl	$⊢ φ \to ({rec (F, B) ↾}_{ω}) (\emptyset) = B$
11	10 2	eqeltrd	$⊢ φ \to ({rec (F, B) ↾}_{ω}) (\emptyset) \in (A ∖ ran F)$
12	11	eldifad	$⊢ φ \to ({rec (F, B) ↾}_{ω}) (\emptyset) \in A$
13		f1f	$⊢ F : A \underset{1-1}{⟶} A \to F : A ⟶ A$
14	1 13	syl	$⊢ φ \to F : A ⟶ A$
15	14	ffvelcdmda	$⊢ (φ \land ({rec (F, B) ↾}_{ω}) (z) \in A) \to F (({rec (F, B) ↾}_{ω}) (z)) \in A$
16		frsuc	$⊢ z \in ω \to ({rec (F, B) ↾}_{ω}) (suc z) = F (({rec (F, B) ↾}_{ω}) (z))$
17	16	eleq1d	$⊢ z \in ω \to (({rec (F, B) ↾}_{ω}) (suc z) \in A \leftrightarrow F (({rec (F, B) ↾}_{ω}) (z)) \in A)$
18	15 17	imbitrrid	$⊢ z \in ω \to ((φ \land ({rec (F, B) ↾}_{ω}) (z) \in A) \to ({rec (F, B) ↾}_{ω}) (suc z) \in A)$
19	18	expd	$⊢ z \in ω \to (φ \to (({rec (F, B) ↾}_{ω}) (z) \in A \to ({rec (F, B) ↾}_{ω}) (suc z) \in A))$
20	4 6 8 12 19	finds2	$⊢ x \in ω \to (φ \to ({rec (F, B) ↾}_{ω}) (x) \in A)$
21	20	com12	$⊢ φ \to (x \in ω \to ({rec (F, B) ↾}_{ω}) (x) \in A)$
22	21	ralrimiv	$⊢ φ \to \forall x \in ω ({rec (F, B) ↾}_{ω}) (x) \in A$
23		frfnom	$⊢ ({rec (F, B) ↾}_{ω}) Fn ω$
24		ffnfv	$⊢ ({rec (F, B) ↾}_{ω}) : ω ⟶ A \leftrightarrow (({rec (F, B) ↾}_{ω}) Fn ω \land \forall x \in ω ({rec (F, B) ↾}_{ω}) (x) \in A)$
25	23 24	mpbiran	$⊢ ({rec (F, B) ↾}_{ω}) : ω ⟶ A \leftrightarrow \forall x \in ω ({rec (F, B) ↾}_{ω}) (x) \in A$
26	22 25	sylibr	$⊢ φ \to ({rec (F, B) ↾}_{ω}) : ω ⟶ A$
27	3	neeq1d	$⊢ x = \emptyset \to (({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (y) \leftrightarrow ({rec (F, B) ↾}_{ω}) (\emptyset) \neq ({rec (F, B) ↾}_{ω}) (y))$
28	27	raleqbi1dv	$⊢ x = \emptyset \to (\forall y \in x ({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (y) \leftrightarrow \forall y \in \emptyset ({rec (F, B) ↾}_{ω}) (\emptyset) \neq ({rec (F, B) ↾}_{ω}) (y))$
29	5	neeq1d	$⊢ x = z \to (({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (y) \leftrightarrow ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y))$
30	29	raleqbi1dv	$⊢ x = z \to (\forall y \in x ({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (y) \leftrightarrow \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y))$
31	7	neeq1d	$⊢ x = suc z \to (({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (y) \leftrightarrow ({rec (F, B) ↾}_{ω}) (suc z) \neq ({rec (F, B) ↾}_{ω}) (y))$
32	31	raleqbi1dv	$⊢ x = suc z \to (\forall y \in x ({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (y) \leftrightarrow \forall y \in suc z ({rec (F, B) ↾}_{ω}) (suc z) \neq ({rec (F, B) ↾}_{ω}) (y))$
33		ral0	$⊢ \forall y \in \emptyset ({rec (F, B) ↾}_{ω}) (\emptyset) \neq ({rec (F, B) ↾}_{ω}) (y)$
34	33	a1i	$⊢ φ \to \forall y \in \emptyset ({rec (F, B) ↾}_{ω}) (\emptyset) \neq ({rec (F, B) ↾}_{ω}) (y)$
35		nfv	$⊢ Ⅎ y (φ \land z \in ω)$
36		nfra1	$⊢ Ⅎ y \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y)$
37	35 36	nfan	$⊢ Ⅎ y ((φ \land z \in ω) \land \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y))$
38	16	ad3antlr	$⊢ (((φ \land z \in ω) \land \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y)) \land y \in suc z) \to ({rec (F, B) ↾}_{ω}) (suc z) = F (({rec (F, B) ↾}_{ω}) (z))$
39		fveq2	$⊢ y = \emptyset \to ({rec (F, B) ↾}_{ω}) (y) = ({rec (F, B) ↾}_{ω}) (\emptyset)$
40	39	neeq2d	$⊢ y = \emptyset \to (F (({rec (F, B) ↾}_{ω}) (z)) \neq ({rec (F, B) ↾}_{ω}) (y) \leftrightarrow F (({rec (F, B) ↾}_{ω}) (z)) \neq ({rec (F, B) ↾}_{ω}) (\emptyset))$
41		peano2b	$⊢ z \in ω \leftrightarrow suc z \in ω$
42		elnn	$⊢ (y \in suc z \land suc z \in ω) \to y \in ω$
43	42	ancoms	$⊢ (suc z \in ω \land y \in suc z) \to y \in ω$
44	41 43	sylanb	$⊢ (z \in ω \land y \in suc z) \to y \in ω$
45	44	ad4ant24	$⊢ (((φ \land z \in ω) \land \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y)) \land y \in suc z) \to y \in ω$
46		nnsuc	$⊢ (y \in ω \land y \neq \emptyset) \to \exists x \in ω y = suc x$
47	45 46	sylan	$⊢ ((((φ \land z \in ω) \land \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y)) \land y \in suc z) \land y \neq \emptyset) \to \exists x \in ω y = suc x$
48		fveq2	$⊢ y = x \to ({rec (F, B) ↾}_{ω}) (y) = ({rec (F, B) ↾}_{ω}) (x)$
49	48	neeq2d	$⊢ y = x \to (({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y) \leftrightarrow ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (x))$
50		simp-4r	$⊢ (((((φ \land z \in ω) \land \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y)) \land y \in suc z) \land y \neq \emptyset) \land (x \in ω \land y = suc x)) \to \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y)$
51		simprr	$⊢ (((((φ \land z \in ω) \land \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y)) \land y \in suc z) \land y \neq \emptyset) \land (x \in ω \land y = suc x)) \to y = suc x$
52		simpllr	$⊢ (((((φ \land z \in ω) \land \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y)) \land y \in suc z) \land y \neq \emptyset) \land (x \in ω \land y = suc x)) \to y \in suc z$
53	51 52	eqeltrrd	$⊢ (((((φ \land z \in ω) \land \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y)) \land y \in suc z) \land y \neq \emptyset) \land (x \in ω \land y = suc x)) \to suc x \in suc z$
54		nnord	$⊢ z \in ω \to Ord z$
55	54	ad5antlr	$⊢ (((((φ \land z \in ω) \land \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y)) \land y \in suc z) \land y \neq \emptyset) \land (x \in ω \land y = suc x)) \to Ord z$
56		ordsucelsuc	$⊢ Ord z \to (x \in z \leftrightarrow suc x \in suc z)$
57	55 56	syl	$⊢ (((((φ \land z \in ω) \land \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y)) \land y \in suc z) \land y \neq \emptyset) \land (x \in ω \land y = suc x)) \to (x \in z \leftrightarrow suc x \in suc z)$
58	53 57	mpbird	$⊢ (((((φ \land z \in ω) \land \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y)) \land y \in suc z) \land y \neq \emptyset) \land (x \in ω \land y = suc x)) \to x \in z$
59	49 50 58	rspcdva	$⊢ (((((φ \land z \in ω) \land \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y)) \land y \in suc z) \land y \neq \emptyset) \land (x \in ω \land y = suc x)) \to ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (x)$
60		simp-5l	$⊢ (((((φ \land z \in ω) \land \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y)) \land y \in suc z) \land y \neq \emptyset) \land (x \in ω \land y = suc x)) \to φ$
61	60 1	syl	$⊢ (((((φ \land z \in ω) \land \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y)) \land y \in suc z) \land y \neq \emptyset) \land (x \in ω \land y = suc x)) \to F : A \underset{1-1}{⟶} A$
62	26	ffvelcdmda	$⊢ (φ \land z \in ω) \to ({rec (F, B) ↾}_{ω}) (z) \in A$
63	62	ad4antr	$⊢ (((((φ \land z \in ω) \land \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y)) \land y \in suc z) \land y \neq \emptyset) \land (x \in ω \land y = suc x)) \to ({rec (F, B) ↾}_{ω}) (z) \in A$
64		simprl	$⊢ (((((φ \land z \in ω) \land \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y)) \land y \in suc z) \land y \neq \emptyset) \land (x \in ω \land y = suc x)) \to x \in ω$
65	64 60 20	sylc	$⊢ (((((φ \land z \in ω) \land \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y)) \land y \in suc z) \land y \neq \emptyset) \land (x \in ω \land y = suc x)) \to ({rec (F, B) ↾}_{ω}) (x) \in A$
66		f1fveq	$⊢ (F : A \underset{1-1}{⟶} A \land (({rec (F, B) ↾}_{ω}) (z) \in A \land ({rec (F, B) ↾}_{ω}) (x) \in A)) \to (F (({rec (F, B) ↾}_{ω}) (z)) = F (({rec (F, B) ↾}_{ω}) (x)) \leftrightarrow ({rec (F, B) ↾}_{ω}) (z) = ({rec (F, B) ↾}_{ω}) (x))$
67	66	necon3bid	$⊢ (F : A \underset{1-1}{⟶} A \land (({rec (F, B) ↾}_{ω}) (z) \in A \land ({rec (F, B) ↾}_{ω}) (x) \in A)) \to (F (({rec (F, B) ↾}_{ω}) (z)) \neq F (({rec (F, B) ↾}_{ω}) (x)) \leftrightarrow ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (x))$
68	61 63 65 67	syl12anc	$⊢ (((((φ \land z \in ω) \land \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y)) \land y \in suc z) \land y \neq \emptyset) \land (x \in ω \land y = suc x)) \to (F (({rec (F, B) ↾}_{ω}) (z)) \neq F (({rec (F, B) ↾}_{ω}) (x)) \leftrightarrow ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (x))$
69	59 68	mpbird	$⊢ (((((φ \land z \in ω) \land \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y)) \land y \in suc z) \land y \neq \emptyset) \land (x \in ω \land y = suc x)) \to F (({rec (F, B) ↾}_{ω}) (z)) \neq F (({rec (F, B) ↾}_{ω}) (x))$
70		fveq2	$⊢ y = suc x \to ({rec (F, B) ↾}_{ω}) (y) = ({rec (F, B) ↾}_{ω}) (suc x)$
71		frsuc	$⊢ x \in ω \to ({rec (F, B) ↾}_{ω}) (suc x) = F (({rec (F, B) ↾}_{ω}) (x))$
72	70 71	sylan9eqr	$⊢ (x \in ω \land y = suc x) \to ({rec (F, B) ↾}_{ω}) (y) = F (({rec (F, B) ↾}_{ω}) (x))$
73	72	adantl	$⊢ (((((φ \land z \in ω) \land \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y)) \land y \in suc z) \land y \neq \emptyset) \land (x \in ω \land y = suc x)) \to ({rec (F, B) ↾}_{ω}) (y) = F (({rec (F, B) ↾}_{ω}) (x))$
74	69 73	neeqtrrd	$⊢ (((((φ \land z \in ω) \land \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y)) \land y \in suc z) \land y \neq \emptyset) \land (x \in ω \land y = suc x)) \to F (({rec (F, B) ↾}_{ω}) (z)) \neq ({rec (F, B) ↾}_{ω}) (y)$
75	47 74	rexlimddv	$⊢ ((((φ \land z \in ω) \land \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y)) \land y \in suc z) \land y \neq \emptyset) \to F (({rec (F, B) ↾}_{ω}) (z)) \neq ({rec (F, B) ↾}_{ω}) (y)$
76	14	ffnd	$⊢ φ \to F Fn A$
77	76	adantr	$⊢ (φ \land z \in ω) \to F Fn A$
78	77 62	fnfvelrnd	$⊢ (φ \land z \in ω) \to F (({rec (F, B) ↾}_{ω}) (z)) \in ran F$
79	11	adantr	$⊢ (φ \land z \in ω) \to ({rec (F, B) ↾}_{ω}) (\emptyset) \in (A ∖ ran F)$
80		elneeldif	$⊢ (F (({rec (F, B) ↾}_{ω}) (z)) \in ran F \land ({rec (F, B) ↾}_{ω}) (\emptyset) \in (A ∖ ran F)) \to F (({rec (F, B) ↾}_{ω}) (z)) \neq ({rec (F, B) ↾}_{ω}) (\emptyset)$
81	78 79 80	syl2anc	$⊢ (φ \land z \in ω) \to F (({rec (F, B) ↾}_{ω}) (z)) \neq ({rec (F, B) ↾}_{ω}) (\emptyset)$
82	81	ad2antrr	$⊢ (((φ \land z \in ω) \land \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y)) \land y \in suc z) \to F (({rec (F, B) ↾}_{ω}) (z)) \neq ({rec (F, B) ↾}_{ω}) (\emptyset)$
83	40 75 82	pm2.61ne	$⊢ (((φ \land z \in ω) \land \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y)) \land y \in suc z) \to F (({rec (F, B) ↾}_{ω}) (z)) \neq ({rec (F, B) ↾}_{ω}) (y)$
84	38 83	eqnetrd	$⊢ (((φ \land z \in ω) \land \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y)) \land y \in suc z) \to ({rec (F, B) ↾}_{ω}) (suc z) \neq ({rec (F, B) ↾}_{ω}) (y)$
85	37 84	ralrimia	$⊢ ((φ \land z \in ω) \land \forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y)) \to \forall y \in suc z ({rec (F, B) ↾}_{ω}) (suc z) \neq ({rec (F, B) ↾}_{ω}) (y)$
86	85	exp31	$⊢ φ \to (z \in ω \to (\forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y) \to \forall y \in suc z ({rec (F, B) ↾}_{ω}) (suc z) \neq ({rec (F, B) ↾}_{ω}) (y)))$
87	86	com12	$⊢ z \in ω \to (φ \to (\forall y \in z ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (y) \to \forall y \in suc z ({rec (F, B) ↾}_{ω}) (suc z) \neq ({rec (F, B) ↾}_{ω}) (y)))$
88	28 30 32 34 87	finds2	$⊢ x \in ω \to (φ \to \forall y \in x ({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (y))$
89		rsp	$⊢ \forall y \in x ({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (y) \to (y \in x \to ({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (y))$
90	88 89	syl6com	$⊢ φ \to (x \in ω \to (y \in x \to ({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (y)))$
91	90	adantrd	$⊢ φ \to ((x \in ω \land y \in ω) \to (y \in x \to ({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (y)))$
92	91	ralrimivv	$⊢ φ \to \forall x \in ω \forall y \in ω (y \in x \to ({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (y))$
93		omsson	$⊢ ω \subseteq On$
94		onelfvnef1	$⊢ (({rec (F, B) ↾}_{ω}) : ω ⟶ A \land ω \subseteq On \land \forall x \in ω \forall y \in ω (y \in x \to ({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (y))) \to ({rec (F, B) ↾}_{ω}) : ω \underset{1-1}{⟶} A$
95	93 94	mp3an2	$⊢ (({rec (F, B) ↾}_{ω}) : ω ⟶ A \land \forall x \in ω \forall y \in ω (y \in x \to ({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (y))) \to ({rec (F, B) ↾}_{ω}) : ω \underset{1-1}{⟶} A$
96	26 92 95	syl2anc	$⊢ φ \to ({rec (F, B) ↾}_{ω}) : ω \underset{1-1}{⟶} A$

Metamath Proof Explorer

Theorem mh-inf3f1

Proof