Theorem mh-inf3f1 37506

Description: A variant of inf3 9660. If 𝐹 is a one-to-one function from 𝐴 into itself, and 𝐵 is an element outside its range, then (rec(𝐹, 𝐵) ↾ ω) is a one-to-one function yielding an infinite sequence of distinct elements from 𝐴. If 𝐴 is a set, we can use this theorem to prove ω ∈ V via f1dmex 7990. (Contributed by Matthew House, 13-Apr-2026.)

Hypotheses

Ref	Expression
mh-inf3f1.1	⊢ (𝜑 → 𝐹:𝐴⟶1-1𝐴)
mh-inf3f1.2	⊢ (𝜑 → 𝐵 ∈ (𝐴 ∖ ran 𝐹))

Assertion

Ref	Expression
mh-inf3f1	⊢ (𝜑 → (rec(𝐹, 𝐵) ↾ ω):ω⟶1-1𝐴)

Proof of Theorem mh-inf3f1

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6905	. . . . . . 7 ⊢ (𝑥 = ∅ → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘∅))
2	1	eleq1d 2849	. . . . . 6 ⊢ (𝑥 = ∅ → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω)‘∅) ∈ 𝐴))
3		fveq2 6905	. . . . . . 7 ⊢ (𝑥 = 𝑧 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑧))
4	3	eleq1d 2849	. . . . . 6 ⊢ (𝑥 = 𝑧 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ∈ 𝐴))
5		fveq2 6905	. . . . . . 7 ⊢ (𝑥 = suc 𝑧 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧))
6	5	eleq1d 2849	. . . . . 6 ⊢ (𝑥 = suc 𝑧 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) ∈ 𝐴))
7		mh-inf3f1.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ (𝐴 ∖ ran 𝐹))
8		fr0g 8469	. . . . . . . . 9 ⊢ (𝐵 ∈ (𝐴 ∖ ran 𝐹) → ((rec(𝐹, 𝐵) ↾ ω)‘∅) = 𝐵)
9	7, 8	syl 18	. . . . . . . 8 ⊢ (𝜑 → ((rec(𝐹, 𝐵) ↾ ω)‘∅) = 𝐵)
10	9, 7	eqeltrd 2864	. . . . . . 7 ⊢ (𝜑 → ((rec(𝐹, 𝐵) ↾ ω)‘∅) ∈ (𝐴 ∖ ran 𝐹))
11	10	eldifad 4054	. . . . . 6 ⊢ (𝜑 → ((rec(𝐹, 𝐵) ↾ ω)‘∅) ∈ 𝐴)
12		mh-inf3f1.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐴⟶1-1𝐴)
13		f1f 6797	. . . . . . . . . 10 ⊢ (𝐹:𝐴⟶1-1𝐴 → 𝐹:𝐴⟶𝐴)
14	12, 13	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:𝐴⟶𝐴)
15	14	ffvelcdmda 7105	. . . . . . . 8 ⊢ ((𝜑 ∧ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ∈ 𝐴) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ∈ 𝐴)
16		frsuc 8470	. . . . . . . . 9 ⊢ (𝑧 ∈ ω → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
17	16	eleq1d 2849	. . . . . . . 8 ⊢ (𝑧 ∈ ω → (((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) ∈ 𝐴 ↔ (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ∈ 𝐴))
18	15, 17	imbitrrid 249	. . . . . . 7 ⊢ (𝑧 ∈ ω → ((𝜑 ∧ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ∈ 𝐴) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) ∈ 𝐴))
19	18	expd 421	. . . . . 6 ⊢ (𝑧 ∈ ω → (𝜑 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ∈ 𝐴 → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) ∈ 𝐴)))
20	2, 4, 6, 11, 19	finds2 7931	. . . . 5 ⊢ (𝑥 ∈ ω → (𝜑 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴))
21	20	com12 33	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ω → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴))
22	21	ralrimiv 3157	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ ω ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴)
23		frfnom 8468	. . . 4 ⊢ (rec(𝐹, 𝐵) ↾ ω) Fn ω
24		ffnfv 7140	. . . 4 ⊢ ((rec(𝐹, 𝐵) ↾ ω):ω⟶𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω) Fn ω ∧ ∀𝑥 ∈ ω ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴))
25	23, 24	mpbiran 722	. . 3 ⊢ ((rec(𝐹, 𝐵) ↾ ω):ω⟶𝐴 ↔ ∀𝑥 ∈ ω ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴)
26	22, 25	sylibr 237	. 2 ⊢ (𝜑 → (rec(𝐹, 𝐵) ↾ ω):ω⟶𝐴)
27	1	neeq1d 3018	. . . . . . 7 ⊢ (𝑥 = ∅ → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘∅) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
28	27	raleqbi1dv 3333	. . . . . 6 ⊢ (𝑥 = ∅ → (∀𝑦 ∈ 𝑥 ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) ↔ ∀𝑦 ∈ ∅ ((rec(𝐹, 𝐵) ↾ ω)‘∅) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
29	3	neeq1d 3018	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
30	29	raleqbi1dv 3333	. . . . . 6 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) ↔ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
31	5	neeq1d 3018	. . . . . . 7 ⊢ (𝑥 = suc 𝑧 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
32	31	raleqbi1dv 3333	. . . . . 6 ⊢ (𝑥 = suc 𝑧 → (∀𝑦 ∈ 𝑥 ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) ↔ ∀𝑦 ∈ suc 𝑧((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
33		ral0 4457	. . . . . . 7 ⊢ ∀𝑦 ∈ ∅ ((rec(𝐹, 𝐵) ↾ ω)‘∅) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)
34	33	a1i 11	. . . . . 6 ⊢ (𝜑 → ∀𝑦 ∈ ∅ ((rec(𝐹, 𝐵) ↾ ω)‘∅) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))
35		nfv 1949	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑧 ∈ ω)
36		nfra1 3290	. . . . . . . . . 10 ⊢ Ⅎ𝑦∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)
37	35, 36	nfan 1934	. . . . . . . . 9 ⊢ Ⅎ𝑦((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))
38	16	ad3antlr 744	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
39		fveq2 6905	. . . . . . . . . . . 12 ⊢ (𝑦 = ∅ → ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) = ((rec(𝐹, 𝐵) ↾ ω)‘∅))
40	39	neeq2d 3019	. . . . . . . . . . 11 ⊢ (𝑦 = ∅ → ((𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) ↔ (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘∅)))
41		peano2b 7915	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ω ↔ suc 𝑧 ∈ ω)
42		elnn 7909	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ suc 𝑧 ∧ suc 𝑧 ∈ ω) → 𝑦 ∈ ω)
43	42	ancoms 464	. . . . . . . . . . . . . . 15 ⊢ ((suc 𝑧 ∈ ω ∧ 𝑦 ∈ suc 𝑧) → 𝑦 ∈ ω)
44	41, 43	sylanb 593	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ ω ∧ 𝑦 ∈ suc 𝑧) → 𝑦 ∈ ω)
45	44	ad4ant24 767	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) → 𝑦 ∈ ω)
46		nnsuc 7916	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ω ∧ 𝑦 ≠ ∅) → ∃𝑥 ∈ ω 𝑦 = suc 𝑥)
47	45, 46	sylan 592	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) ∧ 𝑦 ≠ ∅) → ∃𝑥 ∈ ω 𝑦 = suc 𝑥)
48		fveq2 6905	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑥))
49	48	neeq2d 3019	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑥 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑥)))
50		simp-4r 796	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∈ ω ∧ 𝑦 = suc 𝑥)) → ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))
51		simprr 785	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∈ ω ∧ 𝑦 = suc 𝑥)) → 𝑦 = suc 𝑥)
52		simpllr 788	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∈ ω ∧ 𝑦 = suc 𝑥)) → 𝑦 ∈ suc 𝑧)
53	51, 52	eqeltrrd 2865	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∈ ω ∧ 𝑦 = suc 𝑥)) → suc 𝑥 ∈ suc 𝑧)
54		nnord 7906	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ω → Ord 𝑧)
55	54	ad5antlr 748	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∈ ω ∧ 𝑦 = suc 𝑥)) → Ord 𝑧)
56		ordsucelsuc 7854	. . . . . . . . . . . . . . . . 17 ⊢ (Ord 𝑧 → (𝑥 ∈ 𝑧 ↔ suc 𝑥 ∈ suc 𝑧))
57	55, 56	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∈ ω ∧ 𝑦 = suc 𝑥)) → (𝑥 ∈ 𝑧 ↔ suc 𝑥 ∈ suc 𝑧))
58	53, 57	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∈ ω ∧ 𝑦 = suc 𝑥)) → 𝑥 ∈ 𝑧)
59	49, 50, 58	rspcdva 3581	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∈ ω ∧ 𝑦 = suc 𝑥)) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑥))
60		simp-5l 797	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∈ ω ∧ 𝑦 = suc 𝑥)) → 𝜑)
61	60, 12	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∈ ω ∧ 𝑦 = suc 𝑥)) → 𝐹:𝐴⟶1-1𝐴)
62	26	ffvelcdmda 7105	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ∈ 𝐴)
63	62	ad4antr 745	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∈ ω ∧ 𝑦 = suc 𝑥)) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ∈ 𝐴)
64		simprl 783	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∈ ω ∧ 𝑦 = suc 𝑥)) → 𝑥 ∈ ω)
65	64, 60, 20	sylc 66	. . . . . . . . . . . . . . 15 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∈ ω ∧ 𝑦 = suc 𝑥)) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴)
66		f1fveq 7286	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝐴⟶1-1𝐴 ∧ (((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ∈ 𝐴 ∧ ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴)) → ((𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑥)) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑥)))
67	66	necon3bid 3003	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐴⟶1-1𝐴 ∧ (((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ∈ 𝐴 ∧ ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴)) → ((𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑥)) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑥)))
68	61, 63, 65, 67	syl12anc 850	. . . . . . . . . . . . . 14 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∈ ω ∧ 𝑦 = suc 𝑥)) → ((𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑥)) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑥)))
69	59, 68	mpbird 260	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∈ ω ∧ 𝑦 = suc 𝑥)) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑥)))
70		fveq2 6905	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = suc 𝑥 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) = ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑥))
71		frsuc 8470	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ω → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑥) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑥)))
72	70, 71	sylan9eqr 2820	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ω ∧ 𝑦 = suc 𝑥) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑥)))
73	72	adantl 487	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∈ ω ∧ 𝑦 = suc 𝑥)) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑥)))
74	69, 73	neeqtrrd 3033	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∈ ω ∧ 𝑦 = suc 𝑥)) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))
75	47, 74	rexlimddv 3173	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) ∧ 𝑦 ≠ ∅) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))
76	14	ffnd 6729	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 Fn 𝐴)
77	76	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → 𝐹 Fn 𝐴)
78	77, 62	fnfvelrnd 7103	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ∈ ran 𝐹)
79	10	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘∅) ∈ (𝐴 ∖ ran 𝐹))
80		elneeldif 4056	. . . . . . . . . . . . 13 ⊢ (((𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ∈ ran 𝐹 ∧ ((rec(𝐹, 𝐵) ↾ ω)‘∅) ∈ (𝐴 ∖ ran 𝐹)) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘∅))
81	78, 79, 80	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘∅))
82	81	ad2antrr 739	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘∅))
83	40, 75, 82	pm2.61ne 3044	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))
84	38, 83	eqnetrd 3026	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))
85	37, 84	ralrimia 3265	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) → ∀𝑦 ∈ suc 𝑧((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))
86	85	exp31 425	. . . . . . 7 ⊢ (𝜑 → (𝑧 ∈ ω → (∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) → ∀𝑦 ∈ suc 𝑧((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))))
87	86	com12 33	. . . . . 6 ⊢ (𝑧 ∈ ω → (𝜑 → (∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) → ∀𝑦 ∈ suc 𝑧((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))))
88	28, 30, 32, 34, 87	finds2 7931	. . . . 5 ⊢ (𝑥 ∈ ω → (𝜑 → ∀𝑦 ∈ 𝑥 ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
89		rsp 3254	. . . . 5 ⊢ (∀𝑦 ∈ 𝑥 ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) → (𝑦 ∈ 𝑥 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
90	88, 89	syl6com 38	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ω → (𝑦 ∈ 𝑥 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))))
91	90	adantrd 497	. . 3 ⊢ (𝜑 → ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝑦 ∈ 𝑥 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))))
92	91	ralrimivv 3207	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
93		omsson 7902	. . 3 ⊢ ω ⊆ On
94		onelfvnef1 8474	. . 3 ⊢ (((rec(𝐹, 𝐵) ↾ ω):ω⟶𝐴 ∧ ω ⊆ On ∧ ∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))) → (rec(𝐹, 𝐵) ↾ ω):ω⟶1-1𝐴)
95	93, 94	mp3an2 1479	. 2 ⊢ (((rec(𝐹, 𝐵) ↾ ω):ω⟶𝐴 ∧ ∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))) → (rec(𝐹, 𝐵) ↾ ω):ω⟶1-1𝐴)
96	26, 92, 95	syl2anc 596	1 ⊢ (𝜑 → (rec(𝐹, 𝐵) ↾ ω):ω⟶1-1𝐴)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2147   ≠ wne 2959  ∀wral 3080  ∃wrex 3090   ⊆ wss 3900   ∖ cdif 4048  ∅c0 4281  ran crn 5656   ↾ cres 5657  Ord word 6376  Oncon0 6377  suc csuc 6379   Fn wfn 6550  ⟶wf 6551  ⟶1-1wf1 6552  ‘cfv 6555  ωcom 7898  reccrdg 8442

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-un 7772

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6319  df-ord 6380  df-on 6381  df-lim 6382  df-suc 6383  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-ov 7443  df-om 7899  df-2nd 8023  df-frecs 8324  df-wrecs 8355  df-recs 8404  df-rdg 8443

This theorem is used by:  mh-inf3sn  37507