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 36906

Description: A variant of inf3 9592. 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 7940. (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 8408	. . . 4 ⊢ (rec(𝐹, 𝐵) ↾ ω) Fn ω
2	1	a1i 11	. . 3 ⊢ (𝜑 → (rec(𝐹, 𝐵) ↾ ω) Fn ω)
3		fveq2 6869	. . . . . . 7 ⊢ (𝑥 = ∅ → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘∅))
4	3	eleq1d 2849	. . . . . 6 ⊢ (𝑥 = ∅ → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω)‘∅) ∈ 𝐴))
5		fveq2 6869	. . . . . . 7 ⊢ (𝑥 = 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑤))
6	5	eleq1d 2849	. . . . . 6 ⊢ (𝑥 = 𝑤 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ∈ 𝐴))
7		fveq2 6869	. . . . . . 7 ⊢ (𝑥 = suc 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤))
8	7	eleq1d 2849	. . . . . 6 ⊢ (𝑥 = suc 𝑤 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ∈ 𝐴))
9		mh-inf3f1.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ (𝐴 ∖ ran 𝐹))
10	9	eldifad 3918	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ 𝐴)
11		fr0g 8409	. . . . . . . 8 ⊢ (𝐵 ∈ 𝐴 → ((rec(𝐹, 𝐵) ↾ ω)‘∅) = 𝐵)
12	10, 11	syl 17	. . . . . . 7 ⊢ (𝜑 → ((rec(𝐹, 𝐵) ↾ ω)‘∅) = 𝐵)
13	12, 10	eqeltrd 2864	. . . . . 6 ⊢ (𝜑 → ((rec(𝐹, 𝐵) ↾ ω)‘∅) ∈ 𝐴)
14		mh-inf3f1.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐴–1-1→𝐴)
15		f1f 6762	. . . . . . . . . 10 ⊢ (𝐹:𝐴–1-1→𝐴 → 𝐹:𝐴⟶𝐴)
16	14, 15	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:𝐴⟶𝐴)
17	16	ffvelcdmda 7067	. . . . . . . 8 ⊢ ((𝜑 ∧ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ∈ 𝐴) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)) ∈ 𝐴)
18		frsuc 8410	. . . . . . . . 9 ⊢ (𝑤 ∈ ω → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
19	18	eleq1d 2849	. . . . . . . 8 ⊢ (𝑤 ∈ ω → (((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ∈ 𝐴 ↔ (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)) ∈ 𝐴))
20	17, 19	imbitrrid 248	. . . . . . 7 ⊢ (𝑤 ∈ ω → ((𝜑 ∧ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ∈ 𝐴) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ∈ 𝐴))
21	20	expd 419	. . . . . 6 ⊢ (𝑤 ∈ ω → (𝜑 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ∈ 𝐴 → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ∈ 𝐴)))
22	4, 6, 8, 13, 21	finds2 7881	. . . . 5 ⊢ (𝑥 ∈ ω → (𝜑 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴))
23	22	com12 32	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ω → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴))
24	23	ralrimiv 3155	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ ω ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴)
25		ffnfv 7102	. . 3 ⊢ ((rec(𝐹, 𝐵) ↾ ω):ω⟶𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω) Fn ω ∧ ∀𝑥 ∈ ω ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴))
26	2, 24, 25	sylanbrc 592	. 2 ⊢ (𝜑 → (rec(𝐹, 𝐵) ↾ ω):ω⟶𝐴)
27		nnord 7856	. . . . . . 7 ⊢ (𝑧 ∈ ω → Ord 𝑧)
28		nnord 7856	. . . . . . 7 ⊢ (𝑤 ∈ ω → Ord 𝑤)
29		ordtri3 6384	. . . . . . 7 ⊢ ((Ord 𝑧 ∧ Ord 𝑤) → (𝑧 = 𝑤 ↔ ¬ (𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧)))
30	27, 28, 29	syl2an 605	. . . . . 6 ⊢ ((𝑧 ∈ ω ∧ 𝑤 ∈ ω) → (𝑧 = 𝑤 ↔ ¬ (𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧)))
31	30	adantl 485	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → (𝑧 = 𝑤 ↔ ¬ (𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧)))
32	31	necon2abid 3001	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → ((𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧) ↔ 𝑧 ≠ 𝑤))
33		vex 3460	. . . . . 6 ⊢ 𝑧 ∈ V
34		vex 3460	. . . . . 6 ⊢ 𝑤 ∈ V
35		simpl 486	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝑥 = 𝑧)
36	35	eleq1d 2849	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑥 ∈ ω ↔ 𝑧 ∈ ω))
37		simpr 488	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤)
38	37	eleq1d 2849	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑦 ∈ ω ↔ 𝑤 ∈ ω))
39	36, 38	anbi12d 641	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) ↔ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)))
40	39	anbi2d 639	. . . . . . 7 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) ↔ (𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω))))
41		elequ12 2162	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑥 ∈ 𝑦 ↔ 𝑧 ∈ 𝑤))
42	35	fveq2d 6873	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑧))
43	37	fveq2d 6873	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑤))
44	42, 43	neeq12d 3020	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
45	41, 44	imbi12d 346	. . . . . . 7 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 ∈ 𝑦 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ↔ (𝑧 ∈ 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤))))
46	40, 45	imbi12d 346	. . . . . 6 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) → (𝑥 ∈ 𝑦 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))) ↔ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → (𝑧 ∈ 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))))
47		nnaordex2 8611	. . . . . . . 8 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝑥 ∈ 𝑦 ↔ ∃𝑧 ∈ ω (𝑥 +_o suc 𝑧) = 𝑦))
48	47	adantl 485	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) → (𝑥 ∈ 𝑦 ↔ ∃𝑧 ∈ ω (𝑥 +_o suc 𝑧) = 𝑦))
49		oveq2 7406	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = ∅ → (suc 𝑧 +_o 𝑥) = (suc 𝑧 +_o ∅))
50	49	fveq2d 6873	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ∅ → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o ∅)))
51	3, 50	neeq12d 3020	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ∅ → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘∅) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o ∅))))
52		oveq2 7406	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → (suc 𝑧 +_o 𝑥) = (suc 𝑧 +_o 𝑤))
53	52	fveq2d 6873	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤)))
54	5, 53	neeq12d 3020	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))))
55		oveq2 7406	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = suc 𝑤 → (suc 𝑧 +_o 𝑥) = (suc 𝑧 +_o suc 𝑤))
56	55	fveq2d 6873	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = suc 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤)))
57	7, 56	neeq12d 3020	. . . . . . . . . . . . . 14 ⊢ (𝑥 = suc 𝑤 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤))))
58	16	ffnd 6694	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐹 Fn 𝐴)
59	58	adantr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → 𝐹 Fn 𝐴)
60	26	ffvelcdmda 7067	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ∈ 𝐴)
61	59, 60	fnfvelrnd 7065	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ∈ ran 𝐹)
62	9	eldifbd 3919	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ¬ 𝐵 ∈ ran 𝐹)
63	62	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ¬ 𝐵 ∈ ran 𝐹)
64		nelne2 3057	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ∈ ran 𝐹 ∧ ¬ 𝐵 ∈ ran 𝐹) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ 𝐵)
65	61, 63, 64	syl2anc 593	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ 𝐵)
66	65	necomd 3014	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → 𝐵 ≠ (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
67	12	adantr 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘∅) = 𝐵)
68		peano2 7872	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ω → suc 𝑧 ∈ ω)
69	68	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → suc 𝑧 ∈ ω)
70		nna0 8576	. . . . . . . . . . . . . . . . . 18 ⊢ (suc 𝑧 ∈ ω → (suc 𝑧 +_o ∅) = suc 𝑧)
71	69, 70	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → (suc 𝑧 +_o ∅) = suc 𝑧)
72	71	fveq2d 6873	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o ∅)) = ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧))
73		frsuc 8410	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ω → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
74	73	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
75	72, 74	eqtrd 2799	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o ∅)) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
76	66, 67, 75	3netr4d 3036	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘∅) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o ∅)))
77	18	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
78		nnasuc 8578	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((suc 𝑧 ∈ ω ∧ 𝑤 ∈ ω) → (suc 𝑧 +_o suc 𝑤) = suc (suc 𝑧 +_o 𝑤))
79	69, 78	sylan 589	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → (suc 𝑧 +_o suc 𝑤) = suc (suc 𝑧 +_o 𝑤))
80	79	fveq2d 6873	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤)) = ((rec(𝐹, 𝐵) ↾ ω)‘suc (suc 𝑧 +_o 𝑤)))
81		nnacl 8583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((suc 𝑧 ∈ ω ∧ 𝑤 ∈ ω) → (suc 𝑧 +_o 𝑤) ∈ ω)
82	69, 81	sylan 589	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → (suc 𝑧 +_o 𝑤) ∈ ω)
83		frsuc 8410	. . . . . . . . . . . . . . . . . . . 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 2799	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤)) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))))
86	77, 85	eqeq12d 2780	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → (((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤)) ↔ (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤)))))
87	14	ad2antrr 736	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → 𝐹:𝐴–1-1→𝐴)
88	26	ad2antrr 736	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → (rec(𝐹, 𝐵) ↾ ω):ω⟶𝐴)
89		simpr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → 𝑤 ∈ ω)
90	88, 89	ffvelcdmd 7068	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ∈ 𝐴)
91	88, 82	ffvelcdmd 7068	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤)) ∈ 𝐴)
92		f1veqaeq 7242	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:𝐴–1-1→𝐴 ∧ (((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ∈ 𝐴 ∧ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤)) ∈ 𝐴)) → ((𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))))
93	87, 90, 91, 92	syl12anc 847	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))))
94	86, 93	sylbid 242	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → (((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤)) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))))
95	94	necon3d 2980	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → (((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤)) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤))))
96	95	expcom 417	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ ω → ((𝜑 ∧ 𝑧 ∈ ω) → (((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤)) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤)))))
97	51, 54, 57, 76, 96	finds2 7881	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ω → ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥))))
98	97	impcom 411	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑥 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)))
99	98	an32s 662	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)))
100	99	adantrr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)))
101	68	ad2antrl 738	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → suc 𝑧 ∈ ω)
102		simplr 778	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → 𝑥 ∈ ω)
103		nnacom 8589	. . . . . . . . . . . . 13 ⊢ ((suc 𝑧 ∈ ω ∧ 𝑥 ∈ ω) → (suc 𝑧 +_o 𝑥) = (𝑥 +_o suc 𝑧))
104	101, 102, 103	syl2anc 593	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → (suc 𝑧 +_o 𝑥) = (𝑥 +_o suc 𝑧))
105		simprr 782	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → (𝑥 +_o suc 𝑧) = 𝑦)
106	104, 105	eqtrd 2799	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → (suc 𝑧 +_o 𝑥) = 𝑦)
107	106	fveq2d 6873	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))
108	100, 107	neeqtrd 3028	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))
109	108	rexlimdvaa 3166	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (∃𝑧 ∈ ω (𝑥 +_o suc 𝑧) = 𝑦 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
110	109	adantrr 727	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) → (∃𝑧 ∈ ω (𝑥 +_o suc 𝑧) = 𝑦 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
111	48, 110	sylbid 242	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) → (𝑥 ∈ 𝑦 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
112	33, 34, 46, 111	vtocl2 3533	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → (𝑧 ∈ 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
113		simpl 486	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑤)
114	113	eleq1d 2849	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → (𝑥 ∈ ω ↔ 𝑤 ∈ ω))
115		simpr 488	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → 𝑦 = 𝑧)
116	115	eleq1d 2849	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → (𝑦 ∈ ω ↔ 𝑧 ∈ ω))
117	114, 116	anbi12d 641	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) ↔ (𝑤 ∈ ω ∧ 𝑧 ∈ ω)))
118	117	anbi2d 639	. . . . . . . . 9 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) ↔ (𝜑 ∧ (𝑤 ∈ ω ∧ 𝑧 ∈ ω))))
119		elequ12 2162	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → (𝑥 ∈ 𝑦 ↔ 𝑤 ∈ 𝑧))
120	113	fveq2d 6873	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑤))
121	115	fveq2d 6873	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑧))
122	120, 121	neeq12d 3020	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
123	119, 122	imbi12d 346	. . . . . . . . 9 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → ((𝑥 ∈ 𝑦 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ↔ (𝑤 ∈ 𝑧 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧))))
124	118, 123	imbi12d 346	. . . . . . . 8 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → (((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) → (𝑥 ∈ 𝑦 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))) ↔ ((𝜑 ∧ (𝑤 ∈ ω ∧ 𝑧 ∈ ω)) → (𝑤 ∈ 𝑧 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))))
125	34, 33, 124, 111	vtocl2 3533	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤 ∈ ω ∧ 𝑧 ∈ ω)) → (𝑤 ∈ 𝑧 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
126	125	ancom2s 660	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → (𝑤 ∈ 𝑧 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
127		necom 3012	. . . . . 6 ⊢ (((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧))
128	126, 127	imbitrrdi 254	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → (𝑤 ∈ 𝑧 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
129	112, 128	jaod 870	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → ((𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
130	32, 129	sylbird 262	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → (𝑧 ≠ 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
131	130	ralrimivva 3207	. 2 ⊢ (𝜑 → ∀𝑧 ∈ ω ∀𝑤 ∈ ω (𝑧 ≠ 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
132		dff14a 7256	. 2 ⊢ ((rec(𝐹, 𝐵) ↾ ω):ω–1-1→𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω):ω⟶𝐴 ∧ ∀𝑧 ∈ ω ∀𝑤 ∈ ω (𝑧 ≠ 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤))))
133	26, 131, 132	sylanbrc 592	1 ⊢ (𝜑 → (rec(𝐹, 𝐵) ↾ ω):ω–1-1→𝐴)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∨ wo 858 = wceq 1562 ∈ wcel 2144 ≠ wne 2959 ∀wral 3078 ∃wrex 3088 ∖ cdif 3903 ∅c0 4287 ran crn 5650 ↾ cres 5651 Ord word 6347 suc csuc 6350 Fn wfn 6518 ⟶wf 6519 –1-1→wf1 6520 ‘cfv 6523 (class class class)co 7398 ωcom 7848 reccrdg 8382 +_o coa 8436

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1817 ax-4 1831 ax-5 1932 ax-6 1989 ax-7 2030 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2214 ax-ext 2736 ax-sep 5248 ax-nul 5258 ax-pr 5392 ax-un 7720

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1100 df-3an 1101 df-tru 1565 df-fal 1575 df-ex 1802 df-nf 1806 df-sb 2093 df-mo 2568 df-eu 2598 df-clab 2743 df-cleq 2756 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3079 df-rex 3089 df-reu 3370 df-rab 3417 df-v 3458 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-tr 5210 df-id 5544 df-eprel 5549 df-po 5557 df-so 5558 df-fr 5602 df-we 5604 df-xp 5655 df-rel 5656 df-cnv 5657 df-co 5658 df-dm 5659 df-rn 5660 df-res 5661 df-ima 5662 df-pred 6290 df-ord 6351 df-on 6352 df-lim 6353 df-suc 6354 df-iota 6479 df-fun 6525 df-fn 6526 df-f 6527 df-f1 6528 df-fo 6529 df-f1o 6530 df-fv 6531 df-ov 7401 df-oprab 7402 df-mpo 7403 df-om 7849 df-2nd 7973 df-frecs 8264 df-wrecs 8295 df-recs 8344 df-rdg 8383 df-oadd 8443

This theorem is referenced by: mh-inf3sn 36907

W3C validator