Theorem mh-inf3f1 37329

Description: A variant of inf3 9636. 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 7969. (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 6885	. . . . . . 7 ⊢ (𝑥 = ∅ → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘∅))
2	1	eleq1d 2845	. . . . . 6 ⊢ (𝑥 = ∅ → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω)‘∅) ∈ 𝐴))
3		fveq2 6885	. . . . . . 7 ⊢ (𝑥 = 𝑧 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑧))
4	3	eleq1d 2845	. . . . . 6 ⊢ (𝑥 = 𝑧 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ∈ 𝐴))
5		fveq2 6885	. . . . . . 7 ⊢ (𝑥 = suc 𝑧 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧))
6	5	eleq1d 2845	. . . . . 6 ⊢ (𝑥 = suc 𝑧 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) ∈ 𝐴))
7		mh-inf3f1.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ (𝐴 ∖ ran 𝐹))
8		fr0g 8444	. . . . . . . . 9 ⊢ (𝐵 ∈ (𝐴 ∖ ran 𝐹) → ((rec(𝐹, 𝐵) ↾ ω)‘∅) = 𝐵)
9	7, 8	syl 18	. . . . . . . 8 ⊢ (𝜑 → ((rec(𝐹, 𝐵) ↾ ω)‘∅) = 𝐵)
10	9, 7	eqeltrd 2860	. . . . . . 7 ⊢ (𝜑 → ((rec(𝐹, 𝐵) ↾ ω)‘∅) ∈ (𝐴 ∖ ran 𝐹))
11	10	eldifad 4051	. . . . . 6 ⊢ (𝜑 → ((rec(𝐹, 𝐵) ↾ ω)‘∅) ∈ 𝐴)
12		mh-inf3f1.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐴–1-1→𝐴)
13		f1f 6778	. . . . . . . . . 10 ⊢ (𝐹:𝐴–1-1→𝐴 → 𝐹:𝐴⟶𝐴)
14	12, 13	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:𝐴⟶𝐴)
15	14	ffvelcdmda 7084	. . . . . . . 8 ⊢ ((𝜑 ∧ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ∈ 𝐴) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ∈ 𝐴)
16		frsuc 8445	. . . . . . . . 9 ⊢ (𝑧 ∈ ω → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
17	16	eleq1d 2845	. . . . . . . 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 7910	. . . . 5 ⊢ (𝑥 ∈ ω → (𝜑 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴))
21	20	com12 33	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ω → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴))
22	21	ralrimiv 3153	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ ω ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴)
23		frfnom 8443	. . . 4 ⊢ (rec(𝐹, 𝐵) ↾ ω) Fn ω
24		ffnfv 7119	. . . 4 ⊢ ((rec(𝐹, 𝐵) ↾ ω):ω⟶𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω) Fn ω ∧ ∀𝑥 ∈ ω ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴))
25	23, 24	mpbiran 722	. . 3 ⊢ ((rec(𝐹, 𝐵) ↾ ω):ω⟶𝐴 ↔ ∀𝑥 ∈ ω ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴)
26	22, 25	sylibr 237	. 2 ⊢ (𝜑 → (rec(𝐹, 𝐵) ↾ ω):ω⟶𝐴)
27	1	neeq1d 3014	. . . . . . 7 ⊢ (𝑥 = ∅ → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘∅) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
28	27	raleqbi1dv 3329	. . . . . 6 ⊢ (𝑥 = ∅ → (∀𝑦 ∈ 𝑥 ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) ↔ ∀𝑦 ∈ ∅ ((rec(𝐹, 𝐵) ↾ ω)‘∅) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
29	3	neeq1d 3014	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
30	29	raleqbi1dv 3329	. . . . . 6 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) ↔ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
31	5	neeq1d 3014	. . . . . . 7 ⊢ (𝑥 = suc 𝑧 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
32	31	raleqbi1dv 3329	. . . . . 6 ⊢ (𝑥 = suc 𝑧 → (∀𝑦 ∈ 𝑥 ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) ↔ ∀𝑦 ∈ suc 𝑧((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
33		ral0 4453	. . . . . . 7 ⊢ ∀𝑦 ∈ ∅ ((rec(𝐹, 𝐵) ↾ ω)‘∅) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)
34	33	a1i 11	. . . . . 6 ⊢ (𝜑 → ∀𝑦 ∈ ∅ ((rec(𝐹, 𝐵) ↾ ω)‘∅) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))
35		nfv 1946	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑧 ∈ ω)
36		nfra1 3286	. . . . . . . . . 10 ⊢ Ⅎ𝑦∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)
37	35, 36	nfan 1931	. . . . . . . . 9 ⊢ Ⅎ𝑦((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))
38	16	ad3antlr 744	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
39		fveq2 6885	. . . . . . . . . . . 12 ⊢ (𝑦 = ∅ → ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) = ((rec(𝐹, 𝐵) ↾ ω)‘∅))
40	39	neeq2d 3015	. . . . . . . . . . 11 ⊢ (𝑦 = ∅ → ((𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) ↔ (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘∅)))
41		peano2b 7894	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ω ↔ suc 𝑧 ∈ ω)
42		elnn 7888	. . . . . . . . . . . . . . . 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 7895	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ω ∧ 𝑦 ≠ ∅) → ∃𝑥 ∈ ω 𝑦 = suc 𝑥)
47	45, 46	sylan 592	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) ∧ 𝑦 ≠ ∅) → ∃𝑥 ∈ ω 𝑦 = suc 𝑥)
48		fveq2 6885	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑥 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑥))
49	48	neeq2d 3015	. . . . . . . . . . . . . . 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 2861	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∈ ω ∧ 𝑦 = suc 𝑥)) → suc 𝑥 ∈ suc 𝑧)
54		nnord 7885	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ω → Ord 𝑧)
55	54	ad5antlr 748	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∈ ω ∧ 𝑦 = suc 𝑥)) → Ord 𝑧)
56		ordsucelsuc 7833	. . . . . . . . . . . . . . . . 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 3577	. . . . . . . . . . . . . 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 7084	. . . . . . . . . . . . . . . 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 7266	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:𝐴–1-1→𝐴 ∧ (((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ∈ 𝐴 ∧ ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴)) → ((𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑥)) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑥)))
67	66	necon3bid 2999	. . . . . . . . . . . . . . 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 6885	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = suc 𝑥 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) = ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑥))
71		frsuc 8445	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ω → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑥) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑥)))
72	70, 71	sylan9eqr 2817	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ ω ∧ 𝑦 = suc 𝑥) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑥)))
73	72	adantl 487	. . . . . . . . . . . . 13 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∈ ω ∧ 𝑦 = suc 𝑥)) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑥)))
74	69, 73	neeqtrrd 3029	. . . . . . . . . . . 12 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∈ ω ∧ 𝑦 = suc 𝑥)) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))
75	47, 74	rexlimddv 3169	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) ∧ 𝑦 ≠ ∅) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))
76	14	ffnd 6710	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 Fn 𝐴)
77	76	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → 𝐹 Fn 𝐴)
78	77, 62	fnfvelrnd 7082	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ∈ ran 𝐹)
79	10	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘∅) ∈ (𝐴 ∖ ran 𝐹))
80		elneeldif 4053	. . . . . . . . . . . . 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 3040	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))
84	38, 83	eqnetrd 3022	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))
85	37, 84	ralrimia 3261	. . . . . . . 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 7910	. . . . 5 ⊢ (𝑥 ∈ ω → (𝜑 → ∀𝑦 ∈ 𝑥 ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
89		rsp 3250	. . . . 5 ⊢ (∀𝑦 ∈ 𝑥 ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) → (𝑦 ∈ 𝑥 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
90	88, 89	syl6com 38	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ω → (𝑦 ∈ 𝑥 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))))
91	90	adantrd 497	. . 3 ⊢ (𝜑 → ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝑦 ∈ 𝑥 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))))
92	91	ralrimivv 3203	. 2 ⊢ (𝜑 → ∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
93		omsson 7881	. . 3 ⊢ ω ⊆ On
94		onelfvnef1 8449	. . 3 ⊢ (((rec(𝐹, 𝐵) ↾ ω):ω⟶𝐴 ∧ ω ⊆ On ∧ ∀𝑥 ∈ ω ∀𝑦 ∈ ω (𝑦 ∈ 𝑥 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))) → (rec(𝐹, 𝐵) ↾ ω):ω–1-1→𝐴)
95	93, 94	mp3an2 1478	. 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 1569   ∈ wcel 2144   ≠ wne 2955  ∀wral 3076  ∃wrex 3086   ⊆ wss 3895   ∖ cdif 4045  ∅c0 4278  ran crn 5651   ↾ cres 5652  Ord word 6361  Oncon0 6362  suc csuc 6364   Fn wfn 6533  ⟶wf 6534  –1-1→wf1 6535  ‘cfv 6538  ωcom 7877  reccrdg 8417

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-om 7878  df-2nd 8002  df-frecs 8299  df-wrecs 8330  df-recs 8379  df-rdg 8418

This theorem is used by:  mh-inf3sn  37330