Theorem axdc2lem 10498

Description: Lemma for axdc2 10499. We construct a relation 𝑅 based on 𝐹 such that 𝑥𝑅𝑦 iff 𝑦 ∈ (𝐹‘𝑥), and show that the "function" described by ax-dc 10496 can be restricted so that it is a real function (since the stated properties only show that it is the superset of a function). (Contributed by Mario Carneiro, 25-Jan-2013.) (Revised by Mario Carneiro, 26-Jun-2015.)

Hypotheses

Ref	Expression
axdc2lem.1	⊢ 𝐴 ∈ V
axdc2lem.2	⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
axdc2lem.3	⊢ 𝐺 = (𝑥 ∈ ω ↦ (ℎ‘𝑥))

Assertion

Ref	Expression
axdc2lem	⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))

Distinct variable groups:   𝐴,𝑔,ℎ   𝑥,𝐴,𝑦,ℎ   𝑔,𝐹,ℎ   𝑥,𝐹,𝑦   𝑔,𝐺,𝑘   𝑥,𝐺,𝑦,𝑘   𝑅,ℎ,𝑘,𝑥

Allowed substitution hints:   𝐴(𝑘)   𝑅(𝑦, 𝑔)   𝐹(𝑘)   𝐺(ℎ)

Proof of Theorem axdc2lem

Dummy variable 𝑟 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		axdc2lem.2	. . . . . . . 8 ⊢ 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
2	1	dmeqi 5882	. . . . . . 7 ⊢ dom 𝑅 = dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
3		19.42v 1986	. . . . . . . . 9 ⊢ (∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)))
4	3	abbii 2827	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))}
5		dmopab 5893	. . . . . . . 8 ⊢ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
6		df-rab 3413	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))}
7	4, 5, 6	3eqtr4i 2793	. . . . . . 7 ⊢ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)}
8	2, 7	eqtri 2783	. . . . . 6 ⊢ dom 𝑅 = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)}
9		ffvelcdm 7069	. . . . . . . . 9 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}))
10		eldifsni 4752	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹‘𝑥) ≠ ∅)
11		n0 4299	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))
12	10, 11	sylib 221	. . . . . . . . 9 ⊢ ((𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → ∃𝑦 𝑦 ∈ (𝐹‘𝑥))
13	9, 12	syl 18	. . . . . . . 8 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝐴) → ∃𝑦 𝑦 ∈ (𝐹‘𝑥))
14	13	ralrimiva 3154	. . . . . . 7 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 ∈ (𝐹‘𝑥))
15		rabid2 3444	. . . . . . 7 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 ∈ (𝐹‘𝑥))
16	14, 15	sylibr 237	. . . . . 6 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → 𝐴 = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)})
17	8, 16	eqtr4id 2814	. . . . 5 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → dom 𝑅 = 𝐴)
18	17	neeq1d 3014	. . . 4 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (dom 𝑅 ≠ ∅ ↔ 𝐴 ≠ ∅))
19	18	biimparc 485	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → dom 𝑅 ≠ ∅)
20	1	rneqi 5915	. . . . . . 7 ⊢ ran 𝑅 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
21		rnopab 5932	. . . . . . 7 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
22	20, 21	eqtri 2783	. . . . . 6 ⊢ ran 𝑅 = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
23		eldifi 4077	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹‘𝑥) ∈ 𝒫 𝐴)
24		elelpwi 4566	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (𝐹‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝒫 𝐴) → 𝑦 ∈ 𝐴)
25	24	expcom 419	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ∈ 𝒫 𝐴 → (𝑦 ∈ (𝐹‘𝑥) → 𝑦 ∈ 𝐴))
26	9, 23, 25	3syl 19	. . . . . . . . 9 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝐹‘𝑥) → 𝑦 ∈ 𝐴))
27	26	expimpd 459	. . . . . . . 8 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴))
28	27	exlimdv 1966	. . . . . . 7 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴))
29	28	abssdv 4014	. . . . . 6 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ⊆ 𝐴)
30	22, 29	eqsstrid 3968	. . . . 5 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝑅 ⊆ 𝐴)
31	30, 17	sseqtrrd 3967	. . . 4 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝑅 ⊆ dom 𝑅)
32	31	adantl 487	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝑅 ⊆ dom 𝑅)
33		fvrn0 6901	. . . . . . . . . 10 ⊢ (𝐹‘𝑥) ∈ (ran 𝐹 ∪ {∅})
34		elssuni 4898	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ∈ (ran 𝐹 ∪ {∅}) → (𝐹‘𝑥) ⊆ ∪ (ran 𝐹 ∪ {∅}))
35	33, 34	ax-mp 5	. . . . . . . . 9 ⊢ (𝐹‘𝑥) ⊆ ∪ (ran 𝐹 ∪ {∅})
36	35	sseli 3926	. . . . . . . 8 ⊢ (𝑦 ∈ (𝐹‘𝑥) → 𝑦 ∈ ∪ (ran 𝐹 ∪ {∅}))
37	36	anim2i 629	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∪ (ran 𝐹 ∪ {∅})))
38	37	ssopab2i 5521	. . . . . 6 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∪ (ran 𝐹 ∪ {∅}))}
39		df-xp 5653	. . . . . 6 ⊢ (𝐴 × ∪ (ran 𝐹 ∪ {∅})) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∪ (ran 𝐹 ∪ {∅}))}
40	38, 1, 39	3sstr4i 3981	. . . . 5 ⊢ 𝑅 ⊆ (𝐴 × ∪ (ran 𝐹 ∪ {∅}))
41		axdc2lem.1	. . . . . 6 ⊢ 𝐴 ∈ V
42		frn 6705	. . . . . . . . . 10 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}))
43	42	adantl 487	. . . . . . . . 9 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}))
44	41	pwex 5341	. . . . . . . . . . 11 ⊢ 𝒫 𝐴 ∈ V
45	44	difexi 5291	. . . . . . . . . 10 ⊢ (𝒫 𝐴 ∖ {∅}) ∈ V
46	45	ssex 5281	. . . . . . . . 9 ⊢ (ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}) → ran 𝐹 ∈ V)
47	43, 46	syl 18	. . . . . . . 8 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝐹 ∈ V)
48		p0ex 5345	. . . . . . . 8 ⊢ {∅} ∈ V
49		unexg 7743	. . . . . . . 8 ⊢ ((ran 𝐹 ∈ V ∧ {∅} ∈ V) → (ran 𝐹 ∪ {∅}) ∈ V)
50	47, 48, 49	sylancl 598	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (ran 𝐹 ∪ {∅}) ∈ V)
51	50	uniexd 7742	. . . . . 6 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∪ (ran 𝐹 ∪ {∅}) ∈ V)
52		xpexg 7747	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ ∪ (ran 𝐹 ∪ {∅}) ∈ V) → (𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∈ V)
53	41, 51, 52	sylancr 599	. . . . 5 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∈ V)
54		ssexg 5280	. . . . 5 ⊢ ((𝑅 ⊆ (𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∧ (𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∈ V) → 𝑅 ∈ V)
55	40, 53, 54	sylancr 599	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝑅 ∈ V)
56		n0 4299	. . . . . . . . 9 ⊢ (dom 𝑟 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ dom 𝑟)
57		vex 3454	. . . . . . . . . . 11 ⊢ 𝑥 ∈ V
58	57	eldm 5878	. . . . . . . . . 10 ⊢ (𝑥 ∈ dom 𝑟 ↔ ∃𝑦 𝑥𝑟𝑦)
59	58	exbii 1881	. . . . . . . . 9 ⊢ (∃𝑥 𝑥 ∈ dom 𝑟 ↔ ∃𝑥∃𝑦 𝑥𝑟𝑦)
60	56, 59	bitr2i 279	. . . . . . . 8 ⊢ (∃𝑥∃𝑦 𝑥𝑟𝑦 ↔ dom 𝑟 ≠ ∅)
61		dmeq 5881	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → dom 𝑟 = dom 𝑅)
62	61	neeq1d 3014	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (dom 𝑟 ≠ ∅ ↔ dom 𝑅 ≠ ∅))
63	60, 62	bitrid 286	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (∃𝑥∃𝑦 𝑥𝑟𝑦 ↔ dom 𝑅 ≠ ∅))
64		rneq 5914	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → ran 𝑟 = ran 𝑅)
65	64, 61	sseq12d 3963	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (ran 𝑟 ⊆ dom 𝑟 ↔ ran 𝑅 ⊆ dom 𝑅))
66	63, 65	anbi12d 644	. . . . . 6 ⊢ (𝑟 = 𝑅 → ((∃𝑥∃𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) ↔ (dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅)))
67		breq 5104	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → ((ℎ‘𝑘)𝑟(ℎ‘suc 𝑘) ↔ (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
68	67	ralbidv 3185	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘) ↔ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
69	68	exbidv 1954	. . . . . 6 ⊢ (𝑟 = 𝑅 → (∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘) ↔ ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
70	66, 69	imbi12d 347	. . . . 5 ⊢ (𝑟 = 𝑅 → (((∃𝑥∃𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘)) ↔ ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))))
71		ax-dc 10496	. . . . 5 ⊢ ((∃𝑥∃𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘))
72	70, 71	vtoclg 3517	. . . 4 ⊢ (𝑅 ∈ V → ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
73	55, 72	syl 18	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
74	19, 32, 73	mp2and 712	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))
75		simpr 490	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}))
76		fveq2 6873	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → (ℎ‘𝑘) = (ℎ‘𝑥))
77		suceq 6420	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑥 → suc 𝑘 = suc 𝑥)
78	77	fveq2d 6877	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑥))
79	76, 78	breq12d 5115	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → ((ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ↔ (ℎ‘𝑥)𝑅(ℎ‘suc 𝑥)))
80	79	rspccv 3573	. . . . . . . . . . . . 13 ⊢ (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝑥 ∈ ω → (ℎ‘𝑥)𝑅(ℎ‘suc 𝑥)))
81		fvex 6886	. . . . . . . . . . . . . 14 ⊢ (ℎ‘𝑥) ∈ V
82		fvex 6886	. . . . . . . . . . . . . 14 ⊢ (ℎ‘suc 𝑥) ∈ V
83	81, 82	breldm 5886	. . . . . . . . . . . . 13 ⊢ ((ℎ‘𝑥)𝑅(ℎ‘suc 𝑥) → (ℎ‘𝑥) ∈ dom 𝑅)
84	80, 83	syl6 36	. . . . . . . . . . . 12 ⊢ (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝑥 ∈ ω → (ℎ‘𝑥) ∈ dom 𝑅))
85	84	imp 412	. . . . . . . . . . 11 ⊢ ((∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝑥 ∈ ω) → (ℎ‘𝑥) ∈ dom 𝑅)
86	85	adantll 727	. . . . . . . . . 10 ⊢ (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) ∧ 𝑥 ∈ ω) → (ℎ‘𝑥) ∈ dom 𝑅)
87		eleq2 2849	. . . . . . . . . . 11 ⊢ (dom 𝑅 = 𝐴 → ((ℎ‘𝑥) ∈ dom 𝑅 ↔ (ℎ‘𝑥) ∈ 𝐴))
88	87	ad2antrr 739	. . . . . . . . . 10 ⊢ (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) ∧ 𝑥 ∈ ω) → ((ℎ‘𝑥) ∈ dom 𝑅 ↔ (ℎ‘𝑥) ∈ 𝐴))
89	86, 88	mpbid 235	. . . . . . . . 9 ⊢ (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) ∧ 𝑥 ∈ ω) → (ℎ‘𝑥) ∈ 𝐴)
90		axdc2lem.3	. . . . . . . . 9 ⊢ 𝐺 = (𝑥 ∈ ω ↦ (ℎ‘𝑥))
91	89, 90	fmptd 7102	. . . . . . . 8 ⊢ ((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) → 𝐺:ω⟶𝐴)
92	91	ex 418	. . . . . . 7 ⊢ (dom 𝑅 = 𝐴 → (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → 𝐺:ω⟶𝐴))
93	17, 92	syl 18	. . . . . 6 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → 𝐺:ω⟶𝐴))
94	93	impcom 413	. . . . 5 ⊢ ((∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝐺:ω⟶𝐴)
95		fveq2 6873	. . . . . . . . . 10 ⊢ (𝑥 = 𝑘 → (ℎ‘𝑥) = (ℎ‘𝑘))
96		fvex 6886	. . . . . . . . . 10 ⊢ (ℎ‘𝑘) ∈ V
97	95, 90, 96	fvmpt 6981	. . . . . . . . 9 ⊢ (𝑘 ∈ ω → (𝐺‘𝑘) = (ℎ‘𝑘))
98		peano2 7884	. . . . . . . . . 10 ⊢ (𝑘 ∈ ω → suc 𝑘 ∈ ω)
99		fvex 6886	. . . . . . . . . 10 ⊢ (ℎ‘suc 𝑘) ∈ V
100		fveq2 6873	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑘 → (ℎ‘𝑥) = (ℎ‘suc 𝑘))
101	100, 90	fvmptg 6979	. . . . . . . . . 10 ⊢ ((suc 𝑘 ∈ ω ∧ (ℎ‘suc 𝑘) ∈ V) → (𝐺‘suc 𝑘) = (ℎ‘suc 𝑘))
102	98, 99, 101	sylancl 598	. . . . . . . . 9 ⊢ (𝑘 ∈ ω → (𝐺‘suc 𝑘) = (ℎ‘suc 𝑘))
103	97, 102	breq12d 5115	. . . . . . . 8 ⊢ (𝑘 ∈ ω → ((𝐺‘𝑘)𝑅(𝐺‘suc 𝑘) ↔ (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
104		fvex 6886	. . . . . . . . . 10 ⊢ (𝐺‘𝑘) ∈ V
105		fvex 6886	. . . . . . . . . 10 ⊢ (𝐺‘suc 𝑘) ∈ V
106		eleq1 2848	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐺‘𝑘) → (𝑥 ∈ 𝐴 ↔ (𝐺‘𝑘) ∈ 𝐴))
107		fveq2 6873	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐺‘𝑘) → (𝐹‘𝑥) = (𝐹‘(𝐺‘𝑘)))
108	107	eleq2d 2846	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐺‘𝑘) → (𝑦 ∈ (𝐹‘𝑥) ↔ 𝑦 ∈ (𝐹‘(𝐺‘𝑘))))
109	106, 108	anbi12d 644	. . . . . . . . . 10 ⊢ (𝑥 = (𝐺‘𝑘) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) ↔ ((𝐺‘𝑘) ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘(𝐺‘𝑘)))))
110		eleq1 2848	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐺‘suc 𝑘) → (𝑦 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))
111	110	anbi2d 642	. . . . . . . . . 10 ⊢ (𝑦 = (𝐺‘suc 𝑘) → (((𝐺‘𝑘) ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘(𝐺‘𝑘))) ↔ ((𝐺‘𝑘) ∈ 𝐴 ∧ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))))
112	104, 105, 109, 111, 1	brab 5514	. . . . . . . . 9 ⊢ ((𝐺‘𝑘)𝑅(𝐺‘suc 𝑘) ↔ ((𝐺‘𝑘) ∈ 𝐴 ∧ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))
113	112	simprbi 503	. . . . . . . 8 ⊢ ((𝐺‘𝑘)𝑅(𝐺‘suc 𝑘) → (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))
114	103, 113	biimtrrdi 257	. . . . . . 7 ⊢ (𝑘 ∈ ω → ((ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))
115	114	ralimia 3096	. . . . . 6 ⊢ (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))
116	115	adantr 486	. . . . 5 ⊢ ((∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))
117		fvrn0 6901	. . . . . . . . . 10 ⊢ (ℎ‘𝑥) ∈ (ran ℎ ∪ {∅})
118	117	rgenw 3080	. . . . . . . . 9 ⊢ ∀𝑥 ∈ ω (ℎ‘𝑥) ∈ (ran ℎ ∪ {∅})
119		eqid 2760	. . . . . . . . . 10 ⊢ (𝑥 ∈ ω ↦ (ℎ‘𝑥)) = (𝑥 ∈ ω ↦ (ℎ‘𝑥))
120	119	fmpt 7098	. . . . . . . . 9 ⊢ (∀𝑥 ∈ ω (ℎ‘𝑥) ∈ (ran ℎ ∪ {∅}) ↔ (𝑥 ∈ ω ↦ (ℎ‘𝑥)):ω⟶(ran ℎ ∪ {∅}))
121	118, 120	mpbi 233	. . . . . . . 8 ⊢ (𝑥 ∈ ω ↦ (ℎ‘𝑥)):ω⟶(ran ℎ ∪ {∅})
122		dcomex 10497	. . . . . . . 8 ⊢ ω ∈ V
123		vex 3454	. . . . . . . . . 10 ⊢ ℎ ∈ V
124	123	rnex 7905	. . . . . . . . 9 ⊢ ran ℎ ∈ V
125	124, 48	unex 7744	. . . . . . . 8 ⊢ (ran ℎ ∪ {∅}) ∈ V
126		fex2 7931	. . . . . . . 8 ⊢ (((𝑥 ∈ ω ↦ (ℎ‘𝑥)):ω⟶(ran ℎ ∪ {∅}) ∧ ω ∈ V ∧ (ran ℎ ∪ {∅}) ∈ V) → (𝑥 ∈ ω ↦ (ℎ‘𝑥)) ∈ V)
127	121, 122, 125, 126	mp3an 1490	. . . . . . 7 ⊢ (𝑥 ∈ ω ↦ (ℎ‘𝑥)) ∈ V
128	90, 127	eqeltri 2856	. . . . . 6 ⊢ 𝐺 ∈ V
129		feq1 6675	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (𝑔:ω⟶𝐴 ↔ 𝐺:ω⟶𝐴))
130		fveq1 6872	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (𝑔‘suc 𝑘) = (𝐺‘suc 𝑘))
131		fveq1 6872	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → (𝑔‘𝑘) = (𝐺‘𝑘))
132	131	fveq2d 6877	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (𝐹‘(𝑔‘𝑘)) = (𝐹‘(𝐺‘𝑘)))
133	130, 132	eleq12d 2854	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → ((𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))
134	133	ralbidv 3185	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))
135	129, 134	anbi12d 644	. . . . . 6 ⊢ (𝑔 = 𝐺 → ((𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))) ↔ (𝐺:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))))
136	128, 135	spcev 3560	. . . . 5 ⊢ ((𝐺:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))
137	94, 116, 136	syl2anc 596	. . . 4 ⊢ ((∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))
138	137	ex 418	. . 3 ⊢ (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))))
139	138	exlimiv 1963	. 2 ⊢ (∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))))
140	74, 75, 139	sylc 66	1 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145  {cab 2738   ≠ wne 2955  ∀wral 3076  {crab 3412  Vcvv 3450   ∖ cdif 3895   ∪ cun 3896   ⊆ wss 3898  ∅c0 4278  𝒫 cpw 4556  {csn 4583  ∪ cuni 4866   class class class wbr 5102  {copab 5166   ↦ cmpt 5185   × cxp 5645  dom cdm 5647  ran crn 5648  suc csuc 6353  ⟶wf 6523  ‘cfv 6527  ωcom 7860

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 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7734  ax-dc 10496

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-ord 6354  df-on 6355  df-lim 6356  df-suc 6357  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-fv 6535  df-om 7861  df-1o 8454

This theorem is used by:  axdc2  10499