Theorem axdc2lem 10362

Description: Lemma for axdc2 10363. We construct a relation 𝑅 based on 𝐹 such that 𝑥𝑅𝑦 iff 𝑦 ∈ (𝐹‘𝑥), and show that the "function" described by ax-dc 10360 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 5854	. . . . . . 7 ⊢ dom 𝑅 = dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
3		19.42v 1955	. . . . . . . . 9 ⊢ (∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)))
4	3	abbii 2804	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))}
5		dmopab 5865	. . . . . . . 8 ⊢ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
6		df-rab 3401	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))}
7	4, 5, 6	3eqtr4i 2770	. . . . . . 7 ⊢ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)}
8	2, 7	eqtri 2760	. . . . . 6 ⊢ dom 𝑅 = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)}
9		ffvelcdm 7028	. . . . . . . . 9 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}))
10		eldifsni 4747	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹‘𝑥) ≠ ∅)
11		n0 4306	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))
12	10, 11	sylib 218	. . . . . . . . 9 ⊢ ((𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → ∃𝑦 𝑦 ∈ (𝐹‘𝑥))
13	9, 12	syl 17	. . . . . . . 8 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝐴) → ∃𝑦 𝑦 ∈ (𝐹‘𝑥))
14	13	ralrimiva 3129	. . . . . . 7 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 ∈ (𝐹‘𝑥))
15		rabid2 3433	. . . . . . 7 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 ∈ (𝐹‘𝑥))
16	14, 15	sylibr 234	. . . . . 6 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → 𝐴 = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)})
17	8, 16	eqtr4id 2791	. . . . 5 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → dom 𝑅 = 𝐴)
18	17	neeq1d 2992	. . . 4 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (dom 𝑅 ≠ ∅ ↔ 𝐴 ≠ ∅))
19	18	biimparc 479	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → dom 𝑅 ≠ ∅)
20	1	rneqi 5887	. . . . . . 7 ⊢ ran 𝑅 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
21		rnopab 5904	. . . . . . 7 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
22	20, 21	eqtri 2760	. . . . . 6 ⊢ ran 𝑅 = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
23		eldifi 4084	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹‘𝑥) ∈ 𝒫 𝐴)
24		elelpwi 4565	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (𝐹‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝒫 𝐴) → 𝑦 ∈ 𝐴)
25	24	expcom 413	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ∈ 𝒫 𝐴 → (𝑦 ∈ (𝐹‘𝑥) → 𝑦 ∈ 𝐴))
26	9, 23, 25	3syl 18	. . . . . . . . 9 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝐹‘𝑥) → 𝑦 ∈ 𝐴))
27	26	expimpd 453	. . . . . . . 8 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴))
28	27	exlimdv 1935	. . . . . . 7 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴))
29	28	abssdv 4020	. . . . . 6 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ⊆ 𝐴)
30	22, 29	eqsstrid 3973	. . . . 5 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝑅 ⊆ 𝐴)
31	30, 17	sseqtrrd 3972	. . . 4 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝑅 ⊆ dom 𝑅)
32	31	adantl 481	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝑅 ⊆ dom 𝑅)
33		fvrn0 6863	. . . . . . . . . 10 ⊢ (𝐹‘𝑥) ∈ (ran 𝐹 ∪ {∅})
34		elssuni 4895	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ∈ (ran 𝐹 ∪ {∅}) → (𝐹‘𝑥) ⊆ ∪ (ran 𝐹 ∪ {∅}))
35	33, 34	ax-mp 5	. . . . . . . . 9 ⊢ (𝐹‘𝑥) ⊆ ∪ (ran 𝐹 ∪ {∅})
36	35	sseli 3930	. . . . . . . 8 ⊢ (𝑦 ∈ (𝐹‘𝑥) → 𝑦 ∈ ∪ (ran 𝐹 ∪ {∅}))
37	36	anim2i 618	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∪ (ran 𝐹 ∪ {∅})))
38	37	ssopab2i 5499	. . . . . 6 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∪ (ran 𝐹 ∪ {∅}))}
39		df-xp 5631	. . . . . 6 ⊢ (𝐴 × ∪ (ran 𝐹 ∪ {∅})) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∪ (ran 𝐹 ∪ {∅}))}
40	38, 1, 39	3sstr4i 3986	. . . . 5 ⊢ 𝑅 ⊆ (𝐴 × ∪ (ran 𝐹 ∪ {∅}))
41		axdc2lem.1	. . . . . 6 ⊢ 𝐴 ∈ V
42		frn 6670	. . . . . . . . . 10 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}))
43	42	adantl 481	. . . . . . . . 9 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}))
44	41	pwex 5326	. . . . . . . . . . 11 ⊢ 𝒫 𝐴 ∈ V
45	44	difexi 5276	. . . . . . . . . 10 ⊢ (𝒫 𝐴 ∖ {∅}) ∈ V
46	45	ssex 5267	. . . . . . . . 9 ⊢ (ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}) → ran 𝐹 ∈ V)
47	43, 46	syl 17	. . . . . . . 8 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝐹 ∈ V)
48		p0ex 5330	. . . . . . . 8 ⊢ {∅} ∈ V
49		unexg 7690	. . . . . . . 8 ⊢ ((ran 𝐹 ∈ V ∧ {∅} ∈ V) → (ran 𝐹 ∪ {∅}) ∈ V)
50	47, 48, 49	sylancl 587	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (ran 𝐹 ∪ {∅}) ∈ V)
51	50	uniexd 7689	. . . . . 6 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∪ (ran 𝐹 ∪ {∅}) ∈ V)
52		xpexg 7697	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ ∪ (ran 𝐹 ∪ {∅}) ∈ V) → (𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∈ V)
53	41, 51, 52	sylancr 588	. . . . 5 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∈ V)
54		ssexg 5269	. . . . 5 ⊢ ((𝑅 ⊆ (𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∧ (𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∈ V) → 𝑅 ∈ V)
55	40, 53, 54	sylancr 588	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝑅 ∈ V)
56		n0 4306	. . . . . . . . 9 ⊢ (dom 𝑟 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ dom 𝑟)
57		vex 3445	. . . . . . . . . . 11 ⊢ 𝑥 ∈ V
58	57	eldm 5850	. . . . . . . . . 10 ⊢ (𝑥 ∈ dom 𝑟 ↔ ∃𝑦 𝑥𝑟𝑦)
59	58	exbii 1850	. . . . . . . . 9 ⊢ (∃𝑥 𝑥 ∈ dom 𝑟 ↔ ∃𝑥∃𝑦 𝑥𝑟𝑦)
60	56, 59	bitr2i 276	. . . . . . . 8 ⊢ (∃𝑥∃𝑦 𝑥𝑟𝑦 ↔ dom 𝑟 ≠ ∅)
61		dmeq 5853	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → dom 𝑟 = dom 𝑅)
62	61	neeq1d 2992	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (dom 𝑟 ≠ ∅ ↔ dom 𝑅 ≠ ∅))
63	60, 62	bitrid 283	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (∃𝑥∃𝑦 𝑥𝑟𝑦 ↔ dom 𝑅 ≠ ∅))
64		rneq 5886	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → ran 𝑟 = ran 𝑅)
65	64, 61	sseq12d 3968	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (ran 𝑟 ⊆ dom 𝑟 ↔ ran 𝑅 ⊆ dom 𝑅))
66	63, 65	anbi12d 633	. . . . . 6 ⊢ (𝑟 = 𝑅 → ((∃𝑥∃𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) ↔ (dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅)))
67		breq 5101	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → ((ℎ‘𝑘)𝑟(ℎ‘suc 𝑘) ↔ (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
68	67	ralbidv 3160	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘) ↔ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
69	68	exbidv 1923	. . . . . 6 ⊢ (𝑟 = 𝑅 → (∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘) ↔ ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
70	66, 69	imbi12d 344	. . . . 5 ⊢ (𝑟 = 𝑅 → (((∃𝑥∃𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘)) ↔ ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))))
71		ax-dc 10360	. . . . 5 ⊢ ((∃𝑥∃𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘))
72	70, 71	vtoclg 3512	. . . 4 ⊢ (𝑅 ∈ V → ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
73	55, 72	syl 17	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
74	19, 32, 73	mp2and 700	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))
75		simpr 484	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}))
76		fveq2 6835	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → (ℎ‘𝑘) = (ℎ‘𝑥))
77		suceq 6386	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑥 → suc 𝑘 = suc 𝑥)
78	77	fveq2d 6839	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑥))
79	76, 78	breq12d 5112	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → ((ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ↔ (ℎ‘𝑥)𝑅(ℎ‘suc 𝑥)))
80	79	rspccv 3574	. . . . . . . . . . . . 13 ⊢ (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝑥 ∈ ω → (ℎ‘𝑥)𝑅(ℎ‘suc 𝑥)))
81		fvex 6848	. . . . . . . . . . . . . 14 ⊢ (ℎ‘𝑥) ∈ V
82		fvex 6848	. . . . . . . . . . . . . 14 ⊢ (ℎ‘suc 𝑥) ∈ V
83	81, 82	breldm 5858	. . . . . . . . . . . . 13 ⊢ ((ℎ‘𝑥)𝑅(ℎ‘suc 𝑥) → (ℎ‘𝑥) ∈ dom 𝑅)
84	80, 83	syl6 35	. . . . . . . . . . . 12 ⊢ (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝑥 ∈ ω → (ℎ‘𝑥) ∈ dom 𝑅))
85	84	imp 406	. . . . . . . . . . 11 ⊢ ((∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝑥 ∈ ω) → (ℎ‘𝑥) ∈ dom 𝑅)
86	85	adantll 715	. . . . . . . . . 10 ⊢ (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) ∧ 𝑥 ∈ ω) → (ℎ‘𝑥) ∈ dom 𝑅)
87		eleq2 2826	. . . . . . . . . . 11 ⊢ (dom 𝑅 = 𝐴 → ((ℎ‘𝑥) ∈ dom 𝑅 ↔ (ℎ‘𝑥) ∈ 𝐴))
88	87	ad2antrr 727	. . . . . . . . . 10 ⊢ (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) ∧ 𝑥 ∈ ω) → ((ℎ‘𝑥) ∈ dom 𝑅 ↔ (ℎ‘𝑥) ∈ 𝐴))
89	86, 88	mpbid 232	. . . . . . . . 9 ⊢ (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) ∧ 𝑥 ∈ ω) → (ℎ‘𝑥) ∈ 𝐴)
90		axdc2lem.3	. . . . . . . . 9 ⊢ 𝐺 = (𝑥 ∈ ω ↦ (ℎ‘𝑥))
91	89, 90	fmptd 7061	. . . . . . . 8 ⊢ ((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) → 𝐺:ω⟶𝐴)
92	91	ex 412	. . . . . . 7 ⊢ (dom 𝑅 = 𝐴 → (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → 𝐺:ω⟶𝐴))
93	17, 92	syl 17	. . . . . 6 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → 𝐺:ω⟶𝐴))
94	93	impcom 407	. . . . 5 ⊢ ((∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝐺:ω⟶𝐴)
95		fveq2 6835	. . . . . . . . . 10 ⊢ (𝑥 = 𝑘 → (ℎ‘𝑥) = (ℎ‘𝑘))
96		fvex 6848	. . . . . . . . . 10 ⊢ (ℎ‘𝑘) ∈ V
97	95, 90, 96	fvmpt 6942	. . . . . . . . 9 ⊢ (𝑘 ∈ ω → (𝐺‘𝑘) = (ℎ‘𝑘))
98		peano2 7834	. . . . . . . . . 10 ⊢ (𝑘 ∈ ω → suc 𝑘 ∈ ω)
99		fvex 6848	. . . . . . . . . 10 ⊢ (ℎ‘suc 𝑘) ∈ V
100		fveq2 6835	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑘 → (ℎ‘𝑥) = (ℎ‘suc 𝑘))
101	100, 90	fvmptg 6940	. . . . . . . . . 10 ⊢ ((suc 𝑘 ∈ ω ∧ (ℎ‘suc 𝑘) ∈ V) → (𝐺‘suc 𝑘) = (ℎ‘suc 𝑘))
102	98, 99, 101	sylancl 587	. . . . . . . . 9 ⊢ (𝑘 ∈ ω → (𝐺‘suc 𝑘) = (ℎ‘suc 𝑘))
103	97, 102	breq12d 5112	. . . . . . . 8 ⊢ (𝑘 ∈ ω → ((𝐺‘𝑘)𝑅(𝐺‘suc 𝑘) ↔ (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
104		fvex 6848	. . . . . . . . . 10 ⊢ (𝐺‘𝑘) ∈ V
105		fvex 6848	. . . . . . . . . 10 ⊢ (𝐺‘suc 𝑘) ∈ V
106		eleq1 2825	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐺‘𝑘) → (𝑥 ∈ 𝐴 ↔ (𝐺‘𝑘) ∈ 𝐴))
107		fveq2 6835	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐺‘𝑘) → (𝐹‘𝑥) = (𝐹‘(𝐺‘𝑘)))
108	107	eleq2d 2823	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐺‘𝑘) → (𝑦 ∈ (𝐹‘𝑥) ↔ 𝑦 ∈ (𝐹‘(𝐺‘𝑘))))
109	106, 108	anbi12d 633	. . . . . . . . . 10 ⊢ (𝑥 = (𝐺‘𝑘) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) ↔ ((𝐺‘𝑘) ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘(𝐺‘𝑘)))))
110		eleq1 2825	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐺‘suc 𝑘) → (𝑦 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))
111	110	anbi2d 631	. . . . . . . . . 10 ⊢ (𝑦 = (𝐺‘suc 𝑘) → (((𝐺‘𝑘) ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘(𝐺‘𝑘))) ↔ ((𝐺‘𝑘) ∈ 𝐴 ∧ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))))
112	104, 105, 109, 111, 1	brab 5492	. . . . . . . . 9 ⊢ ((𝐺‘𝑘)𝑅(𝐺‘suc 𝑘) ↔ ((𝐺‘𝑘) ∈ 𝐴 ∧ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))
113	112	simprbi 496	. . . . . . . 8 ⊢ ((𝐺‘𝑘)𝑅(𝐺‘suc 𝑘) → (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))
114	103, 113	biimtrrdi 254	. . . . . . 7 ⊢ (𝑘 ∈ ω → ((ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))
115	114	ralimia 3071	. . . . . 6 ⊢ (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))
116	115	adantr 480	. . . . 5 ⊢ ((∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))
117		fvrn0 6863	. . . . . . . . . 10 ⊢ (ℎ‘𝑥) ∈ (ran ℎ ∪ {∅})
118	117	rgenw 3056	. . . . . . . . 9 ⊢ ∀𝑥 ∈ ω (ℎ‘𝑥) ∈ (ran ℎ ∪ {∅})
119		eqid 2737	. . . . . . . . . 10 ⊢ (𝑥 ∈ ω ↦ (ℎ‘𝑥)) = (𝑥 ∈ ω ↦ (ℎ‘𝑥))
120	119	fmpt 7057	. . . . . . . . 9 ⊢ (∀𝑥 ∈ ω (ℎ‘𝑥) ∈ (ran ℎ ∪ {∅}) ↔ (𝑥 ∈ ω ↦ (ℎ‘𝑥)):ω⟶(ran ℎ ∪ {∅}))
121	118, 120	mpbi 230	. . . . . . . 8 ⊢ (𝑥 ∈ ω ↦ (ℎ‘𝑥)):ω⟶(ran ℎ ∪ {∅})
122		dcomex 10361	. . . . . . . 8 ⊢ ω ∈ V
123		vex 3445	. . . . . . . . . 10 ⊢ ℎ ∈ V
124	123	rnex 7854	. . . . . . . . 9 ⊢ ran ℎ ∈ V
125	124, 48	unex 7691	. . . . . . . 8 ⊢ (ran ℎ ∪ {∅}) ∈ V
126		fex2 7880	. . . . . . . 8 ⊢ (((𝑥 ∈ ω ↦ (ℎ‘𝑥)):ω⟶(ran ℎ ∪ {∅}) ∧ ω ∈ V ∧ (ran ℎ ∪ {∅}) ∈ V) → (𝑥 ∈ ω ↦ (ℎ‘𝑥)) ∈ V)
127	121, 122, 125, 126	mp3an 1464	. . . . . . 7 ⊢ (𝑥 ∈ ω ↦ (ℎ‘𝑥)) ∈ V
128	90, 127	eqeltri 2833	. . . . . 6 ⊢ 𝐺 ∈ V
129		feq1 6641	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (𝑔:ω⟶𝐴 ↔ 𝐺:ω⟶𝐴))
130		fveq1 6834	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (𝑔‘suc 𝑘) = (𝐺‘suc 𝑘))
131		fveq1 6834	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → (𝑔‘𝑘) = (𝐺‘𝑘))
132	131	fveq2d 6839	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (𝐹‘(𝑔‘𝑘)) = (𝐹‘(𝐺‘𝑘)))
133	130, 132	eleq12d 2831	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → ((𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))
134	133	ralbidv 3160	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))
135	129, 134	anbi12d 633	. . . . . 6 ⊢ (𝑔 = 𝐺 → ((𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))) ↔ (𝐺:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))))
136	128, 135	spcev 3561	. . . . 5 ⊢ ((𝐺:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))
137	94, 116, 136	syl2anc 585	. . . 4 ⊢ ((∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))
138	137	ex 412	. . 3 ⊢ (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))))
139	138	exlimiv 1932	. 2 ⊢ (∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))))
140	74, 75, 139	sylc 65	1 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  {cab 2715   ≠ wne 2933  ∀wral 3052  {crab 3400  Vcvv 3441   ∖ cdif 3899   ∪ cun 3900   ⊆ wss 3902  ∅c0 4286  𝒫 cpw 4555  {csn 4581  ∪ cuni 4864   class class class wbr 5099  {copab 5161   ↦ cmpt 5180   × cxp 5623  dom cdm 5625  ran crn 5626  suc csuc 6320  ⟶wf 6489  ‘cfv 6493  ωcom 7810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682  ax-dc 10360

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501  df-om 7811  df-1o 8399

This theorem is referenced by:  axdc2  10363