Theorem axdc2lem 10345

Description: Lemma for axdc2 10346. We construct a relation 𝑅 based on 𝐹 such that 𝑥𝑅𝑦 iff 𝑦 ∈ (𝐹‘𝑥), and show that the "function" described by ax-dc 10343 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 5849	. . . . . . 7 ⊢ dom 𝑅 = dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
3		19.42v 1954	. . . . . . . . 9 ⊢ (∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)))
4	3	abbii 2798	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))}
5		dmopab 5860	. . . . . . . 8 ⊢ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
6		df-rab 3396	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))}
7	4, 5, 6	3eqtr4i 2764	. . . . . . 7 ⊢ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)}
8	2, 7	eqtri 2754	. . . . . 6 ⊢ dom 𝑅 = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)}
9		ffvelcdm 7020	. . . . . . . . 9 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}))
10		eldifsni 4741	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹‘𝑥) ≠ ∅)
11		n0 4302	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))
12	10, 11	sylib 218	. . . . . . . . 9 ⊢ ((𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → ∃𝑦 𝑦 ∈ (𝐹‘𝑥))
13	9, 12	syl 17	. . . . . . . 8 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝐴) → ∃𝑦 𝑦 ∈ (𝐹‘𝑥))
14	13	ralrimiva 3124	. . . . . . 7 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 ∈ (𝐹‘𝑥))
15		rabid2 3428	. . . . . . 7 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 ∈ (𝐹‘𝑥))
16	14, 15	sylibr 234	. . . . . 6 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → 𝐴 = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)})
17	8, 16	eqtr4id 2785	. . . . 5 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → dom 𝑅 = 𝐴)
18	17	neeq1d 2987	. . . 4 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (dom 𝑅 ≠ ∅ ↔ 𝐴 ≠ ∅))
19	18	biimparc 479	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → dom 𝑅 ≠ ∅)
20	1	rneqi 5882	. . . . . . 7 ⊢ ran 𝑅 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
21		rnopab 5899	. . . . . . 7 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
22	20, 21	eqtri 2754	. . . . . 6 ⊢ ran 𝑅 = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
23		eldifi 4080	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹‘𝑥) ∈ 𝒫 𝐴)
24		elelpwi 4559	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (𝐹‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝒫 𝐴) → 𝑦 ∈ 𝐴)
25	24	expcom 413	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ∈ 𝒫 𝐴 → (𝑦 ∈ (𝐹‘𝑥) → 𝑦 ∈ 𝐴))
26	9, 23, 25	3syl 18	. . . . . . . . 9 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝐹‘𝑥) → 𝑦 ∈ 𝐴))
27	26	expimpd 453	. . . . . . . 8 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴))
28	27	exlimdv 1934	. . . . . . 7 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴))
29	28	abssdv 4015	. . . . . 6 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ⊆ 𝐴)
30	22, 29	eqsstrid 3968	. . . . 5 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝑅 ⊆ 𝐴)
31	30, 17	sseqtrrd 3967	. . . 4 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝑅 ⊆ dom 𝑅)
32	31	adantl 481	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝑅 ⊆ dom 𝑅)
33		fvrn0 6856	. . . . . . . . . 10 ⊢ (𝐹‘𝑥) ∈ (ran 𝐹 ∪ {∅})
34		elssuni 4889	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ∈ (ran 𝐹 ∪ {∅}) → (𝐹‘𝑥) ⊆ ∪ (ran 𝐹 ∪ {∅}))
35	33, 34	ax-mp 5	. . . . . . . . 9 ⊢ (𝐹‘𝑥) ⊆ ∪ (ran 𝐹 ∪ {∅})
36	35	sseli 3925	. . . . . . . 8 ⊢ (𝑦 ∈ (𝐹‘𝑥) → 𝑦 ∈ ∪ (ran 𝐹 ∪ {∅}))
37	36	anim2i 617	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∪ (ran 𝐹 ∪ {∅})))
38	37	ssopab2i 5493	. . . . . 6 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∪ (ran 𝐹 ∪ {∅}))}
39		df-xp 5625	. . . . . 6 ⊢ (𝐴 × ∪ (ran 𝐹 ∪ {∅})) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∪ (ran 𝐹 ∪ {∅}))}
40	38, 1, 39	3sstr4i 3981	. . . . 5 ⊢ 𝑅 ⊆ (𝐴 × ∪ (ran 𝐹 ∪ {∅}))
41		axdc2lem.1	. . . . . 6 ⊢ 𝐴 ∈ V
42		frn 6664	. . . . . . . . . 10 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}))
43	42	adantl 481	. . . . . . . . 9 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}))
44	41	pwex 5320	. . . . . . . . . . 11 ⊢ 𝒫 𝐴 ∈ V
45	44	difexi 5270	. . . . . . . . . 10 ⊢ (𝒫 𝐴 ∖ {∅}) ∈ V
46	45	ssex 5261	. . . . . . . . 9 ⊢ (ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}) → ran 𝐹 ∈ V)
47	43, 46	syl 17	. . . . . . . 8 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝐹 ∈ V)
48		p0ex 5324	. . . . . . . 8 ⊢ {∅} ∈ V
49		unexg 7682	. . . . . . . 8 ⊢ ((ran 𝐹 ∈ V ∧ {∅} ∈ V) → (ran 𝐹 ∪ {∅}) ∈ V)
50	47, 48, 49	sylancl 586	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (ran 𝐹 ∪ {∅}) ∈ V)
51	50	uniexd 7681	. . . . . 6 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∪ (ran 𝐹 ∪ {∅}) ∈ V)
52		xpexg 7689	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ ∪ (ran 𝐹 ∪ {∅}) ∈ V) → (𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∈ V)
53	41, 51, 52	sylancr 587	. . . . 5 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∈ V)
54		ssexg 5263	. . . . 5 ⊢ ((𝑅 ⊆ (𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∧ (𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∈ V) → 𝑅 ∈ V)
55	40, 53, 54	sylancr 587	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝑅 ∈ V)
56		n0 4302	. . . . . . . . 9 ⊢ (dom 𝑟 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ dom 𝑟)
57		vex 3440	. . . . . . . . . . 11 ⊢ 𝑥 ∈ V
58	57	eldm 5845	. . . . . . . . . 10 ⊢ (𝑥 ∈ dom 𝑟 ↔ ∃𝑦 𝑥𝑟𝑦)
59	58	exbii 1849	. . . . . . . . 9 ⊢ (∃𝑥 𝑥 ∈ dom 𝑟 ↔ ∃𝑥∃𝑦 𝑥𝑟𝑦)
60	56, 59	bitr2i 276	. . . . . . . 8 ⊢ (∃𝑥∃𝑦 𝑥𝑟𝑦 ↔ dom 𝑟 ≠ ∅)
61		dmeq 5848	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → dom 𝑟 = dom 𝑅)
62	61	neeq1d 2987	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (dom 𝑟 ≠ ∅ ↔ dom 𝑅 ≠ ∅))
63	60, 62	bitrid 283	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (∃𝑥∃𝑦 𝑥𝑟𝑦 ↔ dom 𝑅 ≠ ∅))
64		rneq 5881	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → ran 𝑟 = ran 𝑅)
65	64, 61	sseq12d 3963	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (ran 𝑟 ⊆ dom 𝑟 ↔ ran 𝑅 ⊆ dom 𝑅))
66	63, 65	anbi12d 632	. . . . . 6 ⊢ (𝑟 = 𝑅 → ((∃𝑥∃𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) ↔ (dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅)))
67		breq 5095	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → ((ℎ‘𝑘)𝑟(ℎ‘suc 𝑘) ↔ (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
68	67	ralbidv 3155	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘) ↔ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
69	68	exbidv 1922	. . . . . 6 ⊢ (𝑟 = 𝑅 → (∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘) ↔ ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
70	66, 69	imbi12d 344	. . . . 5 ⊢ (𝑟 = 𝑅 → (((∃𝑥∃𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘)) ↔ ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))))
71		ax-dc 10343	. . . . 5 ⊢ ((∃𝑥∃𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘))
72	70, 71	vtoclg 3507	. . . 4 ⊢ (𝑅 ∈ V → ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
73	55, 72	syl 17	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
74	19, 32, 73	mp2and 699	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))
75		simpr 484	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}))
76		fveq2 6828	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → (ℎ‘𝑘) = (ℎ‘𝑥))
77		suceq 6380	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑥 → suc 𝑘 = suc 𝑥)
78	77	fveq2d 6832	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑥))
79	76, 78	breq12d 5106	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → ((ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ↔ (ℎ‘𝑥)𝑅(ℎ‘suc 𝑥)))
80	79	rspccv 3569	. . . . . . . . . . . . 13 ⊢ (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝑥 ∈ ω → (ℎ‘𝑥)𝑅(ℎ‘suc 𝑥)))
81		fvex 6841	. . . . . . . . . . . . . 14 ⊢ (ℎ‘𝑥) ∈ V
82		fvex 6841	. . . . . . . . . . . . . 14 ⊢ (ℎ‘suc 𝑥) ∈ V
83	81, 82	breldm 5853	. . . . . . . . . . . . 13 ⊢ ((ℎ‘𝑥)𝑅(ℎ‘suc 𝑥) → (ℎ‘𝑥) ∈ dom 𝑅)
84	80, 83	syl6 35	. . . . . . . . . . . 12 ⊢ (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝑥 ∈ ω → (ℎ‘𝑥) ∈ dom 𝑅))
85	84	imp 406	. . . . . . . . . . 11 ⊢ ((∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝑥 ∈ ω) → (ℎ‘𝑥) ∈ dom 𝑅)
86	85	adantll 714	. . . . . . . . . 10 ⊢ (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) ∧ 𝑥 ∈ ω) → (ℎ‘𝑥) ∈ dom 𝑅)
87		eleq2 2820	. . . . . . . . . . 11 ⊢ (dom 𝑅 = 𝐴 → ((ℎ‘𝑥) ∈ dom 𝑅 ↔ (ℎ‘𝑥) ∈ 𝐴))
88	87	ad2antrr 726	. . . . . . . . . 10 ⊢ (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) ∧ 𝑥 ∈ ω) → ((ℎ‘𝑥) ∈ dom 𝑅 ↔ (ℎ‘𝑥) ∈ 𝐴))
89	86, 88	mpbid 232	. . . . . . . . 9 ⊢ (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) ∧ 𝑥 ∈ ω) → (ℎ‘𝑥) ∈ 𝐴)
90		axdc2lem.3	. . . . . . . . 9 ⊢ 𝐺 = (𝑥 ∈ ω ↦ (ℎ‘𝑥))
91	89, 90	fmptd 7053	. . . . . . . 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 6828	. . . . . . . . . 10 ⊢ (𝑥 = 𝑘 → (ℎ‘𝑥) = (ℎ‘𝑘))
96		fvex 6841	. . . . . . . . . 10 ⊢ (ℎ‘𝑘) ∈ V
97	95, 90, 96	fvmpt 6935	. . . . . . . . 9 ⊢ (𝑘 ∈ ω → (𝐺‘𝑘) = (ℎ‘𝑘))
98		peano2 7826	. . . . . . . . . 10 ⊢ (𝑘 ∈ ω → suc 𝑘 ∈ ω)
99		fvex 6841	. . . . . . . . . 10 ⊢ (ℎ‘suc 𝑘) ∈ V
100		fveq2 6828	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑘 → (ℎ‘𝑥) = (ℎ‘suc 𝑘))
101	100, 90	fvmptg 6933	. . . . . . . . . 10 ⊢ ((suc 𝑘 ∈ ω ∧ (ℎ‘suc 𝑘) ∈ V) → (𝐺‘suc 𝑘) = (ℎ‘suc 𝑘))
102	98, 99, 101	sylancl 586	. . . . . . . . 9 ⊢ (𝑘 ∈ ω → (𝐺‘suc 𝑘) = (ℎ‘suc 𝑘))
103	97, 102	breq12d 5106	. . . . . . . 8 ⊢ (𝑘 ∈ ω → ((𝐺‘𝑘)𝑅(𝐺‘suc 𝑘) ↔ (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
104		fvex 6841	. . . . . . . . . 10 ⊢ (𝐺‘𝑘) ∈ V
105		fvex 6841	. . . . . . . . . 10 ⊢ (𝐺‘suc 𝑘) ∈ V
106		eleq1 2819	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐺‘𝑘) → (𝑥 ∈ 𝐴 ↔ (𝐺‘𝑘) ∈ 𝐴))
107		fveq2 6828	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐺‘𝑘) → (𝐹‘𝑥) = (𝐹‘(𝐺‘𝑘)))
108	107	eleq2d 2817	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐺‘𝑘) → (𝑦 ∈ (𝐹‘𝑥) ↔ 𝑦 ∈ (𝐹‘(𝐺‘𝑘))))
109	106, 108	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑥 = (𝐺‘𝑘) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) ↔ ((𝐺‘𝑘) ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘(𝐺‘𝑘)))))
110		eleq1 2819	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐺‘suc 𝑘) → (𝑦 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))
111	110	anbi2d 630	. . . . . . . . . 10 ⊢ (𝑦 = (𝐺‘suc 𝑘) → (((𝐺‘𝑘) ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘(𝐺‘𝑘))) ↔ ((𝐺‘𝑘) ∈ 𝐴 ∧ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))))
112	104, 105, 109, 111, 1	brab 5486	. . . . . . . . 9 ⊢ ((𝐺‘𝑘)𝑅(𝐺‘suc 𝑘) ↔ ((𝐺‘𝑘) ∈ 𝐴 ∧ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))
113	112	simprbi 496	. . . . . . . 8 ⊢ ((𝐺‘𝑘)𝑅(𝐺‘suc 𝑘) → (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))
114	103, 113	biimtrrdi 254	. . . . . . 7 ⊢ (𝑘 ∈ ω → ((ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))
115	114	ralimia 3066	. . . . . 6 ⊢ (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))
116	115	adantr 480	. . . . 5 ⊢ ((∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))
117		fvrn0 6856	. . . . . . . . . 10 ⊢ (ℎ‘𝑥) ∈ (ran ℎ ∪ {∅})
118	117	rgenw 3051	. . . . . . . . 9 ⊢ ∀𝑥 ∈ ω (ℎ‘𝑥) ∈ (ran ℎ ∪ {∅})
119		eqid 2731	. . . . . . . . . 10 ⊢ (𝑥 ∈ ω ↦ (ℎ‘𝑥)) = (𝑥 ∈ ω ↦ (ℎ‘𝑥))
120	119	fmpt 7049	. . . . . . . . 9 ⊢ (∀𝑥 ∈ ω (ℎ‘𝑥) ∈ (ran ℎ ∪ {∅}) ↔ (𝑥 ∈ ω ↦ (ℎ‘𝑥)):ω⟶(ran ℎ ∪ {∅}))
121	118, 120	mpbi 230	. . . . . . . 8 ⊢ (𝑥 ∈ ω ↦ (ℎ‘𝑥)):ω⟶(ran ℎ ∪ {∅})
122		dcomex 10344	. . . . . . . 8 ⊢ ω ∈ V
123		vex 3440	. . . . . . . . . 10 ⊢ ℎ ∈ V
124	123	rnex 7846	. . . . . . . . 9 ⊢ ran ℎ ∈ V
125	124, 48	unex 7683	. . . . . . . 8 ⊢ (ran ℎ ∪ {∅}) ∈ V
126		fex2 7872	. . . . . . . 8 ⊢ (((𝑥 ∈ ω ↦ (ℎ‘𝑥)):ω⟶(ran ℎ ∪ {∅}) ∧ ω ∈ V ∧ (ran ℎ ∪ {∅}) ∈ V) → (𝑥 ∈ ω ↦ (ℎ‘𝑥)) ∈ V)
127	121, 122, 125, 126	mp3an 1463	. . . . . . 7 ⊢ (𝑥 ∈ ω ↦ (ℎ‘𝑥)) ∈ V
128	90, 127	eqeltri 2827	. . . . . 6 ⊢ 𝐺 ∈ V
129		feq1 6635	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (𝑔:ω⟶𝐴 ↔ 𝐺:ω⟶𝐴))
130		fveq1 6827	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (𝑔‘suc 𝑘) = (𝐺‘suc 𝑘))
131		fveq1 6827	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → (𝑔‘𝑘) = (𝐺‘𝑘))
132	131	fveq2d 6832	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (𝐹‘(𝑔‘𝑘)) = (𝐹‘(𝐺‘𝑘)))
133	130, 132	eleq12d 2825	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → ((𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))
134	133	ralbidv 3155	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))
135	129, 134	anbi12d 632	. . . . . 6 ⊢ (𝑔 = 𝐺 → ((𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))) ↔ (𝐺:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))))
136	128, 135	spcev 3556	. . . . 5 ⊢ ((𝐺:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))
137	94, 116, 136	syl2anc 584	. . . 4 ⊢ ((∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))
138	137	ex 412	. . 3 ⊢ (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))))
139	138	exlimiv 1931	. 2 ⊢ (∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))))
140	74, 75, 139	sylc 65	1 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2111  {cab 2709   ≠ wne 2928  ∀wral 3047  {crab 3395  Vcvv 3436   ∖ cdif 3894   ∪ cun 3895   ⊆ wss 3897  ∅c0 4282  𝒫 cpw 4549  {csn 4575  ∪ cuni 4858   class class class wbr 5093  {copab 5155   ↦ cmpt 5174   × cxp 5617  dom cdm 5619  ran crn 5620  suc csuc 6314  ⟶wf 6483  ‘cfv 6487  ωcom 7802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-dc 10343

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-tr 5201  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-ord 6315  df-on 6316  df-lim 6317  df-suc 6318  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-fv 6495  df-om 7803  df-1o 8391

This theorem is referenced by:  axdc2  10346