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 36739

Description: A variant of inf3 9547. If 𝐹 is a one-to-one function from 𝐴 into itself, and there exists an element 𝐵 not in its range, then (rec(𝐹, 𝐵) ↾ ω) is an infinite sequence of distinct elements from 𝐴. If 𝐴 is a set, we can use this theorem to prove ω ∈ V via f1dmex 7903. (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		frfnom 8367	. . . 4 ⊢ (rec(𝐹, 𝐵) ↾ ω) Fn ω
2	1	a1i 11	. . 3 ⊢ (𝜑 → (rec(𝐹, 𝐵) ↾ ω) Fn ω)
3		fveq2 6834	. . . . . . 7 ⊢ (𝑥 = ∅ → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘∅))
4	3	eleq1d 2822	. . . . . 6 ⊢ (𝑥 = ∅ → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω)‘∅) ∈ 𝐴))
5		fveq2 6834	. . . . . . 7 ⊢ (𝑥 = 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑤))
6	5	eleq1d 2822	. . . . . 6 ⊢ (𝑥 = 𝑤 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ∈ 𝐴))
7		fveq2 6834	. . . . . . 7 ⊢ (𝑥 = suc 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤))
8	7	eleq1d 2822	. . . . . 6 ⊢ (𝑥 = suc 𝑤 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ∈ 𝐴))
9		mh-inf3f1.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ (𝐴 ∖ ran 𝐹))
10	9	eldifad 3902	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ 𝐴)
11		fr0g 8368	. . . . . . . 8 ⊢ (𝐵 ∈ 𝐴 → ((rec(𝐹, 𝐵) ↾ ω)‘∅) = 𝐵)
12	10, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((rec(𝐹, 𝐵) ↾ ω)‘∅) = 𝐵)
13	12, 10	eqeltrd 2837	. . . . . 6 ⊢ (𝜑 → ((rec(𝐹, 𝐵) ↾ ω)‘∅) ∈ 𝐴)
14		mh-inf3f1.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐴–1-1→𝐴)
15		f1f 6730	. . . . . . . . . 10 ⊢ (𝐹:𝐴–1-1→𝐴 → 𝐹:𝐴⟶𝐴)
16	14, 15	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:𝐴⟶𝐴)
17	16	ffvelcdmda 7030	. . . . . . . 8 ⊢ ((𝜑 ∧ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ∈ 𝐴) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)) ∈ 𝐴)
18		frsuc 8369	. . . . . . . . 9 ⊢ (𝑤 ∈ ω → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
19	18	eleq1d 2822	. . . . . . . 8 ⊢ (𝑤 ∈ ω → (((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ∈ 𝐴 ↔ (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)) ∈ 𝐴))
20	17, 19	imbitrrid 246	. . . . . . 7 ⊢ (𝑤 ∈ ω → ((𝜑 ∧ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ∈ 𝐴) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ∈ 𝐴))
21	20	expd 415	. . . . . 6 ⊢ (𝑤 ∈ ω → (𝜑 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ∈ 𝐴 → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ∈ 𝐴)))
22	4, 6, 8, 13, 21	finds2 7842	. . . . 5 ⊢ (𝑥 ∈ ω → (𝜑 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴))
23	22	com12 32	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ω → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴))
24	23	ralrimiv 3129	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ ω ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴)
25		ffnfv 7065	. . 3 ⊢ ((rec(𝐹, 𝐵) ↾ ω):ω⟶𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω) Fn ω ∧ ∀𝑥 ∈ ω ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴))
26	2, 24, 25	sylanbrc 584	. 2 ⊢ (𝜑 → (rec(𝐹, 𝐵) ↾ ω):ω⟶𝐴)
27		nnord 7818	. . . . . . 7 ⊢ (𝑧 ∈ ω → Ord 𝑧)
28		nnord 7818	. . . . . . 7 ⊢ (𝑤 ∈ ω → Ord 𝑤)
29		ordtri3 6353	. . . . . . 7 ⊢ ((Ord 𝑧 ∧ Ord 𝑤) → (𝑧 = 𝑤 ↔ ¬ (𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧)))
30	27, 28, 29	syl2an 597	. . . . . 6 ⊢ ((𝑧 ∈ ω ∧ 𝑤 ∈ ω) → (𝑧 = 𝑤 ↔ ¬ (𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧)))
31	30	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → (𝑧 = 𝑤 ↔ ¬ (𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧)))
32	31	necon2abid 2975	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → ((𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧) ↔ 𝑧 ≠ 𝑤))
33		vex 3434	. . . . . 6 ⊢ 𝑧 ∈ V
34		vex 3434	. . . . . 6 ⊢ 𝑤 ∈ V
35		simpl 482	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝑥 = 𝑧)
36	35	eleq1d 2822	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑥 ∈ ω ↔ 𝑧 ∈ ω))
37		simpr 484	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤)
38	37	eleq1d 2822	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑦 ∈ ω ↔ 𝑤 ∈ ω))
39	36, 38	anbi12d 633	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) ↔ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)))
40	39	anbi2d 631	. . . . . . 7 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) ↔ (𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω))))
41		elequ12 2132	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑥 ∈ 𝑦 ↔ 𝑧 ∈ 𝑤))
42	35	fveq2d 6838	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑧))
43	37	fveq2d 6838	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑤))
44	42, 43	neeq12d 2994	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
45	41, 44	imbi12d 344	. . . . . . 7 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 ∈ 𝑦 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ↔ (𝑧 ∈ 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤))))
46	40, 45	imbi12d 344	. . . . . 6 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) → (𝑥 ∈ 𝑦 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))) ↔ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → (𝑧 ∈ 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))))
47		nnaordex2 8568	. . . . . . . 8 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝑥 ∈ 𝑦 ↔ ∃𝑧 ∈ ω (𝑥 +_o suc 𝑧) = 𝑦))
48	47	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) → (𝑥 ∈ 𝑦 ↔ ∃𝑧 ∈ ω (𝑥 +_o suc 𝑧) = 𝑦))
49		oveq2 7368	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = ∅ → (suc 𝑧 +_o 𝑥) = (suc 𝑧 +_o ∅))
50	49	fveq2d 6838	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ∅ → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o ∅)))
51	3, 50	neeq12d 2994	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ∅ → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘∅) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o ∅))))
52		oveq2 7368	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → (suc 𝑧 +_o 𝑥) = (suc 𝑧 +_o 𝑤))
53	52	fveq2d 6838	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤)))
54	5, 53	neeq12d 2994	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))))
55		oveq2 7368	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = suc 𝑤 → (suc 𝑧 +_o 𝑥) = (suc 𝑧 +_o suc 𝑤))
56	55	fveq2d 6838	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = suc 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤)))
57	7, 56	neeq12d 2994	. . . . . . . . . . . . . 14 ⊢ (𝑥 = suc 𝑤 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤))))
58	16	ffnd 6663	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐹 Fn 𝐴)
59	58	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → 𝐹 Fn 𝐴)
60	26	ffvelcdmda 7030	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ∈ 𝐴)
61	59, 60	fnfvelrnd 7028	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ∈ ran 𝐹)
62	9	eldifbd 3903	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ¬ 𝐵 ∈ ran 𝐹)
63	62	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ¬ 𝐵 ∈ ran 𝐹)
64		nelne2 3031	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ∈ ran 𝐹 ∧ ¬ 𝐵 ∈ ran 𝐹) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ 𝐵)
65	61, 63, 64	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ 𝐵)
66	65	necomd 2988	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → 𝐵 ≠ (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
67	12	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘∅) = 𝐵)
68		peano2 7834	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ω → suc 𝑧 ∈ ω)
69	68	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → suc 𝑧 ∈ ω)
70		nna0 8533	. . . . . . . . . . . . . . . . . 18 ⊢ (suc 𝑧 ∈ ω → (suc 𝑧 +_o ∅) = suc 𝑧)
71	69, 70	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → (suc 𝑧 +_o ∅) = suc 𝑧)
72	71	fveq2d 6838	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o ∅)) = ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧))
73		frsuc 8369	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ω → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
74	73	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
75	72, 74	eqtrd 2772	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o ∅)) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
76	66, 67, 75	3netr4d 3010	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘∅) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o ∅)))
77	18	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
78		nnasuc 8535	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((suc 𝑧 ∈ ω ∧ 𝑤 ∈ ω) → (suc 𝑧 +_o suc 𝑤) = suc (suc 𝑧 +_o 𝑤))
79	69, 78	sylan 581	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → (suc 𝑧 +_o suc 𝑤) = suc (suc 𝑧 +_o 𝑤))
80	79	fveq2d 6838	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤)) = ((rec(𝐹, 𝐵) ↾ ω)‘suc (suc 𝑧 +_o 𝑤)))
81		nnacl 8540	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((suc 𝑧 ∈ ω ∧ 𝑤 ∈ ω) → (suc 𝑧 +_o 𝑤) ∈ ω)
82	69, 81	sylan 581	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → (suc 𝑧 +_o 𝑤) ∈ ω)
83		frsuc 8369	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((suc 𝑧 +_o 𝑤) ∈ ω → ((rec(𝐹, 𝐵) ↾ ω)‘suc (suc 𝑧 +_o 𝑤)) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))))
84	82, 83	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘suc (suc 𝑧 +_o 𝑤)) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))))
85	80, 84	eqtrd 2772	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤)) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))))
86	77, 85	eqeq12d 2753	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → (((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤)) ↔ (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤)))))
87	14	ad2antrr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → 𝐹:𝐴–1-1→𝐴)
88	26	ad2antrr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → (rec(𝐹, 𝐵) ↾ ω):ω⟶𝐴)
89		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → 𝑤 ∈ ω)
90	88, 89	ffvelcdmd 7031	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ∈ 𝐴)
91	88, 82	ffvelcdmd 7031	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤)) ∈ 𝐴)
92		f1veqaeq 7204	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:𝐴–1-1→𝐴 ∧ (((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ∈ 𝐴 ∧ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤)) ∈ 𝐴)) → ((𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))))
93	87, 90, 91, 92	syl12anc 837	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))))
94	86, 93	sylbid 240	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → (((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤)) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))))
95	94	necon3d 2954	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → (((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤)) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤))))
96	95	expcom 413	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ ω → ((𝜑 ∧ 𝑧 ∈ ω) → (((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤)) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤)))))
97	51, 54, 57, 76, 96	finds2 7842	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ω → ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥))))
98	97	impcom 407	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑥 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)))
99	98	an32s 653	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)))
100	99	adantrr 718	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)))
101	68	ad2antrl 729	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → suc 𝑧 ∈ ω)
102		simplr 769	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → 𝑥 ∈ ω)
103		nnacom 8546	. . . . . . . . . . . . 13 ⊢ ((suc 𝑧 ∈ ω ∧ 𝑥 ∈ ω) → (suc 𝑧 +_o 𝑥) = (𝑥 +_o suc 𝑧))
104	101, 102, 103	syl2anc 585	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → (suc 𝑧 +_o 𝑥) = (𝑥 +_o suc 𝑧))
105		simprr 773	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → (𝑥 +_o suc 𝑧) = 𝑦)
106	104, 105	eqtrd 2772	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → (suc 𝑧 +_o 𝑥) = 𝑦)
107	106	fveq2d 6838	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))
108	100, 107	neeqtrd 3002	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))
109	108	rexlimdvaa 3140	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (∃𝑧 ∈ ω (𝑥 +_o suc 𝑧) = 𝑦 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
110	109	adantrr 718	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) → (∃𝑧 ∈ ω (𝑥 +_o suc 𝑧) = 𝑦 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
111	48, 110	sylbid 240	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) → (𝑥 ∈ 𝑦 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
112	33, 34, 46, 111	vtocl2 3511	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → (𝑧 ∈ 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
113		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑤)
114	113	eleq1d 2822	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → (𝑥 ∈ ω ↔ 𝑤 ∈ ω))
115		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → 𝑦 = 𝑧)
116	115	eleq1d 2822	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → (𝑦 ∈ ω ↔ 𝑧 ∈ ω))
117	114, 116	anbi12d 633	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) ↔ (𝑤 ∈ ω ∧ 𝑧 ∈ ω)))
118	117	anbi2d 631	. . . . . . . . 9 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) ↔ (𝜑 ∧ (𝑤 ∈ ω ∧ 𝑧 ∈ ω))))
119		elequ12 2132	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → (𝑥 ∈ 𝑦 ↔ 𝑤 ∈ 𝑧))
120	113	fveq2d 6838	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑤))
121	115	fveq2d 6838	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑧))
122	120, 121	neeq12d 2994	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
123	119, 122	imbi12d 344	. . . . . . . . 9 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → ((𝑥 ∈ 𝑦 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ↔ (𝑤 ∈ 𝑧 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧))))
124	118, 123	imbi12d 344	. . . . . . . 8 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → (((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) → (𝑥 ∈ 𝑦 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))) ↔ ((𝜑 ∧ (𝑤 ∈ ω ∧ 𝑧 ∈ ω)) → (𝑤 ∈ 𝑧 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))))
125	34, 33, 124, 111	vtocl2 3511	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤 ∈ ω ∧ 𝑧 ∈ ω)) → (𝑤 ∈ 𝑧 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
126	125	ancom2s 651	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → (𝑤 ∈ 𝑧 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
127		necom 2986	. . . . . 6 ⊢ (((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧))
128	126, 127	imbitrrdi 252	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → (𝑤 ∈ 𝑧 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
129	112, 128	jaod 860	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → ((𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
130	32, 129	sylbird 260	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → (𝑧 ≠ 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
131	130	ralrimivva 3181	. 2 ⊢ (𝜑 → ∀𝑧 ∈ ω ∀𝑤 ∈ ω (𝑧 ≠ 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
132		dff14a 7218	. 2 ⊢ ((rec(𝐹, 𝐵) ↾ ω):ω–1-1→𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω):ω⟶𝐴 ∧ ∀𝑧 ∈ ω ∀𝑤 ∈ ω (𝑧 ≠ 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤))))
133	26, 131, 132	sylanbrc 584	1 ⊢ (𝜑 → (rec(𝐹, 𝐵) ↾ ω):ω–1-1→𝐴)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 ∖ cdif 3887 ∅c0 4274 ran crn 5625 ↾ cres 5626 Ord word 6316 suc csuc 6319 Fn wfn 6487 ⟶wf 6488 –1-1→wf1 6489 ‘cfv 6492 (class class class)co 7360 ωcom 7810 reccrdg 8341 +_o coa 8395

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5231 ax-nul 5241 ax-pr 5370 ax-un 7682

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-ov 7363 df-oprab 7364 df-mpo 7365 df-om 7811 df-2nd 7936 df-frecs 8224 df-wrecs 8255 df-recs 8304 df-rdg 8342 df-oadd 8402

This theorem is referenced by: mh-inf3sn 36740

W3C validator