frecabcl - Intuitionistic Logic Explorer

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

Theorem frecabcl 6457

Description: The class abstraction from df-frec 6449 exists. Unlike frecabex 6456 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 276	. . . 4 ⊢ ((𝜑 ∧ 𝑁 = ∅) → 𝐴 ∈ 𝑆)
3		peano1 4630	. . . . . . . . 9 ⊢ ∅ ∈ ω
4		elex2 2779	. . . . . . . . 9 ⊢ (∅ ∈ ω → ∃𝑎 𝑎 ∈ ω)
5		r19.9rmv 3542	. . . . . . . . 9 ⊢ (∃𝑎 𝑎 ∈ ω → (𝑥 ∈ 𝐴 ↔ ∃𝑚 ∈ ω 𝑥 ∈ 𝐴))
6	3, 4, 5	mp2b 8	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑚 ∈ ω 𝑥 ∈ 𝐴)
7		frecabcl.g	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺:𝑁⟶𝑆)
8		fdm 5413	. . . . . . . . . . . . . . 15 ⊢ (𝐺:𝑁⟶𝑆 → dom 𝐺 = 𝑁)
9	7, 8	syl 14	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom 𝐺 = 𝑁)
10	9	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑁 = ∅) → dom 𝐺 = 𝑁)
11		eqeq2 2206	. . . . . . . . . . . . . 14 ⊢ (𝑁 = ∅ → (dom 𝐺 = 𝑁 ↔ dom 𝐺 = ∅))
12	11	adantl 277	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑁 = ∅) → (dom 𝐺 = 𝑁 ↔ dom 𝐺 = ∅))
13	10, 12	mpbid 147	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑁 = ∅) → dom 𝐺 = ∅)
14	13	adantr 276	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → dom 𝐺 = ∅)
15	14	biantrurd 305	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → (𝑥 ∈ 𝐴 ↔ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))
16		peano3 4632	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ω → suc 𝑚 ≠ ∅)
17	16	adantl 277	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → suc 𝑚 ≠ ∅)
18	17, 14	neeqtrrd 2397	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → suc 𝑚 ≠ dom 𝐺)
19	18	necomd 2453	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → dom 𝐺 ≠ suc 𝑚)
20	19	neneqd 2388	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → ¬ dom 𝐺 = suc 𝑚)
21	20	intnanrd 933	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → ¬ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))))
22		biorf 745	. . . . . . . . . . 11 ⊢ (¬ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) → ((dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴) ↔ ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
23	21, 22	syl 14	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → ((dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴) ↔ ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
24	15, 23	bitrd 188	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → (𝑥 ∈ 𝐴 ↔ ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
25	24	rexbidva 2494	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑁 = ∅) → (∃𝑚 ∈ ω 𝑥 ∈ 𝐴 ↔ ∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
26	6, 25	bitrid 192	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑁 = ∅) → (𝑥 ∈ 𝐴 ↔ ∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
27		r19.44mv 3545	. . . . . . . 8 ⊢ (∃𝑎 𝑎 ∈ ω → (∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
28	3, 4, 27	mp2b 8	. . . . . . 7 ⊢ (∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))
29	26, 28	bitrdi 196	. . . . . 6 ⊢ ((𝜑 ∧ 𝑁 = ∅) → (𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
30	29	alrimiv 1888	. . . . 5 ⊢ ((𝜑 ∧ 𝑁 = ∅) → ∀𝑥(𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
31	2, 30	jca 306	. . . 4 ⊢ ((𝜑 ∧ 𝑁 = ∅) → (𝐴 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
32		eleq1 2259	. . . . . 6 ⊢ (𝑧 = 𝐴 → (𝑧 ∈ 𝑆 ↔ 𝐴 ∈ 𝑆))
33		eleq2 2260	. . . . . . . 8 ⊢ (𝑧 = 𝐴 → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ 𝐴))
34	33	bibi1d 233	. . . . . . 7 ⊢ (𝑧 = 𝐴 → ((𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))) ↔ (𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
35	34	albidv 1838	. . . . . 6 ⊢ (𝑧 = 𝐴 → (∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
36	32, 35	anbi12d 473	. . . . 5 ⊢ (𝑧 = 𝐴 → ((𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) ↔ (𝐴 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))))
37	36	spcegv 2852	. . . 4 ⊢ (𝐴 ∈ 𝑆 → ((𝐴 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))))
38	2, 31, 37	sylc 62	. . 3 ⊢ ((𝜑 ∧ 𝑁 = ∅) → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
39		fveq2 5558	. . . . . . . . 9 ⊢ (𝑦 = (𝐺‘𝑘) → (𝐹‘𝑦) = (𝐹‘(𝐺‘𝑘)))
40	39	eleq1d 2265	. . . . . . . 8 ⊢ (𝑦 = (𝐺‘𝑘) → ((𝐹‘𝑦) ∈ 𝑆 ↔ (𝐹‘(𝐺‘𝑘)) ∈ 𝑆))
41		frecabcl.fs	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑦 ∈ 𝑆 (𝐹‘𝑦) ∈ 𝑆)
42	41	ad2antrr 488	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∀𝑦 ∈ 𝑆 (𝐹‘𝑦) ∈ 𝑆)
43	7	ad2antrr 488	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝐺:𝑁⟶𝑆)
44		vex 2766	. . . . . . . . . . . 12 ⊢ 𝑘 ∈ V
45	44	sucid 4452	. . . . . . . . . . 11 ⊢ 𝑘 ∈ suc 𝑘
46		eleq2 2260	. . . . . . . . . . 11 ⊢ (𝑁 = suc 𝑘 → (𝑘 ∈ 𝑁 ↔ 𝑘 ∈ suc 𝑘))
47	45, 46	mpbiri 168	. . . . . . . . . 10 ⊢ (𝑁 = suc 𝑘 → 𝑘 ∈ 𝑁)
48	47	adantl 277	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝑘 ∈ 𝑁)
49	43, 48	ffvelcdmd 5698	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝐺‘𝑘) ∈ 𝑆)
50	40, 42, 49	rspcdva 2873	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝐹‘(𝐺‘𝑘)) ∈ 𝑆)
51		simpllr 534	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → 𝑘 ∈ ω)
52	43, 8	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → dom 𝐺 = 𝑁)
53	52	adantr 276	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → dom 𝐺 = 𝑁)
54		simplr 528	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → 𝑁 = suc 𝑘)
55	53, 54	eqtrd 2229	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → dom 𝐺 = suc 𝑘)
56		simpr 110	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑘)))
57	55, 56	jca 306	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → (dom 𝐺 = suc 𝑘 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))))
58		suceq 4437	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑘 → suc 𝑚 = suc 𝑘)
59	58	eqeq2d 2208	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑘 → (dom 𝐺 = suc 𝑚 ↔ dom 𝐺 = suc 𝑘))
60		fveq2 5558	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑘 → (𝐺‘𝑚) = (𝐺‘𝑘))
61	60	fveq2d 5562	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑘 → (𝐹‘(𝐺‘𝑚)) = (𝐹‘(𝐺‘𝑘)))
62	61	eleq2d 2266	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑘 → (𝑥 ∈ (𝐹‘(𝐺‘𝑚)) ↔ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))))
63	59, 62	anbi12d 473	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑘 → ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ↔ (dom 𝐺 = suc 𝑘 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘)))))
64	63	rspcev 2868	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ω ∧ (dom 𝐺 = suc 𝑘 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘)))) → ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))))
65	51, 57, 64	syl2anc 411	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))))
66	65	ex 115	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝑥 ∈ (𝐹‘(𝐺‘𝑘)) → ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))))
67		simpr 110	. . . . . . . . . . . . . . 15 ⊢ ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))
68	67	adantl 277	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))
69	52	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → dom 𝐺 = 𝑁)
70		simprl 529	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → dom 𝐺 = suc 𝑚)
71		simpllr 534	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑁 = suc 𝑘)
72	69, 70, 71	3eqtr3rd 2238	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → suc 𝑘 = suc 𝑚)
73		simplr 528	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝑘 ∈ ω)
74	73	ad2antrr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑘 ∈ ω)
75		simplr 528	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑚 ∈ ω)
76		peano4 4633	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ω ∧ 𝑚 ∈ ω) → (suc 𝑘 = suc 𝑚 ↔ 𝑘 = 𝑚))
77	74, 75, 76	syl2anc 411	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → (suc 𝑘 = suc 𝑚 ↔ 𝑘 = 𝑚))
78	72, 77	mpbid 147	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑘 = 𝑚)
79	78	fveq2d 5562	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → (𝐺‘𝑘) = (𝐺‘𝑚))
80	79	fveq2d 5562	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → (𝐹‘(𝐺‘𝑘)) = (𝐹‘(𝐺‘𝑚)))
81	80	eleq2d 2266	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → (𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))))
82	68, 81	mpbird 167	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑘)))
83	82	ex 115	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) → ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑘))))
84	83	rexlimdva 2614	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑘))))
85	66, 84	impbid 129	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))))
86	85	alrimiv 1888	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))))
87		peano3 4632	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ω → suc 𝑘 ≠ ∅)
88	73, 87	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → suc 𝑘 ≠ ∅)
89		neeq1 2380	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 = suc 𝑘 → (𝑁 ≠ ∅ ↔ suc 𝑘 ≠ ∅))
90	89	adantl 277	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝑁 ≠ ∅ ↔ suc 𝑘 ≠ ∅))
91	88, 90	mpbird 167	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝑁 ≠ ∅)
92	52, 91	eqnetrd 2391	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → dom 𝐺 ≠ ∅)
93	92	neneqd 2388	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ¬ dom 𝐺 = ∅)
94	93	intnanrd 933	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ¬ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))
95		biorf 745	. . . . . . . . . . . . 13 ⊢ (¬ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ↔ ((dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴) ∨ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))))))
96	94, 95	syl 14	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ↔ ((dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴) ∨ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))))))
97		orcom 729	. . . . . . . . . . . 12 ⊢ (((dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴) ∨ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))
98	96, 97	bitrdi 196	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
99	98	bibi2d 232	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ((𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) ↔ (𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
100	99	albidv 1838	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) ↔ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
101	86, 100	mpbid 147	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
102	50, 101	jca 306	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ((𝐹‘(𝐺‘𝑘)) ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
103		eleq1 2259	. . . . . . . . 9 ⊢ (𝑧 = (𝐹‘(𝐺‘𝑘)) → (𝑧 ∈ 𝑆 ↔ (𝐹‘(𝐺‘𝑘)) ∈ 𝑆))
104		eleq2 2260	. . . . . . . . . . 11 ⊢ (𝑧 = (𝐹‘(𝐺‘𝑘)) → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))))
105	104	bibi1d 233	. . . . . . . . . 10 ⊢ (𝑧 = (𝐹‘(𝐺‘𝑘)) → ((𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))) ↔ (𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
106	105	albidv 1838	. . . . . . . . 9 ⊢ (𝑧 = (𝐹‘(𝐺‘𝑘)) → (∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))) ↔ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
107	103, 106	anbi12d 473	. . . . . . . 8 ⊢ (𝑧 = (𝐹‘(𝐺‘𝑘)) → ((𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) ↔ ((𝐹‘(𝐺‘𝑘)) ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))))
108	107	spcegv 2852	. . . . . . 7 ⊢ ((𝐹‘(𝐺‘𝑘)) ∈ 𝑆 → (((𝐹‘(𝐺‘𝑘)) ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))))
109	50, 102, 108	sylc 62	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
110	109	ex 115	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ ω) → (𝑁 = suc 𝑘 → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))))
111	110	rexlimdva 2614	. . . 4 ⊢ (𝜑 → (∃𝑘 ∈ ω 𝑁 = suc 𝑘 → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))))
112	111	imp 124	. . 3 ⊢ ((𝜑 ∧ ∃𝑘 ∈ ω 𝑁 = suc 𝑘) → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
113		frecabcl.n	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ω)
114		nn0suc 4640	. . . 4 ⊢ (𝑁 ∈ ω → (𝑁 = ∅ ∨ ∃𝑘 ∈ ω 𝑁 = suc 𝑘))
115	113, 114	syl 14	. . 3 ⊢ (𝜑 → (𝑁 = ∅ ∨ ∃𝑘 ∈ ω 𝑁 = suc 𝑘))
116	38, 112, 115	mpjaodan 799	. 2 ⊢ (𝜑 → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
117		clabel 2323	. 2 ⊢ ({𝑥 ∣ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ 𝑆 ↔ ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
118	116, 117	sylibr 134	1 ⊢ (𝜑 → {𝑥 ∣ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))} ∈ 𝑆)

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 104 ↔ wb 105 ∨ wo 709 ∀wal 1362 = wceq 1364 ∃wex 1506 ∈ wcel 2167 {cab 2182 ≠ wne 2367 ∀wral 2475 ∃wrex 2476 ∅c0 3450 suc csuc 4400 ωcom 4626 dom cdm 4663 ⟶wf 5254 ‘cfv 5258

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-sep 4151 ax-nul 4159 ax-pow 4207 ax-pr 4242 ax-un 4468 ax-setind 4573 ax-iinf 4624

This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-ral 2480 df-rex 2481 df-v 2765 df-sbc 2990 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3451 df-pw 3607 df-sn 3628 df-pr 3629 df-op 3631 df-uni 3840 df-int 3875 df-br 4034 df-opab 4095 df-id 4328 df-suc 4406 df-iom 4627 df-xp 4669 df-rel 4670 df-cnv 4671 df-co 4672 df-dm 4673 df-rn 4674 df-iota 5219 df-fun 5260 df-fn 5261 df-f 5262 df-fv 5266

This theorem is referenced by: freccllem 6460 frecfcllem 6462 frecsuclem 6464

W3C validator