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 36723

Description: A variant of inf3 9556. 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 7910. (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 8374	. . . 4 ⊢ (rec(𝐹, 𝐵) ↾ ω) Fn ω
2	1	a1i 11	. . 3 ⊢ (𝜑 → (rec(𝐹, 𝐵) ↾ ω) Fn ω)
3		fveq2 6840	. . . . . . 7 ⊢ (𝑥 = ∅ → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘∅))
4	3	eleq1d 2821	. . . . . 6 ⊢ (𝑥 = ∅ → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω)‘∅) ∈ 𝐴))
5		fveq2 6840	. . . . . . 7 ⊢ (𝑥 = 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑤))
6	5	eleq1d 2821	. . . . . 6 ⊢ (𝑥 = 𝑤 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ∈ 𝐴))
7		fveq2 6840	. . . . . . 7 ⊢ (𝑥 = suc 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤))
8	7	eleq1d 2821	. . . . . 6 ⊢ (𝑥 = suc 𝑤 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ∈ 𝐴))
9		mh-inf3f1.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ (𝐴 ∖ ran 𝐹))
10	9	eldifad 3901	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ 𝐴)
11		fr0g 8375	. . . . . . . 8 ⊢ (𝐵 ∈ 𝐴 → ((rec(𝐹, 𝐵) ↾ ω)‘∅) = 𝐵)
12	10, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((rec(𝐹, 𝐵) ↾ ω)‘∅) = 𝐵)
13	12, 10	eqeltrd 2836	. . . . . 6 ⊢ (𝜑 → ((rec(𝐹, 𝐵) ↾ ω)‘∅) ∈ 𝐴)
14		mh-inf3f1.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐴–1-1→𝐴)
15		f1f 6736	. . . . . . . . . 10 ⊢ (𝐹:𝐴–1-1→𝐴 → 𝐹:𝐴⟶𝐴)
16	14, 15	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:𝐴⟶𝐴)
17	16	ffvelcdmda 7036	. . . . . . . 8 ⊢ ((𝜑 ∧ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ∈ 𝐴) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)) ∈ 𝐴)
18		frsuc 8376	. . . . . . . . 9 ⊢ (𝑤 ∈ ω → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
19	18	eleq1d 2821	. . . . . . . 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 7849	. . . . 5 ⊢ (𝑥 ∈ ω → (𝜑 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴))
23	22	com12 32	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ω → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴))
24	23	ralrimiv 3128	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ ω ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴)
25		ffnfv 7071	. . 3 ⊢ ((rec(𝐹, 𝐵) ↾ ω):ω⟶𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω) Fn ω ∧ ∀𝑥 ∈ ω ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴))
26	2, 24, 25	sylanbrc 584	. 2 ⊢ (𝜑 → (rec(𝐹, 𝐵) ↾ ω):ω⟶𝐴)
27		nnord 7825	. . . . . . 7 ⊢ (𝑧 ∈ ω → Ord 𝑧)
28		nnord 7825	. . . . . . 7 ⊢ (𝑤 ∈ ω → Ord 𝑤)
29		ordtri3 6359	. . . . . . 7 ⊢ ((Ord 𝑧 ∧ Ord 𝑤) → (𝑧 = 𝑤 ↔ ¬ (𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧)))
30	27, 28, 29	syl2an 597	. . . . . 6 ⊢ ((𝑧 ∈ ω ∧ 𝑤 ∈ ω) → (𝑧 = 𝑤 ↔ ¬ (𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧)))
31	30	adantl 481	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → (𝑧 = 𝑤 ↔ ¬ (𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧)))
32	31	necon2abid 2974	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → ((𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧) ↔ 𝑧 ≠ 𝑤))
33		vex 3433	. . . . . 6 ⊢ 𝑧 ∈ V
34		vex 3433	. . . . . 6 ⊢ 𝑤 ∈ V
35		simpl 482	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝑥 = 𝑧)
36	35	eleq1d 2821	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑥 ∈ ω ↔ 𝑧 ∈ ω))
37		simpr 484	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤)
38	37	eleq1d 2821	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑦 ∈ ω ↔ 𝑤 ∈ ω))
39	36, 38	anbi12d 633	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) ↔ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)))
40	39	anbi2d 631	. . . . . . 7 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) ↔ (𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω))))
41		elequ12 2132	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑥 ∈ 𝑦 ↔ 𝑧 ∈ 𝑤))
42	35	fveq2d 6844	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑧))
43	37	fveq2d 6844	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑤))
44	42, 43	neeq12d 2993	. . . . . . . 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 8575	. . . . . . . 8 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝑥 ∈ 𝑦 ↔ ∃𝑧 ∈ ω (𝑥 +_o suc 𝑧) = 𝑦))
48	47	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) → (𝑥 ∈ 𝑦 ↔ ∃𝑧 ∈ ω (𝑥 +_o suc 𝑧) = 𝑦))
49		oveq2 7375	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = ∅ → (suc 𝑧 +_o 𝑥) = (suc 𝑧 +_o ∅))
50	49	fveq2d 6844	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ∅ → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o ∅)))
51	3, 50	neeq12d 2993	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ∅ → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘∅) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o ∅))))
52		oveq2 7375	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → (suc 𝑧 +_o 𝑥) = (suc 𝑧 +_o 𝑤))
53	52	fveq2d 6844	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤)))
54	5, 53	neeq12d 2993	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))))
55		oveq2 7375	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = suc 𝑤 → (suc 𝑧 +_o 𝑥) = (suc 𝑧 +_o suc 𝑤))
56	55	fveq2d 6844	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = suc 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤)))
57	7, 56	neeq12d 2993	. . . . . . . . . . . . . 14 ⊢ (𝑥 = suc 𝑤 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤))))
58	16	ffnd 6669	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐹 Fn 𝐴)
59	58	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → 𝐹 Fn 𝐴)
60	26	ffvelcdmda 7036	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ∈ 𝐴)
61	59, 60	fnfvelrnd 7034	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ∈ ran 𝐹)
62	9	eldifbd 3902	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ¬ 𝐵 ∈ ran 𝐹)
63	62	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ¬ 𝐵 ∈ ran 𝐹)
64		nelne2 3030	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ∈ ran 𝐹 ∧ ¬ 𝐵 ∈ ran 𝐹) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ 𝐵)
65	61, 63, 64	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ 𝐵)
66	65	necomd 2987	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → 𝐵 ≠ (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
67	12	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘∅) = 𝐵)
68		peano2 7841	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ω → suc 𝑧 ∈ ω)
69	68	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → suc 𝑧 ∈ ω)
70		nna0 8540	. . . . . . . . . . . . . . . . . 18 ⊢ (suc 𝑧 ∈ ω → (suc 𝑧 +_o ∅) = suc 𝑧)
71	69, 70	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → (suc 𝑧 +_o ∅) = suc 𝑧)
72	71	fveq2d 6844	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o ∅)) = ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧))
73		frsuc 8376	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ω → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
74	73	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
75	72, 74	eqtrd 2771	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o ∅)) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
76	66, 67, 75	3netr4d 3009	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘∅) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o ∅)))
77	18	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
78		nnasuc 8542	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((suc 𝑧 ∈ ω ∧ 𝑤 ∈ ω) → (suc 𝑧 +_o suc 𝑤) = suc (suc 𝑧 +_o 𝑤))
79	69, 78	sylan 581	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → (suc 𝑧 +_o suc 𝑤) = suc (suc 𝑧 +_o 𝑤))
80	79	fveq2d 6844	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤)) = ((rec(𝐹, 𝐵) ↾ ω)‘suc (suc 𝑧 +_o 𝑤)))
81		nnacl 8547	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((suc 𝑧 ∈ ω ∧ 𝑤 ∈ ω) → (suc 𝑧 +_o 𝑤) ∈ ω)
82	69, 81	sylan 581	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → (suc 𝑧 +_o 𝑤) ∈ ω)
83		frsuc 8376	. . . . . . . . . . . . . . . . . . . 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 2771	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤)) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))))
86	77, 85	eqeq12d 2752	. . . . . . . . . . . . . . . . 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 7037	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ∈ 𝐴)
91	88, 82	ffvelcdmd 7037	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤)) ∈ 𝐴)
92		f1veqaeq 7211	. . . . . . . . . . . . . . . . . 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 2953	. . . . . . . . . . . . . . 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 7849	. . . . . . . . . . . . 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 8553	. . . . . . . . . . . . 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 2771	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → (suc 𝑧 +_o 𝑥) = 𝑦)
107	106	fveq2d 6844	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))
108	100, 107	neeqtrd 3001	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))
109	108	rexlimdvaa 3139	. . . . . . . 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 3510	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → (𝑧 ∈ 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
113		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑤)
114	113	eleq1d 2821	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → (𝑥 ∈ ω ↔ 𝑤 ∈ ω))
115		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → 𝑦 = 𝑧)
116	115	eleq1d 2821	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → (𝑦 ∈ ω ↔ 𝑧 ∈ ω))
117	114, 116	anbi12d 633	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) ↔ (𝑤 ∈ ω ∧ 𝑧 ∈ ω)))
118	117	anbi2d 631	. . . . . . . . 9 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) ↔ (𝜑 ∧ (𝑤 ∈ ω ∧ 𝑧 ∈ ω))))
119		elequ12 2132	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → (𝑥 ∈ 𝑦 ↔ 𝑤 ∈ 𝑧))
120	113	fveq2d 6844	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑤))
121	115	fveq2d 6844	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑧))
122	120, 121	neeq12d 2993	. . . . . . . . . 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 3510	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤 ∈ ω ∧ 𝑧 ∈ ω)) → (𝑤 ∈ 𝑧 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
126	125	ancom2s 651	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → (𝑤 ∈ 𝑧 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
127		necom 2985	. . . . . 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 3180	. 2 ⊢ (𝜑 → ∀𝑧 ∈ ω ∀𝑤 ∈ ω (𝑧 ≠ 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
132		dff14a 7225	. 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 2932 ∀wral 3051 ∃wrex 3061 ∖ cdif 3886 ∅c0 4273 ran crn 5632 ↾ cres 5633 Ord word 6322 suc csuc 6325 Fn wfn 6493 ⟶wf 6494 –1-1→wf1 6495 ‘cfv 6498 (class class class)co 7367 ωcom 7817 reccrdg 8348 +_o coa 8402

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 2708 ax-sep 5231 ax-nul 5241 ax-pr 5375 ax-un 7689

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 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3062 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4851 df-int 4890 df-iun 4935 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-ov 7370 df-oprab 7371 df-mpo 7372 df-om 7818 df-2nd 7943 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-oadd 8409

This theorem is referenced by: mh-inf3sn 36724

W3C validator