mh-inf3f1

Description: A variant of inf3 . If F is a one-to-one function from A into itself, and there exists an element B not in its range, then ` ( rec ( F , B ) |`_om ) is 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		frfnom	$⊢ ({rec (F, B) ↾}_{ω}) Fn ω$
4	3	a1i	$⊢ φ \to ({rec (F, B) ↾}_{ω}) Fn ω$
5		fveq2	$⊢ x = \emptyset \to ({rec (F, B) ↾}_{ω}) (x) = ({rec (F, B) ↾}_{ω}) (\emptyset)$
6	5	eleq1d	$⊢ x = \emptyset \to (({rec (F, B) ↾}_{ω}) (x) \in A \leftrightarrow ({rec (F, B) ↾}_{ω}) (\emptyset) \in A)$
7		fveq2	$⊢ x = w \to ({rec (F, B) ↾}_{ω}) (x) = ({rec (F, B) ↾}_{ω}) (w)$
8	7	eleq1d	$⊢ x = w \to (({rec (F, B) ↾}_{ω}) (x) \in A \leftrightarrow ({rec (F, B) ↾}_{ω}) (w) \in A)$
9		fveq2	$⊢ x = suc w \to ({rec (F, B) ↾}_{ω}) (x) = ({rec (F, B) ↾}_{ω}) (suc w)$
10	9	eleq1d	$⊢ x = suc w \to (({rec (F, B) ↾}_{ω}) (x) \in A \leftrightarrow ({rec (F, B) ↾}_{ω}) (suc w) \in A)$
11	2	eldifad	$⊢ φ \to B \in A$
12		fr0g	$⊢ B \in A \to ({rec (F, B) ↾}_{ω}) (\emptyset) = B$
13	11 12	syl	$⊢ φ \to ({rec (F, B) ↾}_{ω}) (\emptyset) = B$
14	13 11	eqeltrd	$⊢ φ \to ({rec (F, B) ↾}_{ω}) (\emptyset) \in A$
15		f1f	$⊢ F : A \underset{1-1}{⟶} A \to F : A ⟶ A$
16	1 15	syl	$⊢ φ \to F : A ⟶ A$
17	16	ffvelcdmda	$⊢ (φ \land ({rec (F, B) ↾}_{ω}) (w) \in A) \to F (({rec (F, B) ↾}_{ω}) (w)) \in A$
18		frsuc	$⊢ w \in ω \to ({rec (F, B) ↾}_{ω}) (suc w) = F (({rec (F, B) ↾}_{ω}) (w))$
19	18	eleq1d	$⊢ w \in ω \to (({rec (F, B) ↾}_{ω}) (suc w) \in A \leftrightarrow F (({rec (F, B) ↾}_{ω}) (w)) \in A)$
20	17 19	imbitrrid	$⊢ w \in ω \to ((φ \land ({rec (F, B) ↾}_{ω}) (w) \in A) \to ({rec (F, B) ↾}_{ω}) (suc w) \in A)$
21	20	expd	$⊢ w \in ω \to (φ \to (({rec (F, B) ↾}_{ω}) (w) \in A \to ({rec (F, B) ↾}_{ω}) (suc w) \in A))$
22	6 8 10 14 21	finds2	$⊢ x \in ω \to (φ \to ({rec (F, B) ↾}_{ω}) (x) \in A)$
23	22	com12	$⊢ φ \to (x \in ω \to ({rec (F, B) ↾}_{ω}) (x) \in A)$
24	23	ralrimiv	$⊢ φ \to \forall x \in ω ({rec (F, B) ↾}_{ω}) (x) \in A$
25		ffnfv	$⊢ ({rec (F, B) ↾}_{ω}) : ω ⟶ A \leftrightarrow (({rec (F, B) ↾}_{ω}) Fn ω \land \forall x \in ω ({rec (F, B) ↾}_{ω}) (x) \in A)$
26	4 24 25	sylanbrc	$⊢ φ \to ({rec (F, B) ↾}_{ω}) : ω ⟶ A$
27		nnord	$⊢ z \in ω \to Ord z$
28		nnord	$⊢ w \in ω \to Ord w$
29		ordtri3	$⊢ (Ord z \land Ord w) \to (z = w \leftrightarrow \neg (z \in w \lor w \in z))$
30	27 28 29	syl2an	$⊢ (z \in ω \land w \in ω) \to (z = w \leftrightarrow \neg (z \in w \lor w \in z))$
31	30	adantl	$⊢ (φ \land (z \in ω \land w \in ω)) \to (z = w \leftrightarrow \neg (z \in w \lor w \in z))$
32	31	necon2abid	$⊢ (φ \land (z \in ω \land w \in ω)) \to ((z \in w \lor w \in z) \leftrightarrow z \neq w)$
33		vex	$⊢ z \in V$
34		vex	$⊢ w \in V$
35		simpl	$⊢ (x = z \land y = w) \to x = z$
36	35	eleq1d	$⊢ (x = z \land y = w) \to (x \in ω \leftrightarrow z \in ω)$
37		simpr	$⊢ (x = z \land y = w) \to y = w$
38	37	eleq1d	$⊢ (x = z \land y = w) \to (y \in ω \leftrightarrow w \in ω)$
39	36 38	anbi12d	$⊢ (x = z \land y = w) \to ((x \in ω \land y \in ω) \leftrightarrow (z \in ω \land w \in ω))$
40	39	anbi2d	$⊢ (x = z \land y = w) \to ((φ \land (x \in ω \land y \in ω)) \leftrightarrow (φ \land (z \in ω \land w \in ω)))$
41		elequ12	$⊢ (x = z \land y = w) \to (x \in y \leftrightarrow z \in w)$
42	35	fveq2d	$⊢ (x = z \land y = w) \to ({rec (F, B) ↾}_{ω}) (x) = ({rec (F, B) ↾}_{ω}) (z)$
43	37	fveq2d	$⊢ (x = z \land y = w) \to ({rec (F, B) ↾}_{ω}) (y) = ({rec (F, B) ↾}_{ω}) (w)$
44	42 43	neeq12d	$⊢ (x = z \land y = w) \to (({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (y) \leftrightarrow ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (w))$
45	41 44	imbi12d	$⊢ (x = z \land y = w) \to ((x \in y \to ({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (y)) \leftrightarrow (z \in w \to ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (w)))$
46	40 45	imbi12d	$⊢ (x = z \land y = w) \to (((φ \land (x \in ω \land y \in ω)) \to (x \in y \to ({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (y))) \leftrightarrow ((φ \land (z \in ω \land w \in ω)) \to (z \in w \to ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (w))))$
47		nnaordex2	$⊢ (x \in ω \land y \in ω) \to (x \in y \leftrightarrow \exists z \in ω x +_{𝑜} suc z = y)$
48	47	adantl	$⊢ (φ \land (x \in ω \land y \in ω)) \to (x \in y \leftrightarrow \exists z \in ω x +_{𝑜} suc z = y)$
49		oveq2	$⊢ x = \emptyset \to suc z +_{𝑜} x = suc z +_{𝑜} \emptyset$
50	49	fveq2d	$⊢ x = \emptyset \to ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} x) = ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} \emptyset)$
51	5 50	neeq12d	$⊢ x = \emptyset \to (({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} x) \leftrightarrow ({rec (F, B) ↾}_{ω}) (\emptyset) \neq ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} \emptyset))$
52		oveq2	$⊢ x = w \to suc z +_{𝑜} x = suc z +_{𝑜} w$
53	52	fveq2d	$⊢ x = w \to ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} x) = ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} w)$
54	7 53	neeq12d	$⊢ x = w \to (({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} x) \leftrightarrow ({rec (F, B) ↾}_{ω}) (w) \neq ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} w))$
55		oveq2	$⊢ x = suc w \to suc z +_{𝑜} x = suc z +_{𝑜} suc w$
56	55	fveq2d	$⊢ x = suc w \to ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} x) = ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} suc w)$
57	9 56	neeq12d	$⊢ x = suc w \to (({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} x) \leftrightarrow ({rec (F, B) ↾}_{ω}) (suc w) \neq ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} suc w))$
58	16	ffnd	$⊢ φ \to F Fn A$
59	58	adantr	$⊢ (φ \land z \in ω) \to F Fn A$
60	26	ffvelcdmda	$⊢ (φ \land z \in ω) \to ({rec (F, B) ↾}_{ω}) (z) \in A$
61	59 60	fnfvelrnd	$⊢ (φ \land z \in ω) \to F (({rec (F, B) ↾}_{ω}) (z)) \in ran F$
62	2	eldifbd	$⊢ φ \to \neg B \in ran F$
63	62	adantr	$⊢ (φ \land z \in ω) \to \neg B \in ran F$
64		nelne2	$⊢ (F (({rec (F, B) ↾}_{ω}) (z)) \in ran F \land \neg B \in ran F) \to F (({rec (F, B) ↾}_{ω}) (z)) \neq B$
65	61 63 64	syl2anc	$⊢ (φ \land z \in ω) \to F (({rec (F, B) ↾}_{ω}) (z)) \neq B$
66	65	necomd	$⊢ (φ \land z \in ω) \to B \neq F (({rec (F, B) ↾}_{ω}) (z))$
67	13	adantr	$⊢ (φ \land z \in ω) \to ({rec (F, B) ↾}_{ω}) (\emptyset) = B$
68		peano2	$⊢ z \in ω \to suc z \in ω$
69	68	adantl	$⊢ (φ \land z \in ω) \to suc z \in ω$
70		nna0	$⊢ suc z \in ω \to suc z +_{𝑜} \emptyset = suc z$
71	69 70	syl	$⊢ (φ \land z \in ω) \to suc z +_{𝑜} \emptyset = suc z$
72	71	fveq2d	$⊢ (φ \land z \in ω) \to ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} \emptyset) = ({rec (F, B) ↾}_{ω}) (suc z)$
73		frsuc	$⊢ z \in ω \to ({rec (F, B) ↾}_{ω}) (suc z) = F (({rec (F, B) ↾}_{ω}) (z))$
74	73	adantl	$⊢ (φ \land z \in ω) \to ({rec (F, B) ↾}_{ω}) (suc z) = F (({rec (F, B) ↾}_{ω}) (z))$
75	72 74	eqtrd	$⊢ (φ \land z \in ω) \to ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} \emptyset) = F (({rec (F, B) ↾}_{ω}) (z))$
76	66 67 75	3netr4d	$⊢ (φ \land z \in ω) \to ({rec (F, B) ↾}_{ω}) (\emptyset) \neq ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} \emptyset)$
77	18	adantl	$⊢ ((φ \land z \in ω) \land w \in ω) \to ({rec (F, B) ↾}_{ω}) (suc w) = F (({rec (F, B) ↾}_{ω}) (w))$
78		nnasuc	$⊢ (suc z \in ω \land w \in ω) \to suc z +_{𝑜} suc w = suc (suc z +_{𝑜} w)$
79	69 78	sylan	$⊢ ((φ \land z \in ω) \land w \in ω) \to suc z +_{𝑜} suc w = suc (suc z +_{𝑜} w)$
80	79	fveq2d	$⊢ ((φ \land z \in ω) \land w \in ω) \to ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} suc w) = ({rec (F, B) ↾}_{ω}) (suc (suc z +_{𝑜} w))$
81		nnacl	$⊢ (suc z \in ω \land w \in ω) \to suc z +_{𝑜} w \in ω$
82	69 81	sylan	$⊢ ((φ \land z \in ω) \land w \in ω) \to suc z +_{𝑜} w \in ω$
83		frsuc	$⊢ suc z +_{𝑜} w \in ω \to ({rec (F, B) ↾}_{ω}) (suc (suc z +_{𝑜} w)) = F (({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} w))$
84	82 83	syl	$⊢ ((φ \land z \in ω) \land w \in ω) \to ({rec (F, B) ↾}_{ω}) (suc (suc z +_{𝑜} w)) = F (({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} w))$
85	80 84	eqtrd	$⊢ ((φ \land z \in ω) \land w \in ω) \to ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} suc w) = F (({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} w))$
86	77 85	eqeq12d	$⊢ ((φ \land z \in ω) \land w \in ω) \to (({rec (F, B) ↾}_{ω}) (suc w) = ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} suc w) \leftrightarrow F (({rec (F, B) ↾}_{ω}) (w)) = F (({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} w)))$
87	1	ad2antrr	$⊢ ((φ \land z \in ω) \land w \in ω) \to F : A \underset{1-1}{⟶} A$
88	26	ad2antrr	$⊢ ((φ \land z \in ω) \land w \in ω) \to ({rec (F, B) ↾}_{ω}) : ω ⟶ A$
89		simpr	$⊢ ((φ \land z \in ω) \land w \in ω) \to w \in ω$
90	88 89	ffvelcdmd	$⊢ ((φ \land z \in ω) \land w \in ω) \to ({rec (F, B) ↾}_{ω}) (w) \in A$
91	88 82	ffvelcdmd	$⊢ ((φ \land z \in ω) \land w \in ω) \to ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} w) \in A$
92		f1veqaeq	$⊢ (F : A \underset{1-1}{⟶} A \land (({rec (F, B) ↾}_{ω}) (w) \in A \land ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} w) \in A)) \to (F (({rec (F, B) ↾}_{ω}) (w)) = F (({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} w)) \to ({rec (F, B) ↾}_{ω}) (w) = ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} w))$
93	87 90 91 92	syl12anc	$⊢ ((φ \land z \in ω) \land w \in ω) \to (F (({rec (F, B) ↾}_{ω}) (w)) = F (({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} w)) \to ({rec (F, B) ↾}_{ω}) (w) = ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} w))$
94	86 93	sylbid	$⊢ ((φ \land z \in ω) \land w \in ω) \to (({rec (F, B) ↾}_{ω}) (suc w) = ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} suc w) \to ({rec (F, B) ↾}_{ω}) (w) = ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} w))$
95	94	necon3d	$⊢ ((φ \land z \in ω) \land w \in ω) \to (({rec (F, B) ↾}_{ω}) (w) \neq ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} w) \to ({rec (F, B) ↾}_{ω}) (suc w) \neq ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} suc w))$
96	95	expcom	$⊢ w \in ω \to ((φ \land z \in ω) \to (({rec (F, B) ↾}_{ω}) (w) \neq ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} w) \to ({rec (F, B) ↾}_{ω}) (suc w) \neq ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} suc w)))$
97	51 54 57 76 96	finds2	$⊢ x \in ω \to ((φ \land z \in ω) \to ({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} x))$
98	97	impcom	$⊢ ((φ \land z \in ω) \land x \in ω) \to ({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} x)$
99	98	an32s	$⊢ ((φ \land x \in ω) \land z \in ω) \to ({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} x)$
100	99	adantrr	$⊢ ((φ \land x \in ω) \land (z \in ω \land x +_{𝑜} suc z = y)) \to ({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} x)$
101	68	ad2antrl	$⊢ ((φ \land x \in ω) \land (z \in ω \land x +_{𝑜} suc z = y)) \to suc z \in ω$
102		simplr	$⊢ ((φ \land x \in ω) \land (z \in ω \land x +_{𝑜} suc z = y)) \to x \in ω$
103		nnacom	$⊢ (suc z \in ω \land x \in ω) \to suc z +_{𝑜} x = x +_{𝑜} suc z$
104	101 102 103	syl2anc	$⊢ ((φ \land x \in ω) \land (z \in ω \land x +_{𝑜} suc z = y)) \to suc z +_{𝑜} x = x +_{𝑜} suc z$
105		simprr	$⊢ ((φ \land x \in ω) \land (z \in ω \land x +_{𝑜} suc z = y)) \to x +_{𝑜} suc z = y$
106	104 105	eqtrd	$⊢ ((φ \land x \in ω) \land (z \in ω \land x +_{𝑜} suc z = y)) \to suc z +_{𝑜} x = y$
107	106	fveq2d	$⊢ ((φ \land x \in ω) \land (z \in ω \land x +_{𝑜} suc z = y)) \to ({rec (F, B) ↾}_{ω}) (suc z +_{𝑜} x) = ({rec (F, B) ↾}_{ω}) (y)$
108	100 107	neeqtrd	$⊢ ((φ \land x \in ω) \land (z \in ω \land x +_{𝑜} suc z = y)) \to ({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (y)$
109	108	rexlimdvaa	$⊢ (φ \land x \in ω) \to (\exists z \in ω x +_{𝑜} suc z = y \to ({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (y))$
110	109	adantrr	$⊢ (φ \land (x \in ω \land y \in ω)) \to (\exists z \in ω x +_{𝑜} suc z = y \to ({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (y))$
111	48 110	sylbid	$⊢ (φ \land (x \in ω \land y \in ω)) \to (x \in y \to ({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (y))$
112	33 34 46 111	vtocl2	$⊢ (φ \land (z \in ω \land w \in ω)) \to (z \in w \to ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (w))$
113		simpl	$⊢ (x = w \land y = z) \to x = w$
114	113	eleq1d	$⊢ (x = w \land y = z) \to (x \in ω \leftrightarrow w \in ω)$
115		simpr	$⊢ (x = w \land y = z) \to y = z$
116	115	eleq1d	$⊢ (x = w \land y = z) \to (y \in ω \leftrightarrow z \in ω)$
117	114 116	anbi12d	$⊢ (x = w \land y = z) \to ((x \in ω \land y \in ω) \leftrightarrow (w \in ω \land z \in ω))$
118	117	anbi2d	$⊢ (x = w \land y = z) \to ((φ \land (x \in ω \land y \in ω)) \leftrightarrow (φ \land (w \in ω \land z \in ω)))$
119		elequ12	$⊢ (x = w \land y = z) \to (x \in y \leftrightarrow w \in z)$
120	113	fveq2d	$⊢ (x = w \land y = z) \to ({rec (F, B) ↾}_{ω}) (x) = ({rec (F, B) ↾}_{ω}) (w)$
121	115	fveq2d	$⊢ (x = w \land y = z) \to ({rec (F, B) ↾}_{ω}) (y) = ({rec (F, B) ↾}_{ω}) (z)$
122	120 121	neeq12d	$⊢ (x = w \land y = z) \to (({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (y) \leftrightarrow ({rec (F, B) ↾}_{ω}) (w) \neq ({rec (F, B) ↾}_{ω}) (z))$
123	119 122	imbi12d	$⊢ (x = w \land y = z) \to ((x \in y \to ({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (y)) \leftrightarrow (w \in z \to ({rec (F, B) ↾}_{ω}) (w) \neq ({rec (F, B) ↾}_{ω}) (z)))$
124	118 123	imbi12d	$⊢ (x = w \land y = z) \to (((φ \land (x \in ω \land y \in ω)) \to (x \in y \to ({rec (F, B) ↾}_{ω}) (x) \neq ({rec (F, B) ↾}_{ω}) (y))) \leftrightarrow ((φ \land (w \in ω \land z \in ω)) \to (w \in z \to ({rec (F, B) ↾}_{ω}) (w) \neq ({rec (F, B) ↾}_{ω}) (z))))$
125	34 33 124 111	vtocl2	$⊢ (φ \land (w \in ω \land z \in ω)) \to (w \in z \to ({rec (F, B) ↾}_{ω}) (w) \neq ({rec (F, B) ↾}_{ω}) (z))$
126	125	ancom2s	$⊢ (φ \land (z \in ω \land w \in ω)) \to (w \in z \to ({rec (F, B) ↾}_{ω}) (w) \neq ({rec (F, B) ↾}_{ω}) (z))$
127		necom	$⊢ ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (w) \leftrightarrow ({rec (F, B) ↾}_{ω}) (w) \neq ({rec (F, B) ↾}_{ω}) (z)$
128	126 127	imbitrrdi	$⊢ (φ \land (z \in ω \land w \in ω)) \to (w \in z \to ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (w))$
129	112 128	jaod	$⊢ (φ \land (z \in ω \land w \in ω)) \to ((z \in w \lor w \in z) \to ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (w))$
130	32 129	sylbird	$⊢ (φ \land (z \in ω \land w \in ω)) \to (z \neq w \to ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (w))$
131	130	ralrimivva	$⊢ φ \to \forall z \in ω \forall w \in ω (z \neq w \to ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (w))$
132		dff14a	$⊢ ({rec (F, B) ↾}_{ω}) : ω \underset{1-1}{⟶} A \leftrightarrow (({rec (F, B) ↾}_{ω}) : ω ⟶ A \land \forall z \in ω \forall w \in ω (z \neq w \to ({rec (F, B) ↾}_{ω}) (z) \neq ({rec (F, B) ↾}_{ω}) (w)))$
133	26 131 132	sylanbrc	$⊢ φ \to ({rec (F, B) ↾}_{ω}) : ω \underset{1-1}{⟶} A$

Metamath Proof Explorer

Theorem mh-inf3f1

Proof