frecabcl - Intuitionistic Logic Explorer

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

Theorem frecabcl 6226

Description: The class abstraction from df-frec 6218 exists. Unlike frecabex 6225 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 272	. . . 4 ⊢ ((𝜑 ∧ 𝑁 = ∅) → 𝐴 ∈ 𝑆)
3		peano1 4446	. . . . . . . . 9 ⊢ ∅ ∈ ω
4		elex2 2657	. . . . . . . . 9 ⊢ (∅ ∈ ω → ∃𝑎 𝑎 ∈ ω)
5		r19.9rmv 3401	. . . . . . . . 9 ⊢ (∃𝑎 𝑎 ∈ ω → (𝑥 ∈ 𝐴 ↔ ∃𝑚 ∈ ω 𝑥 ∈ 𝐴))
6	3, 4, 5	mp2b 8	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑚 ∈ ω 𝑥 ∈ 𝐴)
7		frecabcl.g	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺:𝑁⟶𝑆)
8		fdm 5214	. . . . . . . . . . . . . . 15 ⊢ (𝐺:𝑁⟶𝑆 → dom 𝐺 = 𝑁)
9	7, 8	syl 14	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom 𝐺 = 𝑁)
10	9	adantr 272	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑁 = ∅) → dom 𝐺 = 𝑁)
11		eqeq2 2109	. . . . . . . . . . . . . 14 ⊢ (𝑁 = ∅ → (dom 𝐺 = 𝑁 ↔ dom 𝐺 = ∅))
12	11	adantl 273	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑁 = ∅) → (dom 𝐺 = 𝑁 ↔ dom 𝐺 = ∅))
13	10, 12	mpbid 146	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑁 = ∅) → dom 𝐺 = ∅)
14	13	adantr 272	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → dom 𝐺 = ∅)
15	14	biantrurd 301	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → (𝑥 ∈ 𝐴 ↔ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))
16		peano3 4448	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ω → suc 𝑚 ≠ ∅)
17	16	adantl 273	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → suc 𝑚 ≠ ∅)
18	17, 14	neeqtrrd 2297	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → suc 𝑚 ≠ dom 𝐺)
19	18	necomd 2353	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → dom 𝐺 ≠ suc 𝑚)
20	19	neneqd 2288	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → ¬ dom 𝐺 = suc 𝑚)
21	20	intnanrd 885	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → ¬ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))))
22		biorf 704	. . . . . . . . . . 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 2393	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑁 = ∅) → (∃𝑚 ∈ ω 𝑥 ∈ 𝐴 ↔ ∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
26	6, 25	syl5bb 191	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑁 = ∅) → (𝑥 ∈ 𝐴 ↔ ∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
27		r19.44mv 3404	. . . . . . . 8 ⊢ (∃𝑎 𝑎 ∈ ω → (∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
28	3, 4, 27	mp2b 8	. . . . . . 7 ⊢ (∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))
29	26, 28	syl6bb 195	. . . . . 6 ⊢ ((𝜑 ∧ 𝑁 = ∅) → (𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
30	29	alrimiv 1813	. . . . 5 ⊢ ((𝜑 ∧ 𝑁 = ∅) → ∀𝑥(𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
31	2, 30	jca 302	. . . 4 ⊢ ((𝜑 ∧ 𝑁 = ∅) → (𝐴 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
32		eleq1 2162	. . . . . 6 ⊢ (𝑧 = 𝐴 → (𝑧 ∈ 𝑆 ↔ 𝐴 ∈ 𝑆))
33		eleq2 2163	. . . . . . . 8 ⊢ (𝑧 = 𝐴 → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ 𝐴))
34	33	bibi1d 232	. . . . . . 7 ⊢ (𝑧 = 𝐴 → ((𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))) ↔ (𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
35	34	albidv 1763	. . . . . 6 ⊢ (𝑧 = 𝐴 → (∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
36	32, 35	anbi12d 460	. . . . 5 ⊢ (𝑧 = 𝐴 → ((𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) ↔ (𝐴 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))))
37	36	spcegv 2729	. . . 4 ⊢ (𝐴 ∈ 𝑆 → ((𝐴 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))))
38	2, 31, 37	sylc 62	. . 3 ⊢ ((𝜑 ∧ 𝑁 = ∅) → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
39		fveq2 5353	. . . . . . . . 9 ⊢ (𝑦 = (𝐺‘𝑘) → (𝐹‘𝑦) = (𝐹‘(𝐺‘𝑘)))
40	39	eleq1d 2168	. . . . . . . 8 ⊢ (𝑦 = (𝐺‘𝑘) → ((𝐹‘𝑦) ∈ 𝑆 ↔ (𝐹‘(𝐺‘𝑘)) ∈ 𝑆))
41		frecabcl.fs	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑦 ∈ 𝑆 (𝐹‘𝑦) ∈ 𝑆)
42	41	ad2antrr 475	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∀𝑦 ∈ 𝑆 (𝐹‘𝑦) ∈ 𝑆)
43	7	ad2antrr 475	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝐺:𝑁⟶𝑆)
44		vex 2644	. . . . . . . . . . . 12 ⊢ 𝑘 ∈ V
45	44	sucid 4277	. . . . . . . . . . 11 ⊢ 𝑘 ∈ suc 𝑘
46		eleq2 2163	. . . . . . . . . . 11 ⊢ (𝑁 = suc 𝑘 → (𝑘 ∈ 𝑁 ↔ 𝑘 ∈ suc 𝑘))
47	45, 46	mpbiri 167	. . . . . . . . . 10 ⊢ (𝑁 = suc 𝑘 → 𝑘 ∈ 𝑁)
48	47	adantl 273	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝑘 ∈ 𝑁)
49	43, 48	ffvelrnd 5488	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝐺‘𝑘) ∈ 𝑆)
50	40, 42, 49	rspcdva 2749	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝐹‘(𝐺‘𝑘)) ∈ 𝑆)
51		simpllr 504	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → 𝑘 ∈ ω)
52	43, 8	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → dom 𝐺 = 𝑁)
53	52	adantr 272	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → dom 𝐺 = 𝑁)
54		simplr 500	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → 𝑁 = suc 𝑘)
55	53, 54	eqtrd 2132	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → dom 𝐺 = suc 𝑘)
56		simpr 109	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑘)))
57	55, 56	jca 302	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → (dom 𝐺 = suc 𝑘 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))))
58		suceq 4262	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑘 → suc 𝑚 = suc 𝑘)
59	58	eqeq2d 2111	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑘 → (dom 𝐺 = suc 𝑚 ↔ dom 𝐺 = suc 𝑘))
60		fveq2 5353	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑘 → (𝐺‘𝑚) = (𝐺‘𝑘))
61	60	fveq2d 5357	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑘 → (𝐹‘(𝐺‘𝑚)) = (𝐹‘(𝐺‘𝑘)))
62	61	eleq2d 2169	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑘 → (𝑥 ∈ (𝐹‘(𝐺‘𝑚)) ↔ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))))
63	59, 62	anbi12d 460	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑘 → ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ↔ (dom 𝐺 = suc 𝑘 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘)))))
64	63	rspcev 2744	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ω ∧ (dom 𝐺 = suc 𝑘 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘)))) → ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))))
65	51, 57, 64	syl2anc 406	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))))
66	65	ex 114	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝑥 ∈ (𝐹‘(𝐺‘𝑘)) → ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))))
67		simpr 109	. . . . . . . . . . . . . . 15 ⊢ ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))
68	67	adantl 273	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))
69	52	ad2antrr 475	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → dom 𝐺 = 𝑁)
70		simprl 501	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → dom 𝐺 = suc 𝑚)
71		simpllr 504	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑁 = suc 𝑘)
72	69, 70, 71	3eqtr3rd 2141	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → suc 𝑘 = suc 𝑚)
73		simplr 500	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝑘 ∈ ω)
74	73	ad2antrr 475	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑘 ∈ ω)
75		simplr 500	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑚 ∈ ω)
76		peano4 4449	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ω ∧ 𝑚 ∈ ω) → (suc 𝑘 = suc 𝑚 ↔ 𝑘 = 𝑚))
77	74, 75, 76	syl2anc 406	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → (suc 𝑘 = suc 𝑚 ↔ 𝑘 = 𝑚))
78	72, 77	mpbid 146	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑘 = 𝑚)
79	78	fveq2d 5357	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → (𝐺‘𝑘) = (𝐺‘𝑚))
80	79	fveq2d 5357	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → (𝐹‘(𝐺‘𝑘)) = (𝐹‘(𝐺‘𝑚)))
81	80	eleq2d 2169	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → (𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))))
82	68, 81	mpbird 166	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑘)))
83	82	ex 114	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) → ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑘))))
84	83	rexlimdva 2508	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑘))))
85	66, 84	impbid 128	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))))
86	85	alrimiv 1813	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))))
87		peano3 4448	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ω → suc 𝑘 ≠ ∅)
88	73, 87	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → suc 𝑘 ≠ ∅)
89		neeq1 2280	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 = suc 𝑘 → (𝑁 ≠ ∅ ↔ suc 𝑘 ≠ ∅))
90	89	adantl 273	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝑁 ≠ ∅ ↔ suc 𝑘 ≠ ∅))
91	88, 90	mpbird 166	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝑁 ≠ ∅)
92	52, 91	eqnetrd 2291	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → dom 𝐺 ≠ ∅)
93	92	neneqd 2288	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ¬ dom 𝐺 = ∅)
94	93	intnanrd 885	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ¬ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))
95		biorf 704	. . . . . . . . . . . . 13 ⊢ (¬ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ↔ ((dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴) ∨ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))))))
96	94, 95	syl 14	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ↔ ((dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴) ∨ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))))))
97		orcom 688	. . . . . . . . . . . 12 ⊢ (((dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴) ∨ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))
98	96, 97	syl6bb 195	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
99	98	bibi2d 231	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ((𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) ↔ (𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
100	99	albidv 1763	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) ↔ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
101	86, 100	mpbid 146	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
102	50, 101	jca 302	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ((𝐹‘(𝐺‘𝑘)) ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
103		eleq1 2162	. . . . . . . . 9 ⊢ (𝑧 = (𝐹‘(𝐺‘𝑘)) → (𝑧 ∈ 𝑆 ↔ (𝐹‘(𝐺‘𝑘)) ∈ 𝑆))
104		eleq2 2163	. . . . . . . . . . 11 ⊢ (𝑧 = (𝐹‘(𝐺‘𝑘)) → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))))
105	104	bibi1d 232	. . . . . . . . . 10 ⊢ (𝑧 = (𝐹‘(𝐺‘𝑘)) → ((𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))) ↔ (𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
106	105	albidv 1763	. . . . . . . . 9 ⊢ (𝑧 = (𝐹‘(𝐺‘𝑘)) → (∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))) ↔ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
107	103, 106	anbi12d 460	. . . . . . . 8 ⊢ (𝑧 = (𝐹‘(𝐺‘𝑘)) → ((𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) ↔ ((𝐹‘(𝐺‘𝑘)) ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))))
108	107	spcegv 2729	. . . . . . 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 2508	. . . 4 ⊢ (𝜑 → (∃𝑘 ∈ ω 𝑁 = suc 𝑘 → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))))
112	111	imp 123	. . 3 ⊢ ((𝜑 ∧ ∃𝑘 ∈ ω 𝑁 = suc 𝑘) → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
113		frecabcl.n	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ω)
114		nn0suc 4456	. . . 4 ⊢ (𝑁 ∈ ω → (𝑁 = ∅ ∨ ∃𝑘 ∈ ω 𝑁 = suc 𝑘))
115	113, 114	syl 14	. . 3 ⊢ (𝜑 → (𝑁 = ∅ ∨ ∃𝑘 ∈ ω 𝑁 = suc 𝑘))
116	38, 112, 115	mpjaodan 753	. 2 ⊢ (𝜑 → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
117		clabel 2225	. 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 670 ∀wal 1297 = wceq 1299 ∃wex 1436 ∈ wcel 1448 {cab 2086 ≠ wne 2267 ∀wral 2375 ∃wrex 2376 ∅c0 3310 suc csuc 4225 ωcom 4442 dom cdm 4477 ⟶wf 5055 ‘cfv 5059

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 584 ax-in2 585 ax-io 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-13 1459 ax-14 1460 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 ax-sep 3986 ax-nul 3994 ax-pow 4038 ax-pr 4069 ax-un 4293 ax-setind 4390 ax-iinf 4440

This theorem depends on definitions: df-bi 116 df-3an 932 df-tru 1302 df-nf 1405 df-sb 1704 df-eu 1963 df-mo 1964 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-ne 2268 df-ral 2380 df-rex 2381 df-v 2643 df-sbc 2863 df-dif 3023 df-un 3025 df-in 3027 df-ss 3034 df-nul 3311 df-pw 3459 df-sn 3480 df-pr 3481 df-op 3483 df-uni 3684 df-int 3719 df-br 3876 df-opab 3930 df-id 4153 df-suc 4231 df-iom 4443 df-xp 4483 df-rel 4484 df-cnv 4485 df-co 4486 df-dm 4487 df-rn 4488 df-iota 5024 df-fun 5061 df-fn 5062 df-f 5063 df-fv 5067

This theorem is referenced by: freccllem 6229 frecfcllem 6231 frecsuclem 6233

W3C validator