mh-inf3f1 - Mathbox for Matthew House

	Mathbox for Matthew House		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > mh-inf3f1		Structured version Visualization version GIF version

Theorem mh-inf3f1 37245

Description: A variant of inf3 9614. 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 7953. (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 6874	. . . . . . 7 ⊢ (𝑥 = ∅ → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘∅))
2	1	eleq1d 2845	. . . . . 6 ⊢ (𝑥 = ∅ → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω)‘∅) ∈ 𝐴))
3		fveq2 6874	. . . . . . 7 ⊢ (𝑥 = 𝑧 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑧))
4	3	eleq1d 2845	. . . . . 6 ⊢ (𝑥 = 𝑧 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ∈ 𝐴))
5		fveq2 6874	. . . . . . 7 ⊢ (𝑥 = suc 𝑧 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧))
6	5	eleq1d 2845	. . . . . 6 ⊢ (𝑥 = suc 𝑧 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) ∈ 𝐴))
7		mh-inf3f1.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ (𝐴 ∖ ran 𝐹))
8		fr0g 8423	. . . . . . . . 9 ⊢ (𝐵 ∈ (𝐴 ∖ ran 𝐹) → ((rec(𝐹, 𝐵) ↾ ω)‘∅) = 𝐵)
9	7, 8	syl 18	. . . . . . . 8 ⊢ (𝜑 → ((rec(𝐹, 𝐵) ↾ ω)‘∅) = 𝐵)
10	9, 7	eqeltrd 2860	. . . . . . 7 ⊢ (𝜑 → ((rec(𝐹, 𝐵) ↾ ω)‘∅) ∈ (𝐴 ∖ ran 𝐹))
11	10	eldifad 3911	. . . . . 6 ⊢ (𝜑 → ((rec(𝐹, 𝐵) ↾ ω)‘∅) ∈ 𝐴)
12		mh-inf3f1.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐴–1-1→𝐴)
13		f1f 6767	. . . . . . . . . 10 ⊢ (𝐹:𝐴–1-1→𝐴 → 𝐹:𝐴⟶𝐴)
14	12, 13	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:𝐴⟶𝐴)
15	14	ffvelcdmda 7073	. . . . . . . 8 ⊢ ((𝜑 ∧ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ∈ 𝐴) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ∈ 𝐴)
16		frsuc 8424	. . . . . . . . 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 7894	. . . . 5 ⊢ (𝑥 ∈ ω → (𝜑 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴))
21	20	com12 33	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ω → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴))
22	21	ralrimiv 3153	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ ω ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴)
23		frfnom 8422	. . . 4 ⊢ (rec(𝐹, 𝐵) ↾ ω) Fn ω
24		ffnfv 7108	. . . 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 4454	. . . . . . 7 ⊢ ∀𝑦 ∈ ∅ ((rec(𝐹, 𝐵) ↾ ω)‘∅) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)
34	33	a1i 11	. . . . . 6 ⊢ (𝜑 → ∀𝑦 ∈ ∅ ((rec(𝐹, 𝐵) ↾ ω)‘∅) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))
35		nfv 1947	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝜑 ∧ 𝑧 ∈ ω)
36		nfra1 3286	. . . . . . . . . 10 ⊢ Ⅎ𝑦∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)
37	35, 36	nfan 1932	. . . . . . . . 9 ⊢ Ⅎ𝑦((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))
38	16	ad3antlr 744	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
39		fveq2 6874	. . . . . . . . . . . 12 ⊢ (𝑦 = ∅ → ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) = ((rec(𝐹, 𝐵) ↾ ω)‘∅))
40	39	neeq2d 3015	. . . . . . . . . . 11 ⊢ (𝑦 = ∅ → ((𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) ↔ (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘∅)))
41		peano2b 7878	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ω ↔ suc 𝑧 ∈ ω)
42		elnn 7872	. . . . . . . . . . . . . . . 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 7879	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ ω ∧ 𝑦 ≠ ∅) → ∃𝑥 ∈ ω 𝑦 = suc 𝑥)
47	45, 46	sylan 592	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) ∧ 𝑦 ≠ ∅) → ∃𝑥 ∈ ω 𝑦 = suc 𝑥)
48		fveq2 6874	. . . . . . . . . . . . . . . 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 7869	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ω → Ord 𝑧)
55	54	ad5antlr 748	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝜑 ∧ 𝑧 ∈ ω) ∧ ∀𝑦 ∈ 𝑧 ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ∧ 𝑦 ∈ suc 𝑧) ∧ 𝑦 ≠ ∅) ∧ (𝑥 ∈ ω ∧ 𝑦 = suc 𝑥)) → Ord 𝑧)
56		ordsucelsuc 7817	. . . . . . . . . . . . . . . . 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 7073	. . . . . . . . . . . . . . . 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 7255	. . . . . . . . . . . . . . . 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 6874	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = suc 𝑥 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) = ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑥))
71		frsuc 8424	. . . . . . . . . . . . . . 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 6699	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐹 Fn 𝐴)
77	76	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → 𝐹 Fn 𝐴)
78	77, 62	fnfvelrnd 7071	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ∈ ran 𝐹)
79	10	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘∅) ∈ (𝐴 ∖ ran 𝐹))
80		elneeldif 3913	. . . . . . . . . . . . 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 7894	. . . . 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 7865	. . 3 ⊢ ω ⊆ On
94		onelfvnef1 8428	. . 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→𝐴)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 ∖ cdif 3896 ⊆ wss 3899 ∅c0 4279 ran crn 5649 ↾ cres 5650 Ord word 6351 Oncon0 6352 suc csuc 6354 Fn wfn 6523 ⟶wf 6524 –1-1→wf1 6525 ‘cfv 6528 ωcom 7861 reccrdg 8396

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 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-sep 5249 ax-nul 5260 ax-pr 5391 ax-un 7735

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 2100 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 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5543 df-eprel 5548 df-po 5556 df-so 5557 df-fr 5601 df-we 5603 df-xp 5654 df-rel 5655 df-cnv 5656 df-co 5657 df-dm 5658 df-rn 5659 df-res 5660 df-ima 5661 df-pred 6294 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6484 df-fun 6530 df-fn 6531 df-f 6532 df-f1 6533 df-fo 6534 df-f1o 6535 df-fv 6536 df-ov 7412 df-om 7862 df-2nd 7986 df-frecs 8278 df-wrecs 8309 df-recs 8358 df-rdg 8397

This theorem is used by: mh-inf3sn 37246

W3C validator