frecabcl - Intuitionistic Logic Explorer

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

Theorem frecabcl 6296

Description: The class abstraction from df-frec 6288 exists. Unlike frecabex 6295 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 4508	. . . . . . . . 9 ⊢ ∅ ∈ ω
4		elex2 2702	. . . . . . . . 9 ⊢ (∅ ∈ ω → ∃𝑎 𝑎 ∈ ω)
5		r19.9rmv 3454	. . . . . . . . 9 ⊢ (∃𝑎 𝑎 ∈ ω → (𝑥 ∈ 𝐴 ↔ ∃𝑚 ∈ ω 𝑥 ∈ 𝐴))
6	3, 4, 5	mp2b 8	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑚 ∈ ω 𝑥 ∈ 𝐴)
7		frecabcl.g	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐺:𝑁⟶𝑆)
8		fdm 5278	. . . . . . . . . . . . . . 15 ⊢ (𝐺:𝑁⟶𝑆 → dom 𝐺 = 𝑁)
9	7, 8	syl 14	. . . . . . . . . . . . . 14 ⊢ (𝜑 → dom 𝐺 = 𝑁)
10	9	adantr 274	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑁 = ∅) → dom 𝐺 = 𝑁)
11		eqeq2 2149	. . . . . . . . . . . . . 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 4510	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ω → suc 𝑚 ≠ ∅)
17	16	adantl 275	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → suc 𝑚 ≠ ∅)
18	17, 14	neeqtrrd 2338	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → suc 𝑚 ≠ dom 𝐺)
19	18	necomd 2394	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → dom 𝐺 ≠ suc 𝑚)
20	19	neneqd 2329	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → ¬ dom 𝐺 = suc 𝑚)
21	20	intnanrd 917	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 = ∅) ∧ 𝑚 ∈ ω) → ¬ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))))
22		biorf 733	. . . . . . . . . . 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 2434	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑁 = ∅) → (∃𝑚 ∈ ω 𝑥 ∈ 𝐴 ↔ ∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
26	6, 25	syl5bb 191	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑁 = ∅) → (𝑥 ∈ 𝐴 ↔ ∃𝑚 ∈ ω ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
27		r19.44mv 3457	. . . . . . . 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 1846	. . . . 5 ⊢ ((𝜑 ∧ 𝑁 = ∅) → ∀𝑥(𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))
31	2, 30	jca 304	. . . 4 ⊢ ((𝜑 ∧ 𝑁 = ∅) → (𝐴 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
32		eleq1 2202	. . . . . 6 ⊢ (𝑧 = 𝐴 → (𝑧 ∈ 𝑆 ↔ 𝐴 ∈ 𝑆))
33		eleq2 2203	. . . . . . . 8 ⊢ (𝑧 = 𝐴 → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ 𝐴))
34	33	bibi1d 232	. . . . . . 7 ⊢ (𝑧 = 𝐴 → ((𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))) ↔ (𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
35	34	albidv 1796	. . . . . 6 ⊢ (𝑧 = 𝐴 → (∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
36	32, 35	anbi12d 464	. . . . 5 ⊢ (𝑧 = 𝐴 → ((𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) ↔ (𝐴 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))))
37	36	spcegv 2774	. . . 4 ⊢ (𝐴 ∈ 𝑆 → ((𝐴 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝐴 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))))
38	2, 31, 37	sylc 62	. . 3 ⊢ ((𝜑 ∧ 𝑁 = ∅) → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
39		fveq2 5421	. . . . . . . . 9 ⊢ (𝑦 = (𝐺‘𝑘) → (𝐹‘𝑦) = (𝐹‘(𝐺‘𝑘)))
40	39	eleq1d 2208	. . . . . . . 8 ⊢ (𝑦 = (𝐺‘𝑘) → ((𝐹‘𝑦) ∈ 𝑆 ↔ (𝐹‘(𝐺‘𝑘)) ∈ 𝑆))
41		frecabcl.fs	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑦 ∈ 𝑆 (𝐹‘𝑦) ∈ 𝑆)
42	41	ad2antrr 479	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∀𝑦 ∈ 𝑆 (𝐹‘𝑦) ∈ 𝑆)
43	7	ad2antrr 479	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝐺:𝑁⟶𝑆)
44		vex 2689	. . . . . . . . . . . 12 ⊢ 𝑘 ∈ V
45	44	sucid 4339	. . . . . . . . . . 11 ⊢ 𝑘 ∈ suc 𝑘
46		eleq2 2203	. . . . . . . . . . 11 ⊢ (𝑁 = suc 𝑘 → (𝑘 ∈ 𝑁 ↔ 𝑘 ∈ suc 𝑘))
47	45, 46	mpbiri 167	. . . . . . . . . 10 ⊢ (𝑁 = suc 𝑘 → 𝑘 ∈ 𝑁)
48	47	adantl 275	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝑘 ∈ 𝑁)
49	43, 48	ffvelrnd 5556	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝐺‘𝑘) ∈ 𝑆)
50	40, 42, 49	rspcdva 2794	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝐹‘(𝐺‘𝑘)) ∈ 𝑆)
51		simpllr 523	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → 𝑘 ∈ ω)
52	43, 8	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → dom 𝐺 = 𝑁)
53	52	adantr 274	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → dom 𝐺 = 𝑁)
54		simplr 519	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → 𝑁 = suc 𝑘)
55	53, 54	eqtrd 2172	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → dom 𝐺 = suc 𝑘)
56		simpr 109	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑘)))
57	55, 56	jca 304	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))) → (dom 𝐺 = suc 𝑘 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))))
58		suceq 4324	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑘 → suc 𝑚 = suc 𝑘)
59	58	eqeq2d 2151	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑘 → (dom 𝐺 = suc 𝑚 ↔ dom 𝐺 = suc 𝑘))
60		fveq2 5421	. . . . . . . . . . . . . . . . 17 ⊢ (𝑚 = 𝑘 → (𝐺‘𝑚) = (𝐺‘𝑘))
61	60	fveq2d 5425	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = 𝑘 → (𝐹‘(𝐺‘𝑚)) = (𝐹‘(𝐺‘𝑘)))
62	61	eleq2d 2209	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = 𝑘 → (𝑥 ∈ (𝐹‘(𝐺‘𝑚)) ↔ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))))
63	59, 62	anbi12d 464	. . . . . . . . . . . . . 14 ⊢ (𝑚 = 𝑘 → ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ↔ (dom 𝐺 = suc 𝑘 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘)))))
64	63	rspcev 2789	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ω ∧ (dom 𝐺 = suc 𝑘 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑘)))) → ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))))
65	51, 57, 64	syl2anc 408	. . . . . . . . . . . 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 479	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → dom 𝐺 = 𝑁)
70		simprl 520	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → dom 𝐺 = suc 𝑚)
71		simpllr 523	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑁 = suc 𝑘)
72	69, 70, 71	3eqtr3rd 2181	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → suc 𝑘 = suc 𝑚)
73		simplr 519	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝑘 ∈ ω)
74	73	ad2antrr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑘 ∈ ω)
75		simplr 519	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑚 ∈ ω)
76		peano4 4511	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑘 ∈ ω ∧ 𝑚 ∈ ω) → (suc 𝑘 = suc 𝑚 ↔ 𝑘 = 𝑚))
77	74, 75, 76	syl2anc 408	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → (suc 𝑘 = suc 𝑚 ↔ 𝑘 = 𝑚))
78	72, 77	mpbid 146	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑘 = 𝑚)
79	78	fveq2d 5425	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → (𝐺‘𝑘) = (𝐺‘𝑚))
80	79	fveq2d 5425	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → (𝐹‘(𝐺‘𝑘)) = (𝐹‘(𝐺‘𝑚)))
81	80	eleq2d 2209	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → (𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))))
82	68, 81	mpbird 166	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) ∧ (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑘)))
83	82	ex 114	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) ∧ 𝑚 ∈ ω) → ((dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑘))))
84	83	rexlimdva 2549	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) → 𝑥 ∈ (𝐹‘(𝐺‘𝑘))))
85	66, 84	impbid 128	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))))
86	85	alrimiv 1846	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚)))))
87		peano3 4510	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ω → suc 𝑘 ≠ ∅)
88	73, 87	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → suc 𝑘 ≠ ∅)
89		neeq1 2321	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑁 = suc 𝑘 → (𝑁 ≠ ∅ ↔ suc 𝑘 ≠ ∅))
90	89	adantl 275	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (𝑁 ≠ ∅ ↔ suc 𝑘 ≠ ∅))
91	88, 90	mpbird 166	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → 𝑁 ≠ ∅)
92	52, 91	eqnetrd 2332	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → dom 𝐺 ≠ ∅)
93	92	neneqd 2329	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ¬ dom 𝐺 = ∅)
94	93	intnanrd 917	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → ¬ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))
95		biorf 733	. . . . . . . . . . . . 13 ⊢ (¬ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ↔ ((dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴) ∨ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))))))
96	94, 95	syl 14	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ ω) ∧ 𝑁 = suc 𝑘) → (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ↔ ((dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴) ∨ ∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))))))
97		orcom 717	. . . . . . . . . . . 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 1796	. . . . . . . . 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 2202	. . . . . . . . 9 ⊢ (𝑧 = (𝐹‘(𝐺‘𝑘)) → (𝑧 ∈ 𝑆 ↔ (𝐹‘(𝐺‘𝑘)) ∈ 𝑆))
104		eleq2 2203	. . . . . . . . . . 11 ⊢ (𝑧 = (𝐹‘(𝐺‘𝑘)) → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ (𝐹‘(𝐺‘𝑘))))
105	104	bibi1d 232	. . . . . . . . . 10 ⊢ (𝑧 = (𝐹‘(𝐺‘𝑘)) → ((𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))) ↔ (𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
106	105	albidv 1796	. . . . . . . . 9 ⊢ (𝑧 = (𝐹‘(𝐺‘𝑘)) → (∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))) ↔ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
107	103, 106	anbi12d 464	. . . . . . . 8 ⊢ (𝑧 = (𝐹‘(𝐺‘𝑘)) → ((𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))) ↔ ((𝐹‘(𝐺‘𝑘)) ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))))
108	107	spcegv 2774	. . . . . . 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 2549	. . . 4 ⊢ (𝜑 → (∃𝑘 ∈ ω 𝑁 = suc 𝑘 → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴))))))
112	111	imp 123	. . 3 ⊢ ((𝜑 ∧ ∃𝑘 ∈ ω 𝑁 = suc 𝑘) → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
113		frecabcl.n	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ω)
114		nn0suc 4518	. . . 4 ⊢ (𝑁 ∈ ω → (𝑁 = ∅ ∨ ∃𝑘 ∈ ω 𝑁 = suc 𝑘))
115	113, 114	syl 14	. . 3 ⊢ (𝜑 → (𝑁 = ∅ ∨ ∃𝑘 ∈ ω 𝑁 = suc 𝑘))
116	38, 112, 115	mpjaodan 787	. 2 ⊢ (𝜑 → ∃𝑧(𝑧 ∈ 𝑆 ∧ ∀𝑥(𝑥 ∈ 𝑧 ↔ (∃𝑚 ∈ ω (dom 𝐺 = suc 𝑚 ∧ 𝑥 ∈ (𝐹‘(𝐺‘𝑚))) ∨ (dom 𝐺 = ∅ ∧ 𝑥 ∈ 𝐴)))))
117		clabel 2266	. 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 697 ∀wal 1329 = wceq 1331 ∃wex 1468 ∈ wcel 1480 {cab 2125 ≠ wne 2308 ∀wral 2416 ∃wrex 2417 ∅c0 3363 suc csuc 4287 ωcom 4504 dom cdm 4539 ⟶wf 5119 ‘cfv 5123

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 603 ax-in2 604 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-13 1491 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-sep 4046 ax-nul 4054 ax-pow 4098 ax-pr 4131 ax-un 4355 ax-setind 4452 ax-iinf 4502

This theorem depends on definitions: df-bi 116 df-3an 964 df-tru 1334 df-nf 1437 df-sb 1736 df-eu 2002 df-mo 2003 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-ne 2309 df-ral 2421 df-rex 2422 df-v 2688 df-sbc 2910 df-dif 3073 df-un 3075 df-in 3077 df-ss 3084 df-nul 3364 df-pw 3512 df-sn 3533 df-pr 3534 df-op 3536 df-uni 3737 df-int 3772 df-br 3930 df-opab 3990 df-id 4215 df-suc 4293 df-iom 4505 df-xp 4545 df-rel 4546 df-cnv 4547 df-co 4548 df-dm 4549 df-rn 4550 df-iota 5088 df-fun 5125 df-fn 5126 df-f 5127 df-fv 5131

This theorem is referenced by: freccllem 6299 frecfcllem 6301 frecsuclem 6303

W3C validator