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 37147

Description: A variant of inf3 9617. 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 7957. (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 8427	. . . 4 ⊢ (rec(𝐹, 𝐵) ↾ ω) Fn ω
2	1	a1i 11	. . 3 ⊢ (𝜑 → (rec(𝐹, 𝐵) ↾ ω) Fn ω)
3		fveq2 6882	. . . . . . 7 ⊢ (𝑥 = ∅ → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘∅))
4	3	eleq1d 2847	. . . . . 6 ⊢ (𝑥 = ∅ → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω)‘∅) ∈ 𝐴))
5		fveq2 6882	. . . . . . 7 ⊢ (𝑥 = 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑤))
6	5	eleq1d 2847	. . . . . 6 ⊢ (𝑥 = 𝑤 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ∈ 𝐴))
7		fveq2 6882	. . . . . . 7 ⊢ (𝑥 = suc 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤))
8	7	eleq1d 2847	. . . . . 6 ⊢ (𝑥 = suc 𝑤 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ∈ 𝐴))
9		mh-inf3f1.2	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ (𝐴 ∖ ran 𝐹))
10	9	eldifad 3914	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ 𝐴)
11		fr0g 8428	. . . . . . . 8 ⊢ (𝐵 ∈ 𝐴 → ((rec(𝐹, 𝐵) ↾ ω)‘∅) = 𝐵)
12	10, 11	syl 18	. . . . . . 7 ⊢ (𝜑 → ((rec(𝐹, 𝐵) ↾ ω)‘∅) = 𝐵)
13	12, 10	eqeltrd 2862	. . . . . 6 ⊢ (𝜑 → ((rec(𝐹, 𝐵) ↾ ω)‘∅) ∈ 𝐴)
14		mh-inf3f1.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:𝐴–1-1→𝐴)
15		f1f 6775	. . . . . . . . . 10 ⊢ (𝐹:𝐴–1-1→𝐴 → 𝐹:𝐴⟶𝐴)
16	14, 15	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:𝐴⟶𝐴)
17	16	ffvelcdmda 7080	. . . . . . . 8 ⊢ ((𝜑 ∧ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ∈ 𝐴) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)) ∈ 𝐴)
18		frsuc 8429	. . . . . . . . 9 ⊢ (𝑤 ∈ ω → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
19	18	eleq1d 2847	. . . . . . . 8 ⊢ (𝑤 ∈ ω → (((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ∈ 𝐴 ↔ (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)) ∈ 𝐴))
20	17, 19	imbitrrid 249	. . . . . . 7 ⊢ (𝑤 ∈ ω → ((𝜑 ∧ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ∈ 𝐴) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ∈ 𝐴))
21	20	expd 421	. . . . . 6 ⊢ (𝑤 ∈ ω → (𝜑 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ∈ 𝐴 → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ∈ 𝐴)))
22	4, 6, 8, 13, 21	finds2 7898	. . . . 5 ⊢ (𝑥 ∈ ω → (𝜑 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴))
23	22	com12 33	. . . 4 ⊢ (𝜑 → (𝑥 ∈ ω → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴))
24	23	ralrimiv 3155	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ ω ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴)
25		ffnfv 7115	. . 3 ⊢ ((rec(𝐹, 𝐵) ↾ ω):ω⟶𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω) Fn ω ∧ ∀𝑥 ∈ ω ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ∈ 𝐴))
26	2, 24, 25	sylanbrc 595	. 2 ⊢ (𝜑 → (rec(𝐹, 𝐵) ↾ ω):ω⟶𝐴)
27		nnord 7873	. . . . . . 7 ⊢ (𝑧 ∈ ω → Ord 𝑧)
28		nnord 7873	. . . . . . 7 ⊢ (𝑤 ∈ ω → Ord 𝑤)
29		ordtri3 6398	. . . . . . 7 ⊢ ((Ord 𝑧 ∧ Ord 𝑤) → (𝑧 = 𝑤 ↔ ¬ (𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧)))
30	27, 28, 29	syl2an 608	. . . . . 6 ⊢ ((𝑧 ∈ ω ∧ 𝑤 ∈ ω) → (𝑧 = 𝑤 ↔ ¬ (𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧)))
31	30	adantl 487	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → (𝑧 = 𝑤 ↔ ¬ (𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧)))
32	31	necon2abid 2999	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → ((𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧) ↔ 𝑧 ≠ 𝑤))
33		vex 3457	. . . . . 6 ⊢ 𝑧 ∈ V
34		vex 3457	. . . . . 6 ⊢ 𝑤 ∈ V
35		simpl 488	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝑥 = 𝑧)
36	35	eleq1d 2847	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑥 ∈ ω ↔ 𝑧 ∈ ω))
37		simpr 490	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝑦 = 𝑤)
38	37	eleq1d 2847	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑦 ∈ ω ↔ 𝑤 ∈ ω))
39	36, 38	anbi12d 644	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) ↔ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)))
40	39	anbi2d 642	. . . . . . 7 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) ↔ (𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω))))
41		elequ12 2163	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑥 ∈ 𝑦 ↔ 𝑧 ∈ 𝑤))
42	35	fveq2d 6886	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑧))
43	37	fveq2d 6886	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑤))
44	42, 43	neeq12d 3018	. . . . . . . 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 8630	. . . . . . . 8 ⊢ ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) → (𝑥 ∈ 𝑦 ↔ ∃𝑧 ∈ ω (𝑥 +_o suc 𝑧) = 𝑦))
48	47	adantl 487	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) → (𝑥 ∈ 𝑦 ↔ ∃𝑧 ∈ ω (𝑥 +_o suc 𝑧) = 𝑦))
49		oveq2 7424	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = ∅ → (suc 𝑧 +_o 𝑥) = (suc 𝑧 +_o ∅))
50	49	fveq2d 6886	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = ∅ → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o ∅)))
51	3, 50	neeq12d 3018	. . . . . . . . . . . . . 14 ⊢ (𝑥 = ∅ → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘∅) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o ∅))))
52		oveq2 7424	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑤 → (suc 𝑧 +_o 𝑥) = (suc 𝑧 +_o 𝑤))
53	52	fveq2d 6886	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤)))
54	5, 53	neeq12d 3018	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑤 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))))
55		oveq2 7424	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = suc 𝑤 → (suc 𝑧 +_o 𝑥) = (suc 𝑧 +_o suc 𝑤))
56	55	fveq2d 6886	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = suc 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤)))
57	7, 56	neeq12d 3018	. . . . . . . . . . . . . 14 ⊢ (𝑥 = suc 𝑤 → (((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤))))
58	16	ffnd 6707	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐹 Fn 𝐴)
59	58	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → 𝐹 Fn 𝐴)
60	26	ffvelcdmda 7080	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ∈ 𝐴)
61	59, 60	fnfvelrnd 7078	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ∈ ran 𝐹)
62	9	eldifbd 3915	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ¬ 𝐵 ∈ ran 𝐹)
63	62	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ¬ 𝐵 ∈ ran 𝐹)
64		nelne2 3055	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ∈ ran 𝐹 ∧ ¬ 𝐵 ∈ ran 𝐹) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ 𝐵)
65	61, 63, 64	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)) ≠ 𝐵)
66	65	necomd 3012	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → 𝐵 ≠ (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
67	12	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘∅) = 𝐵)
68		peano2 7889	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ω → suc 𝑧 ∈ ω)
69	68	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → suc 𝑧 ∈ ω)
70		nna0 8595	. . . . . . . . . . . . . . . . . 18 ⊢ (suc 𝑧 ∈ ω → (suc 𝑧 +_o ∅) = suc 𝑧)
71	69, 70	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → (suc 𝑧 +_o ∅) = suc 𝑧)
72	71	fveq2d 6886	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o ∅)) = ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧))
73		frsuc 8429	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ω → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
74	73	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑧) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
75	72, 74	eqtrd 2797	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o ∅)) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
76	66, 67, 75	3netr4d 3034	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘∅) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o ∅)))
77	18	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
78		nnasuc 8597	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((suc 𝑧 ∈ ω ∧ 𝑤 ∈ ω) → (suc 𝑧 +_o suc 𝑤) = suc (suc 𝑧 +_o 𝑤))
79	69, 78	sylan 592	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → (suc 𝑧 +_o suc 𝑤) = suc (suc 𝑧 +_o 𝑤))
80	79	fveq2d 6886	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤)) = ((rec(𝐹, 𝐵) ↾ ω)‘suc (suc 𝑧 +_o 𝑤)))
81		nnacl 8602	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((suc 𝑧 ∈ ω ∧ 𝑤 ∈ ω) → (suc 𝑧 +_o 𝑤) ∈ ω)
82	69, 81	sylan 592	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → (suc 𝑧 +_o 𝑤) ∈ ω)
83		frsuc 8429	. . . . . . . . . . . . . . . . . . . 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 2797	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤)) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))))
86	77, 85	eqeq12d 2778	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → (((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤)) ↔ (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤)))))
87	14	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → 𝐹:𝐴–1-1→𝐴)
88	26	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → (rec(𝐹, 𝐵) ↾ ω):ω⟶𝐴)
89		simpr 490	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → 𝑤 ∈ ω)
90	88, 89	ffvelcdmd 7081	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ∈ 𝐴)
91	88, 82	ffvelcdmd 7081	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤)) ∈ 𝐴)
92		f1veqaeq 7256	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:𝐴–1-1→𝐴 ∧ (((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ∈ 𝐴 ∧ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤)) ∈ 𝐴)) → ((𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘𝑤)) = (𝐹‘((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) = ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤))))
93	87, 90, 91, 92	syl12anc 850	. . . . . . . . . . . . . . . . 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 2978	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑤 ∈ ω) → (((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤)) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤))))
96	95	expcom 419	. . . . . . . . . . . . . 14 ⊢ (𝑤 ∈ ω → ((𝜑 ∧ 𝑧 ∈ ω) → (((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑤)) → ((rec(𝐹, 𝐵) ↾ ω)‘suc 𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o suc 𝑤)))))
97	51, 54, 57, 76, 96	finds2 7898	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ω → ((𝜑 ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥))))
98	97	impcom 413	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑧 ∈ ω) ∧ 𝑥 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)))
99	98	an32s 665	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ 𝑧 ∈ ω) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)))
100	99	adantrr 730	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)))
101	68	ad2antrl 741	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → suc 𝑧 ∈ ω)
102		simplr 781	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → 𝑥 ∈ ω)
103		nnacom 8608	. . . . . . . . . . . . 13 ⊢ ((suc 𝑧 ∈ ω ∧ 𝑥 ∈ ω) → (suc 𝑧 +_o 𝑥) = (𝑥 +_o suc 𝑧))
104	101, 102, 103	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → (suc 𝑧 +_o 𝑥) = (𝑥 +_o suc 𝑧))
105		simprr 785	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → (𝑥 +_o suc 𝑧) = 𝑦)
106	104, 105	eqtrd 2797	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → (suc 𝑧 +_o 𝑥) = 𝑦)
107	106	fveq2d 6886	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → ((rec(𝐹, 𝐵) ↾ ω)‘(suc 𝑧 +_o 𝑥)) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))
108	100, 107	neeqtrd 3026	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ ω) ∧ (𝑧 ∈ ω ∧ (𝑥 +_o suc 𝑧) = 𝑦)) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦))
109	108	rexlimdvaa 3166	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ ω) → (∃𝑧 ∈ ω (𝑥 +_o suc 𝑧) = 𝑦 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
110	109	adantrr 730	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) → (∃𝑧 ∈ ω (𝑥 +_o suc 𝑧) = 𝑦 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
111	48, 110	sylbid 243	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) → (𝑥 ∈ 𝑦 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑦)))
112	33, 34, 46, 111	vtocl2 3529	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → (𝑧 ∈ 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
113		simpl 488	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑤)
114	113	eleq1d 2847	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → (𝑥 ∈ ω ↔ 𝑤 ∈ ω))
115		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → 𝑦 = 𝑧)
116	115	eleq1d 2847	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → (𝑦 ∈ ω ↔ 𝑧 ∈ ω))
117	114, 116	anbi12d 644	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → ((𝑥 ∈ ω ∧ 𝑦 ∈ ω) ↔ (𝑤 ∈ ω ∧ 𝑧 ∈ ω)))
118	117	anbi2d 642	. . . . . . . . 9 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → ((𝜑 ∧ (𝑥 ∈ ω ∧ 𝑦 ∈ ω)) ↔ (𝜑 ∧ (𝑤 ∈ ω ∧ 𝑧 ∈ ω))))
119		elequ12 2163	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → (𝑥 ∈ 𝑦 ↔ 𝑤 ∈ 𝑧))
120	113	fveq2d 6886	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑥) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑤))
121	115	fveq2d 6886	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑧) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑦) = ((rec(𝐹, 𝐵) ↾ ω)‘𝑧))
122	120, 121	neeq12d 3018	. . . . . . . . . 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 3529	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤 ∈ ω ∧ 𝑧 ∈ ω)) → (𝑤 ∈ 𝑧 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
126	125	ancom2s 663	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → (𝑤 ∈ 𝑧 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧)))
127		necom 3010	. . . . . 6 ⊢ (((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ↔ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑧))
128	126, 127	imbitrrdi 255	. . . . 5 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → (𝑤 ∈ 𝑧 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
129	112, 128	jaod 873	. . . 4 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → ((𝑧 ∈ 𝑤 ∨ 𝑤 ∈ 𝑧) → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
130	32, 129	sylbird 263	. . 3 ⊢ ((𝜑 ∧ (𝑧 ∈ ω ∧ 𝑤 ∈ ω)) → (𝑧 ≠ 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
131	130	ralrimivva 3207	. 2 ⊢ (𝜑 → ∀𝑧 ∈ ω ∀𝑤 ∈ ω (𝑧 ≠ 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤)))
132		dff14a 7270	. 2 ⊢ ((rec(𝐹, 𝐵) ↾ ω):ω–1-1→𝐴 ↔ ((rec(𝐹, 𝐵) ↾ ω):ω⟶𝐴 ∧ ∀𝑧 ∈ ω ∀𝑤 ∈ ω (𝑧 ≠ 𝑤 → ((rec(𝐹, 𝐵) ↾ ω)‘𝑧) ≠ ((rec(𝐹, 𝐵) ↾ ω)‘𝑤))))
133	26, 131, 132	sylanbrc 595	1 ⊢ (𝜑 → (rec(𝐹, 𝐵) ↾ ω):ω–1-1→𝐴)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 = wceq 1570 ∈ wcel 2145 ≠ wne 2957 ∀wral 3078 ∃wrex 3088 ∖ cdif 3899 ∅c0 4282 ran crn 5660 ↾ cres 5661 Ord word 6360 suc csuc 6363 Fn wfn 6532 ⟶wf 6533 –1-1→wf1 6534 ‘cfv 6537 (class class class)co 7416 ωcom 7865 reccrdg 8401 +_o coa 8455

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 2215 ax-ext 2734 ax-sep 5255 ax-nul 5267 ax-pr 5402 ax-un 7739

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 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-ral 3079 df-rex 3089 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-ov 7419 df-oprab 7420 df-mpo 7421 df-om 7866 df-2nd 7990 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-oadd 8462

This theorem is used by: mh-inf3sn 37148

W3C validator