frecabcl - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > frecabcl		GIF version

Theorem frecabcl 6367

Description: The class abstraction from df-frec 6359 exists. Unlike frecabex 6366 the function 𝐹 only needs to be defined on 𝑆, not all sets. This is a lemma for other finite recursion proofs. (Contributed by Jim Kingdon, 21-Mar-2022.)

**Hypotheses**
Ref	Expression
frecabcl.n	⊢ (𝜑 → 𝑁 ∈ ω)
frecabcl.g	⊢ (𝜑 → 𝐺:𝑁⟶𝑆)
frecabcl.fs	⊢ (𝜑 → ∀𝑦 ∈ 𝑆 (𝐹‘𝑦) ∈ 𝑆)
frecabcl.as	⊢ (𝜑 → 𝐴 ∈ 𝑆)

**Assertion**
Ref	Expression
frecabcl	⊢ (𝜑 → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ 𝑆)

Distinct variable groups: 𝐴,𝑚,𝑥 𝑚,𝐹,𝑥,𝑦 𝑚,𝐺,𝑥,𝑦 𝑚,𝑁,𝑥,𝑦 𝑥,𝑆,𝑦 𝜑,𝑚,𝑥,𝑦 Allowed substitution hints: 𝐴(𝑦) 𝑆(𝑚)

Proof of Theorem frecabcl Dummy variables 𝑘 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		frecabcl.as	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑆)
2	1	adantr 274	. . . 4 ⊢ ((𝜑 ∧ 𝑁 = ∅) → 𝐴 ∈ 𝑆)
3		peano1 4571	. . . . . . . . 9 ⊢ ∅ ∈ ω
4		elex2 2742	. . . . . . . . 9 ⊢ (∅ ∈ ω → ∃𝑎 𝑎 ∈ ω)
5		r19.9rmv 3500	. . . . . . . . 9 ⊢ (∃𝑎 𝑎 ∈ ω → (𝑥 ∈ 𝐴 ↔ ∃𝑚 ∈ ω 𝑥 ∈ 𝐴))
6	3, 4, 5	mp2b 8	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑚 ∈ ω 𝑥 ∈ 𝐴)
7		frecabcl.g	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺:𝑁⟶𝑆)
8		fdm 5343	. . . . . . . . . . . . . . 15 ⊢ (𝐺:𝑁⟶𝑆 → dom 𝐺 = 𝑁)
9	7, 8	syl 14	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom 𝐺 = 𝑁)
10	9	adantr 274	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑁 = ∅) → dom 𝐺 = 𝑁)
11		eqeq2 2175	. . . . . . . . . . . . . 14 ⊢ (𝑁 = ∅ → (dom 𝐺 = 𝑁 ↔ dom 𝐺 = ∅))
12	11	adantl 275	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑁 = ∅) → (dom 𝐺 = 𝑁 ↔ dom 𝐺 = ∅))
13	10, 12	mpbid 146	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑁 = ∅) → dom 𝐺 = ∅)
14	13	adantr 274	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → dom 𝐺 = ∅)
15	14	biantrurd 303	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → (𝑥 ∈ 𝐴 ↔ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))
16		peano3 4573	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ω → suc 𝑚 ≠ ∅)
17	16	adantl 275	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → suc 𝑚 ≠ ∅)
18	17, 14	neeqtrrd 2366	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → suc 𝑚 ≠ dom 𝐺)
19	18	necomd 2422	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → dom 𝐺 ≠ suc 𝑚)
20	19	neneqd 2357	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → ¬ dom 𝐺 = suc 𝑚)
21	20	intnanrd 922	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → ¬ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))))
22		biorf 734	. . . . . . . . . . 11 ⊢ (¬ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) → ((dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴) ↔ ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
23	21, 22	syl 14	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → ((dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴) ↔ ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
24	15, 23	bitrd 187	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → (𝑥 ∈ 𝐴 ↔ ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
25	24	rexbidva 2463	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑁 = ∅) → (∃𝑚 ∈ ω 𝑥 ∈ 𝐴 ↔ ∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
26	6, 25	syl5bb 191	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑁 = ∅) → (𝑥 ∈ 𝐴 ↔ ∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
27		r19.44mv 3503	. . . . . . . 8 ⊢ (∃𝑎 𝑎 ∈ ω → (∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
28	3, 4, 27	mp2b 8	. . . . . . 7 ⊢ (∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))
29	26, 28	bitrdi 195	. . . . . 6 ⊢ ((𝜑 ∧ 𝑁 = ∅) → (𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
30	29	alrimiv 1862	. . . . 5 ⊢ ((𝜑 ∧ 𝑁 = ∅) → ∀𝑥(𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
31	2, 30	jca 304	. . . 4 ⊢ ((𝜑 ∧ 𝑁 = ∅) → (𝐴 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
32		eleq1 2229	. . . . . 6 ⊢ (𝑧 = 𝐴 → (𝑧 ∈ 𝑆 ↔ 𝐴 ∈ 𝑆))
33		eleq2 2230	. . . . . . . 8 ⊢ (𝑧 = 𝐴 → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ 𝐴))
34	33	bibi1d 232	. . . . . . 7 ⊢ (𝑧 = 𝐴 → ((𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))) ↔ (𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
35	34	albidv 1812	. . . . . 6 ⊢ (𝑧 = 𝐴 → (∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
36	32, 35	anbi12d 465	. . . . 5 ⊢ (𝑧 = 𝐴 → ((𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) ↔ (𝐴 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))))
37	36	spcegv 2814	. . . 4 ⊢ (𝐴 ∈ 𝑆 → ((𝐴 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))))
38	2, 31, 37	sylc 62	. . 3 ⊢ ((𝜑 ∧ 𝑁 = ∅) → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
39		fveq2 5486	. . . . . . . . 9 ⊢ (𝑦 = (𝐺‘𝑘) → (𝐹‘𝑦) = (𝐹‘(𝐺‘𝑘)))
40	39	eleq1d 2235	. . . . . . . 8 ⊢ (𝑦 = (𝐺‘𝑘) → ((𝐹‘𝑦) ∈ 𝑆 ↔ (𝐹‘(𝐺‘𝑘)) ∈ 𝑆))
41		frecabcl.fs	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑦 ∈ 𝑆 (𝐹‘𝑦) ∈ 𝑆)
42	41	ad2antrr 480	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∀𝑦 ∈ 𝑆 (𝐹‘𝑦) ∈ 𝑆)
43	7	ad2antrr 480	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝐺:𝑁⟶𝑆)
44		vex 2729	. . . . . . . . . . . 12 ⊢ 𝑘 ∈ V
45	44	sucid 4395	. . . . . . . . . . 11 ⊢ 𝑘 ∈ suc 𝑘
46		eleq2 2230	. . . . . . . . . . 11 ⊢ (𝑁 = suc 𝑘 → (𝑘 ∈ 𝑁 ↔ 𝑘 ∈ suc 𝑘))
47	45, 46	mpbiri 167	. . . . . . . . . 10 ⊢ (𝑁 = suc 𝑘 → 𝑘 ∈ 𝑁)
48	47	adantl 275	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝑘 ∈ 𝑁)
49	43, 48	ffvelrnd 5621	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝐺‘𝑘) ∈ 𝑆)
50	40, 42, 49	rspcdva 2835	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝐹‘(𝐺‘𝑘)) ∈ 𝑆)
51		simpllr 524	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → 𝑘 ∈ ω)
52	43, 8	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → dom 𝐺 = 𝑁)
53	52	adantr 274	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → dom 𝐺 = 𝑁)
54		simplr 520	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → 𝑁 = suc 𝑘)
55	53, 54	eqtrd 2198	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → dom 𝐺 = suc 𝑘)
56		simpr 109	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑘)))
57	55, 56	jca 304	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → (dom 𝐺 = suc 𝑘 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))))
58		suceq 4380	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑘 → suc 𝑚 = suc 𝑘)
59	58	eqeq2d 2177	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑘 → (dom 𝐺 = suc 𝑚 ↔ dom 𝐺 = suc 𝑘))
60		fveq2 5486	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑘 → (𝐺‘𝑚) = (𝐺‘𝑘))
61	60	fveq2d 5490	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑘 → (𝐹‘(𝐺‘𝑚)) = (𝐹‘(𝐺‘𝑘)))
62	61	eleq2d 2236	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑘 → (𝑥 ∈ (𝐹‘(𝐺‘𝑚)) ↔ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))))
63	59, 62	anbi12d 465	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑘 → ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ↔ (dom 𝐺 = suc 𝑘 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘)))))
64	63	rspcev 2830	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ω ∧ (dom 𝐺 = suc 𝑘 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘)))) → ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))))
65	51, 57, 64	syl2anc 409	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))))
66	65	ex 114	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝑥 ∈ (𝐹‘(𝐺‘𝑘)) → ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))))
67		simpr 109	. . . . . . . . . . . . . . 15 ⊢ ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))
68	67	adantl 275	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))
69	52	ad2antrr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → dom 𝐺 = 𝑁)
70		simprl 521	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → dom 𝐺 = suc 𝑚)
71		simpllr 524	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑁 = suc 𝑘)
72	69, 70, 71	3eqtr3rd 2207	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → suc 𝑘 = suc 𝑚)
73		simplr 520	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝑘 ∈ ω)
74	73	ad2antrr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑘 ∈ ω)
75		simplr 520	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑚 ∈ ω)
76		peano4 4574	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ω ∧ 𝑚 ∈ ω) → (suc 𝑘 = suc 𝑚 ↔ 𝑘 = 𝑚))
77	74, 75, 76	syl2anc 409	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → (suc 𝑘 = suc 𝑚 ↔ 𝑘 = 𝑚))
78	72, 77	mpbid 146	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑘 = 𝑚)
79	78	fveq2d 5490	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → (𝐺‘𝑘) = (𝐺‘𝑚))
80	79	fveq2d 5490	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → (𝐹‘(𝐺‘𝑘)) = (𝐹‘(𝐺‘𝑚)))
81	80	eleq2d 2236	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → (𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))))
82	68, 81	mpbird 166	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑘)))
83	82	ex 114	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) → ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑘))))
84	83	rexlimdva 2583	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑘))))
85	66, 84	impbid 128	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))))
86	85	alrimiv 1862	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))))
87		peano3 4573	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ω → suc 𝑘 ≠ ∅)
88	73, 87	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → suc 𝑘 ≠ ∅)
89		neeq1 2349	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 = suc 𝑘 → (𝑁 ≠ ∅ ↔ suc 𝑘 ≠ ∅))
90	89	adantl 275	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝑁 ≠ ∅ ↔ suc 𝑘 ≠ ∅))
91	88, 90	mpbird 166	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝑁 ≠ ∅)
92	52, 91	eqnetrd 2360	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → dom 𝐺 ≠ ∅)
93	92	neneqd 2357	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ¬ dom 𝐺 = ∅)
94	93	intnanrd 922	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ¬ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))
95		biorf 734	. . . . . . . . . . . . 13 ⊢ (¬ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ↔ ((dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴) ∨ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))))))
96	94, 95	syl 14	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ↔ ((dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴) ∨ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))))))
97		orcom 718	. . . . . . . . . . . 12 ⊢ (((dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴) ∨ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))
98	96, 97	bitrdi 195	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
99	98	bibi2d 231	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ((𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) ↔ (𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
100	99	albidv 1812	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) ↔ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
101	86, 100	mpbid 146	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
102	50, 101	jca 304	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ((𝐹‘(𝐺‘𝑘)) ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
103		eleq1 2229	. . . . . . . . 9 ⊢ (𝑧 = (𝐹‘(𝐺‘𝑘)) → (𝑧 ∈ 𝑆 ↔ (𝐹‘(𝐺‘𝑘)) ∈ 𝑆))
104		eleq2 2230	. . . . . . . . . . 11 ⊢ (𝑧 = (𝐹‘(𝐺‘𝑘)) → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))))
105	104	bibi1d 232	. . . . . . . . . 10 ⊢ (𝑧 = (𝐹‘(𝐺‘𝑘)) → ((𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))) ↔ (𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
106	105	albidv 1812	. . . . . . . . 9 ⊢ (𝑧 = (𝐹‘(𝐺‘𝑘)) → (∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))) ↔ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
107	103, 106	anbi12d 465	. . . . . . . 8 ⊢ (𝑧 = (𝐹‘(𝐺‘𝑘)) → ((𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) ↔ ((𝐹‘(𝐺‘𝑘)) ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))))
108	107	spcegv 2814	. . . . . . 7 ⊢ ((𝐹‘(𝐺‘𝑘)) ∈ 𝑆 → (((𝐹‘(𝐺‘𝑘)) ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))))
109	50, 102, 108	sylc 62	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
110	109	ex 114	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ω) → (𝑁 = suc 𝑘 → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))))
111	110	rexlimdva 2583	. . . 4 ⊢ (𝜑 → (∃𝑘 ∈ ω 𝑁 = suc 𝑘 → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))))
112	111	imp 123	. . 3 ⊢ ((𝜑 ∧ ∃𝑘 ∈ ω 𝑁 = suc 𝑘) → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
113		frecabcl.n	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ω)
114		nn0suc 4581	. . . 4 ⊢ (𝑁 ∈ ω → (𝑁 = ∅ ∨ ∃𝑘 ∈ ω 𝑁 = suc 𝑘))
115	113, 114	syl 14	. . 3 ⊢ (𝜑 → (𝑁 = ∅ ∨ ∃𝑘 ∈ ω 𝑁 = suc 𝑘))
116	38, 112, 115	mpjaodan 788	. 2 ⊢ (𝜑 → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
117		clabel 2293	. 2 ⊢ ({𝑥 ∣ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ 𝑆 ↔ ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
118	116, 117	sylibr 133	1 ⊢ (𝜑 → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ 𝑆)

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ↔ wb 104 ∨ wo 698 ∀wal 1341 = wceq 1343 ∃wex 1480 ∈ wcel 2136 {cab 2151 ≠ wne 2336 ∀wral 2444 ∃wrex 2445 ∅c0 3409 suc csuc 4343 ωcom 4567 dom cdm 4604 ⟶wf 5184 ‘cfv 5188

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-13 2138 ax-14 2139 ax-ext 2147 ax-sep 4100 ax-nul 4108 ax-pow 4153 ax-pr 4187 ax-un 4411 ax-setind 4514 ax-iinf 4565

This theorem depends on definitions: df-bi 116 df-3an 970 df-tru 1346 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ne 2337 df-ral 2449 df-rex 2450 df-v 2728 df-sbc 2952 df-dif 3118 df-un 3120 df-in 3122 df-ss 3129 df-nul 3410 df-pw 3561 df-sn 3582 df-pr 3583 df-op 3585 df-uni 3790 df-int 3825 df-br 3983 df-opab 4044 df-id 4271 df-suc 4349 df-iom 4568 df-xp 4610 df-rel 4611 df-cnv 4612 df-co 4613 df-dm 4614 df-rn 4615 df-iota 5153 df-fun 5190 df-fn 5191 df-f 5192 df-fv 5196

This theorem is referenced by: freccllem 6370 frecfcllem 6372 frecsuclem 6374

W3C validator