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 36996

Description: A variant of inf3 9603. 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 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		frfnom 8421	. . . 4 ⊢ (rec(𝐹, 𝐵) ↾ ω) Fn ω
2	1	a1i 11	. . 3 ⊢ (𝜑 → (rec(𝐹, 𝐵) ↾ ω) Fn ω)
3		fveq2 6881	. . . . . . 7 ⊢ (𝑥 = ∅ → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘∅))
4	3	eleq1d 2846	. . . . . 6 ⊢ (𝑥 = ∅ → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω)‘∅) ∈ 𝐴))
5		fveq2 6881	. . . . . . 7 ⊢ (𝑥 = 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑤))
6	5	eleq1d 2846	. . . . . 6 ⊢ (𝑥 = 𝑤 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ∈ 𝐴))
7		fveq2 6881	. . . . . . 7 ⊢ (𝑥 = suc 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤))
8	7	eleq1d 2846	. . . . . 6 ⊢ (𝑥 = suc 𝑤 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ∈ 𝐴))
9		mh-inf3f1.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ (𝐴 ∖ ran 𝐹))
10	9	eldifad 3916	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ 𝐴)
11		fr0g 8422	. . . . . . . 8 ⊢ (𝐵 ∈ 𝐴 → ((rec(𝐹, 𝐵) ↾ ω)‘∅) = 𝐵)
12	10, 11	syl 18	. . . . . . 7 ⊢ (𝜑 → ((rec(𝐹, 𝐵) ↾ ω)‘∅) = 𝐵)
13	12, 10	eqeltrd 2861	. . . . . 6 ⊢ (𝜑 → ((rec(𝐹, 𝐵) ↾ ω)‘∅) ∈ 𝐴)
14		mh-inf3f1.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐴–1-1→𝐴)
15		f1f 6774	. . . . . . . . . 10 ⊢ (𝐹:𝐴–1-1→𝐴 → 𝐹:𝐴⟶𝐴)
16	14, 15	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:𝐴⟶𝐴)
17	16	ffvelcdmda 7079	. . . . . . . 8 ⊢ ((𝜑 ∧ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ∈ 𝐴) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)) ∈ 𝐴)
18		frsuc 8423	. . . . . . . . 9 ⊢ (𝑤 ∈ ω → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
19	18	eleq1d 2846	. . . . . . . 8 ⊢ (𝑤 ∈ ω → (((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ∈ 𝐴 ↔ (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)) ∈ 𝐴))
20	17, 19	imbitrrid 249	. . . . . . 7 ⊢ (𝑤 ∈ ω → ((𝜑 ∧ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ∈ 𝐴) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ∈ 𝐴))
21	20	expd 420	. . . . . 6 ⊢ (𝑤 ∈ ω → (𝜑 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ∈ 𝐴 → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ∈ 𝐴)))
22	4, 6, 8, 13, 21	finds2 7894	. . . . 5 ⊢ (𝑥 ∈ ω → (𝜑 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴))
23	22	com12 33	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ω → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴))
24	23	ralrimiv 3154	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ ω ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴)
25		ffnfv 7114	. . 3 ⊢ ((rec(𝐹, 𝐵) ↾ ω):ω⟶𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω) Fn ω ∧ ∀𝑥 ∈ ω ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴))
26	2, 24, 25	sylanbrc 594	. 2 ⊢ (𝜑 → (rec(𝐹, 𝐵) ↾ ω):ω⟶𝐴)
27		nnord 7869	. . . . . . 7 ⊢ (𝑧 ∈ ω → Ord 𝑧)
28		nnord 7869	. . . . . . 7 ⊢ (𝑤 ∈ ω → Ord 𝑤)
29		ordtri3 6397	. . . . . . 7 ⊢ ((Ord 𝑧 ∧ Ord 𝑤) → (𝑧 = 𝑤 ↔ ¬ (𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧)))
30	27, 28, 29	syl2an 607	. . . . . 6 ⊢ ((𝑧 ∈ ω ∧ 𝑤 ∈ ω) → (𝑧 = 𝑤 ↔ ¬ (𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧)))
31	30	adantl 486	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → (𝑧 = 𝑤 ↔ ¬ (𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧)))
32	31	necon2abid 2998	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → ((𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧) ↔ 𝑧 ≠ 𝑤))
33		vex 3457	. . . . . 6 ⊢ 𝑧 ∈ V
34		vex 3457	. . . . . 6 ⊢ 𝑤 ∈ V
35		simpl 487	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝑥 = 𝑧)
36	35	eleq1d 2846	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑥 ∈ ω ↔ 𝑧 ∈ ω))
37		simpr 489	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤)
38	37	eleq1d 2846	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑦 ∈ ω ↔ 𝑤 ∈ ω))
39	36, 38	anbi12d 643	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) ↔ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)))
40	39	anbi2d 641	. . . . . . 7 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) ↔ (𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω))))
41		elequ12 2159	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑥 ∈ 𝑦 ↔ 𝑧 ∈ 𝑤))
42	35	fveq2d 6885	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑧))
43	37	fveq2d 6885	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑤))
44	42, 43	neeq12d 3017	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
45	41, 44	imbi12d 347	. . . . . . 7 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 ∈ 𝑦 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ↔ (𝑧 ∈ 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤))))
46	40, 45	imbi12d 347	. . . . . 6 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) → (𝑥 ∈ 𝑦 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))) ↔ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → (𝑧 ∈ 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))))
47		nnaordex2 8624	. . . . . . . 8 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝑥 ∈ 𝑦 ↔ ∃𝑧 ∈ ω (𝑥 +_o suc 𝑧) = 𝑦))
48	47	adantl 486	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) → (𝑥 ∈ 𝑦 ↔ ∃𝑧 ∈ ω (𝑥 +_o suc 𝑧) = 𝑦))
49		oveq2 7418	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = ∅ → (suc 𝑧 +_o 𝑥) = (suc 𝑧 +_o ∅))
50	49	fveq2d 6885	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ∅ → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o ∅)))
51	3, 50	neeq12d 3017	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ∅ → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘∅) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o ∅))))
52		oveq2 7418	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → (suc 𝑧 +_o 𝑥) = (suc 𝑧 +_o 𝑤))
53	52	fveq2d 6885	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤)))
54	5, 53	neeq12d 3017	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))))
55		oveq2 7418	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = suc 𝑤 → (suc 𝑧 +_o 𝑥) = (suc 𝑧 +_o suc 𝑤))
56	55	fveq2d 6885	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = suc 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤)))
57	7, 56	neeq12d 3017	. . . . . . . . . . . . . 14 ⊢ (𝑥 = suc 𝑤 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤))))
58	16	ffnd 6706	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐹 Fn 𝐴)
59	58	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → 𝐹 Fn 𝐴)
60	26	ffvelcdmda 7079	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ∈ 𝐴)
61	59, 60	fnfvelrnd 7077	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ∈ ran 𝐹)
62	9	eldifbd 3917	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ¬ 𝐵 ∈ ran 𝐹)
63	62	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ¬ 𝐵 ∈ ran 𝐹)
64		nelne2 3054	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ∈ ran 𝐹 ∧ ¬ 𝐵 ∈ ran 𝐹) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ 𝐵)
65	61, 63, 64	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ 𝐵)
66	65	necomd 3011	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → 𝐵 ≠ (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
67	12	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘∅) = 𝐵)
68		peano2 7885	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ω → suc 𝑧 ∈ ω)
69	68	adantl 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → suc 𝑧 ∈ ω)
70		nna0 8589	. . . . . . . . . . . . . . . . . 18 ⊢ (suc 𝑧 ∈ ω → (suc 𝑧 +_o ∅) = suc 𝑧)
71	69, 70	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → (suc 𝑧 +_o ∅) = suc 𝑧)
72	71	fveq2d 6885	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o ∅)) = ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧))
73		frsuc 8423	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ω → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
74	73	adantl 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
75	72, 74	eqtrd 2796	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o ∅)) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
76	66, 67, 75	3netr4d 3033	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘∅) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o ∅)))
77	18	adantl 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
78		nnasuc 8591	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((suc 𝑧 ∈ ω ∧ 𝑤 ∈ ω) → (suc 𝑧 +_o suc 𝑤) = suc (suc 𝑧 +_o 𝑤))
79	69, 78	sylan 591	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → (suc 𝑧 +_o suc 𝑤) = suc (suc 𝑧 +_o 𝑤))
80	79	fveq2d 6885	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤)) = ((rec(𝐹, 𝐵) ↾ ω)‘suc (suc 𝑧 +_o 𝑤)))
81		nnacl 8596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((suc 𝑧 ∈ ω ∧ 𝑤 ∈ ω) → (suc 𝑧 +_o 𝑤) ∈ ω)
82	69, 81	sylan 591	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → (suc 𝑧 +_o 𝑤) ∈ ω)
83		frsuc 8423	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((suc 𝑧 +_o 𝑤) ∈ ω → ((rec(𝐹, 𝐵) ↾ ω)‘suc (suc 𝑧 +_o 𝑤)) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))))
84	82, 83	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘suc (suc 𝑧 +_o 𝑤)) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))))
85	80, 84	eqtrd 2796	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤)) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))))
86	77, 85	eqeq12d 2777	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → (((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤)) ↔ (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤)))))
87	14	ad2antrr 738	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → 𝐹:𝐴–1-1→𝐴)
88	26	ad2antrr 738	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → (rec(𝐹, 𝐵) ↾ ω):ω⟶𝐴)
89		simpr 489	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → 𝑤 ∈ ω)
90	88, 89	ffvelcdmd 7080	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ∈ 𝐴)
91	88, 82	ffvelcdmd 7080	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤)) ∈ 𝐴)
92		f1veqaeq 7254	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:𝐴–1-1→𝐴 ∧ (((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ∈ 𝐴 ∧ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤)) ∈ 𝐴)) → ((𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))))
93	87, 90, 91, 92	syl12anc 849	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))))
94	86, 93	sylbid 243	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → (((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤)) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))))
95	94	necon3d 2977	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → (((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤)) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤))))
96	95	expcom 418	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ ω → ((𝜑 ∧ 𝑧 ∈ ω) → (((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤)) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤)))))
97	51, 54, 57, 76, 96	finds2 7894	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ω → ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥))))
98	97	impcom 412	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑥 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)))
99	98	an32s 664	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)))
100	99	adantrr 729	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)))
101	68	ad2antrl 740	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → suc 𝑧 ∈ ω)
102		simplr 780	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → 𝑥 ∈ ω)
103		nnacom 8602	. . . . . . . . . . . . 13 ⊢ ((suc 𝑧 ∈ ω ∧ 𝑥 ∈ ω) → (suc 𝑧 +_o 𝑥) = (𝑥 +_o suc 𝑧))
104	101, 102, 103	syl2anc 595	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → (suc 𝑧 +_o 𝑥) = (𝑥 +_o suc 𝑧))
105		simprr 784	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → (𝑥 +_o suc 𝑧) = 𝑦)
106	104, 105	eqtrd 2796	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → (suc 𝑧 +_o 𝑥) = 𝑦)
107	106	fveq2d 6885	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))
108	100, 107	neeqtrd 3025	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))
109	108	rexlimdvaa 3165	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (∃𝑧 ∈ ω (𝑥 +_o suc 𝑧) = 𝑦 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
110	109	adantrr 729	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) → (∃𝑧 ∈ ω (𝑥 +_o suc 𝑧) = 𝑦 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
111	48, 110	sylbid 243	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) → (𝑥 ∈ 𝑦 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
112	33, 34, 46, 111	vtocl2 3530	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → (𝑧 ∈ 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
113		simpl 487	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑤)
114	113	eleq1d 2846	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → (𝑥 ∈ ω ↔ 𝑤 ∈ ω))
115		simpr 489	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → 𝑦 = 𝑧)
116	115	eleq1d 2846	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → (𝑦 ∈ ω ↔ 𝑧 ∈ ω))
117	114, 116	anbi12d 643	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) ↔ (𝑤 ∈ ω ∧ 𝑧 ∈ ω)))
118	117	anbi2d 641	. . . . . . . . 9 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) ↔ (𝜑 ∧ (𝑤 ∈ ω ∧ 𝑧 ∈ ω))))
119		elequ12 2159	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → (𝑥 ∈ 𝑦 ↔ 𝑤 ∈ 𝑧))
120	113	fveq2d 6885	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑤))
121	115	fveq2d 6885	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑧))
122	120, 121	neeq12d 3017	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
123	119, 122	imbi12d 347	. . . . . . . . 9 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → ((𝑥 ∈ 𝑦 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)) ↔ (𝑤 ∈ 𝑧 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧))))
124	118, 123	imbi12d 347	. . . . . . . 8 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → (((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) → (𝑥 ∈ 𝑦 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))) ↔ ((𝜑 ∧ (𝑤 ∈ ω ∧ 𝑧 ∈ ω)) → (𝑤 ∈ 𝑧 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))))
125	34, 33, 124, 111	vtocl2 3530	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤 ∈ ω ∧ 𝑧 ∈ ω)) → (𝑤 ∈ 𝑧 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
126	125	ancom2s 662	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → (𝑤 ∈ 𝑧 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
127		necom 3009	. . . . . 6 ⊢ (((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧))
128	126, 127	imbitrrdi 255	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → (𝑤 ∈ 𝑧 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
129	112, 128	jaod 872	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → ((𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
130	32, 129	sylbird 263	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → (𝑧 ≠ 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
131	130	ralrimivva 3206	. 2 ⊢ (𝜑 → ∀𝑧 ∈ ω ∀𝑤 ∈ ω (𝑧 ≠ 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
132		dff14a 7268	. 2 ⊢ ((rec(𝐹, 𝐵) ↾ ω):ω–1-1→𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω):ω⟶𝐴 ∧ ∀𝑧 ∈ ω ∀𝑤 ∈ ω (𝑧 ≠ 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤))))
133	26, 131, 132	sylanbrc 594	1 ⊢ (𝜑 → (rec(𝐹, 𝐵) ↾ ω):ω–1-1→𝐴)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 = wceq 1568 ∈ wcel 2141 ≠ wne 2956 ∀wral 3077 ∃wrex 3087 ∖ cdif 3901 ∅c0 4285 ran crn 5662 ↾ cres 5663 Ord word 6359 suc csuc 6362 Fn wfn 6531 ⟶wf 6532 –1-1→wf1 6533 ‘cfv 6536 (class class class)co 7410 ωcom 7861 reccrdg 8395 +_o coa 8449

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1823 ax-4 1837 ax-5 1938 ax-6 1995 ax-7 2036 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-sep 5256 ax-nul 5268 ax-pr 5404 ax-un 7732

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1571 df-fal 1581 df-ex 1808 df-nf 1812 df-sb 2095 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3078 df-rex 3088 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-op 4595 df-uni 4872 df-int 4912 df-iun 4957 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7862 df-2nd 7986 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-oadd 8456

This theorem is referenced by: mh-inf3sn 36997

W3C validator