Theorem axdc2lem 10204

Description: Lemma for axdc2 10205. We construct a relation 𝑅 based on 𝐹 such that 𝑥𝑅𝑦 iff 𝑦 ∈ (𝐹‘𝑥), and show that the "function" described by ax-dc 10202 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 5813	. . . . . . 7 ⊢ dom 𝑅 = dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
3		19.42v 1957	. . . . . . . . 9 ⊢ (∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)))
4	3	abbii 2808	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))}
5		dmopab 5824	. . . . . . . 8 ⊢ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
6		df-rab 3073	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))}
7	4, 5, 6	3eqtr4i 2776	. . . . . . 7 ⊢ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)}
8	2, 7	eqtri 2766	. . . . . 6 ⊢ dom 𝑅 = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)}
9		ffvelrn 6959	. . . . . . . . 9 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}))
10		eldifsni 4723	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹‘𝑥) ≠ ∅)
11		n0 4280	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))
12	10, 11	sylib 217	. . . . . . . . 9 ⊢ ((𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → ∃𝑦 𝑦 ∈ (𝐹‘𝑥))
13	9, 12	syl 17	. . . . . . . 8 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝐴) → ∃𝑦 𝑦 ∈ (𝐹‘𝑥))
14	13	ralrimiva 3103	. . . . . . 7 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 ∈ (𝐹‘𝑥))
15		rabid2 3314	. . . . . . 7 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 ∈ (𝐹‘𝑥))
16	14, 15	sylibr 233	. . . . . 6 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → 𝐴 = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)})
17	8, 16	eqtr4id 2797	. . . . 5 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → dom 𝑅 = 𝐴)
18	17	neeq1d 3003	. . . 4 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (dom 𝑅 ≠ ∅ ↔ 𝐴 ≠ ∅))
19	18	biimparc 480	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → dom 𝑅 ≠ ∅)
20		eldifi 4061	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹‘𝑥) ∈ 𝒫 𝐴)
21		elelpwi 4545	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (𝐹‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝒫 𝐴) → 𝑦 ∈ 𝐴)
22	21	expcom 414	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ∈ 𝒫 𝐴 → (𝑦 ∈ (𝐹‘𝑥) → 𝑦 ∈ 𝐴))
23	9, 20, 22	3syl 18	. . . . . . . . 9 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝐹‘𝑥) → 𝑦 ∈ 𝐴))
24	23	expimpd 454	. . . . . . . 8 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴))
25	24	exlimdv 1936	. . . . . . 7 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴))
26	25	alrimiv 1930	. . . . . 6 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑦(∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴))
27	1	rneqi 5846	. . . . . . . . 9 ⊢ ran 𝑅 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
28		rnopab 5863	. . . . . . . . 9 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
29	27, 28	eqtri 2766	. . . . . . . 8 ⊢ ran 𝑅 = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
30	29	sseq1i 3949	. . . . . . 7 ⊢ (ran 𝑅 ⊆ 𝐴 ↔ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ⊆ 𝐴)
31		abss 3994	. . . . . . 7 ⊢ ({𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ⊆ 𝐴 ↔ ∀𝑦(∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴))
32	30, 31	bitri 274	. . . . . 6 ⊢ (ran 𝑅 ⊆ 𝐴 ↔ ∀𝑦(∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴))
33	26, 32	sylibr 233	. . . . 5 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝑅 ⊆ 𝐴)
34	33, 17	sseqtrrd 3962	. . . 4 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝑅 ⊆ dom 𝑅)
35	34	adantl 482	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝑅 ⊆ dom 𝑅)
36		fvrn0 6802	. . . . . . . . . 10 ⊢ (𝐹‘𝑥) ∈ (ran 𝐹 ∪ {∅})
37		elssuni 4871	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ∈ (ran 𝐹 ∪ {∅}) → (𝐹‘𝑥) ⊆ ∪ (ran 𝐹 ∪ {∅}))
38	36, 37	ax-mp 5	. . . . . . . . 9 ⊢ (𝐹‘𝑥) ⊆ ∪ (ran 𝐹 ∪ {∅})
39	38	sseli 3917	. . . . . . . 8 ⊢ (𝑦 ∈ (𝐹‘𝑥) → 𝑦 ∈ ∪ (ran 𝐹 ∪ {∅}))
40	39	anim2i 617	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∪ (ran 𝐹 ∪ {∅})))
41	40	ssopab2i 5463	. . . . . 6 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∪ (ran 𝐹 ∪ {∅}))}
42		df-xp 5595	. . . . . 6 ⊢ (𝐴 × ∪ (ran 𝐹 ∪ {∅})) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∪ (ran 𝐹 ∪ {∅}))}
43	41, 1, 42	3sstr4i 3964	. . . . 5 ⊢ 𝑅 ⊆ (𝐴 × ∪ (ran 𝐹 ∪ {∅}))
44		axdc2lem.1	. . . . . 6 ⊢ 𝐴 ∈ V
45		frn 6607	. . . . . . . . . 10 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}))
46	45	adantl 482	. . . . . . . . 9 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}))
47	44	pwex 5303	. . . . . . . . . . 11 ⊢ 𝒫 𝐴 ∈ V
48	47	difexi 5252	. . . . . . . . . 10 ⊢ (𝒫 𝐴 ∖ {∅}) ∈ V
49	48	ssex 5245	. . . . . . . . 9 ⊢ (ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}) → ran 𝐹 ∈ V)
50	46, 49	syl 17	. . . . . . . 8 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝐹 ∈ V)
51		p0ex 5307	. . . . . . . 8 ⊢ {∅} ∈ V
52		unexg 7599	. . . . . . . 8 ⊢ ((ran 𝐹 ∈ V ∧ {∅} ∈ V) → (ran 𝐹 ∪ {∅}) ∈ V)
53	50, 51, 52	sylancl 586	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (ran 𝐹 ∪ {∅}) ∈ V)
54	53	uniexd 7595	. . . . . 6 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∪ (ran 𝐹 ∪ {∅}) ∈ V)
55		xpexg 7600	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ ∪ (ran 𝐹 ∪ {∅}) ∈ V) → (𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∈ V)
56	44, 54, 55	sylancr 587	. . . . 5 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∈ V)
57		ssexg 5247	. . . . 5 ⊢ ((𝑅 ⊆ (𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∧ (𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∈ V) → 𝑅 ∈ V)
58	43, 56, 57	sylancr 587	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝑅 ∈ V)
59		n0 4280	. . . . . . . . 9 ⊢ (dom 𝑟 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ dom 𝑟)
60		vex 3436	. . . . . . . . . . 11 ⊢ 𝑥 ∈ V
61	60	eldm 5809	. . . . . . . . . 10 ⊢ (𝑥 ∈ dom 𝑟 ↔ ∃𝑦 𝑥𝑟𝑦)
62	61	exbii 1850	. . . . . . . . 9 ⊢ (∃𝑥 𝑥 ∈ dom 𝑟 ↔ ∃𝑥∃𝑦 𝑥𝑟𝑦)
63	59, 62	bitr2i 275	. . . . . . . 8 ⊢ (∃𝑥∃𝑦 𝑥𝑟𝑦 ↔ dom 𝑟 ≠ ∅)
64		dmeq 5812	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → dom 𝑟 = dom 𝑅)
65	64	neeq1d 3003	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (dom 𝑟 ≠ ∅ ↔ dom 𝑅 ≠ ∅))
66	63, 65	bitrid 282	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (∃𝑥∃𝑦 𝑥𝑟𝑦 ↔ dom 𝑅 ≠ ∅))
67		rneq 5845	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → ran 𝑟 = ran 𝑅)
68	67, 64	sseq12d 3954	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (ran 𝑟 ⊆ dom 𝑟 ↔ ran 𝑅 ⊆ dom 𝑅))
69	66, 68	anbi12d 631	. . . . . 6 ⊢ (𝑟 = 𝑅 → ((∃𝑥∃𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) ↔ (dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅)))
70		breq 5076	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → ((ℎ‘𝑘)𝑟(ℎ‘suc 𝑘) ↔ (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
71	70	ralbidv 3112	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘) ↔ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
72	71	exbidv 1924	. . . . . 6 ⊢ (𝑟 = 𝑅 → (∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘) ↔ ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
73	69, 72	imbi12d 345	. . . . 5 ⊢ (𝑟 = 𝑅 → (((∃𝑥∃𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘)) ↔ ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))))
74		ax-dc 10202	. . . . 5 ⊢ ((∃𝑥∃𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘))
75	73, 74	vtoclg 3505	. . . 4 ⊢ (𝑅 ∈ V → ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
76	58, 75	syl 17	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
77	19, 35, 76	mp2and 696	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))
78		simpr 485	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}))
79		fveq2 6774	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → (ℎ‘𝑘) = (ℎ‘𝑥))
80		suceq 6331	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑥 → suc 𝑘 = suc 𝑥)
81	80	fveq2d 6778	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑥))
82	79, 81	breq12d 5087	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → ((ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ↔ (ℎ‘𝑥)𝑅(ℎ‘suc 𝑥)))
83	82	rspccv 3558	. . . . . . . . . . . . 13 ⊢ (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝑥 ∈ ω → (ℎ‘𝑥)𝑅(ℎ‘suc 𝑥)))
84		fvex 6787	. . . . . . . . . . . . . 14 ⊢ (ℎ‘𝑥) ∈ V
85		fvex 6787	. . . . . . . . . . . . . 14 ⊢ (ℎ‘suc 𝑥) ∈ V
86	84, 85	breldm 5817	. . . . . . . . . . . . 13 ⊢ ((ℎ‘𝑥)𝑅(ℎ‘suc 𝑥) → (ℎ‘𝑥) ∈ dom 𝑅)
87	83, 86	syl6 35	. . . . . . . . . . . 12 ⊢ (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝑥 ∈ ω → (ℎ‘𝑥) ∈ dom 𝑅))
88	87	imp 407	. . . . . . . . . . 11 ⊢ ((∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝑥 ∈ ω) → (ℎ‘𝑥) ∈ dom 𝑅)
89	88	adantll 711	. . . . . . . . . 10 ⊢ (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) ∧ 𝑥 ∈ ω) → (ℎ‘𝑥) ∈ dom 𝑅)
90		eleq2 2827	. . . . . . . . . . 11 ⊢ (dom 𝑅 = 𝐴 → ((ℎ‘𝑥) ∈ dom 𝑅 ↔ (ℎ‘𝑥) ∈ 𝐴))
91	90	ad2antrr 723	. . . . . . . . . 10 ⊢ (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) ∧ 𝑥 ∈ ω) → ((ℎ‘𝑥) ∈ dom 𝑅 ↔ (ℎ‘𝑥) ∈ 𝐴))
92	89, 91	mpbid 231	. . . . . . . . 9 ⊢ (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) ∧ 𝑥 ∈ ω) → (ℎ‘𝑥) ∈ 𝐴)
93		axdc2lem.3	. . . . . . . . 9 ⊢ 𝐺 = (𝑥 ∈ ω ↦ (ℎ‘𝑥))
94	92, 93	fmptd 6988	. . . . . . . 8 ⊢ ((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) → 𝐺:ω⟶𝐴)
95	94	ex 413	. . . . . . 7 ⊢ (dom 𝑅 = 𝐴 → (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → 𝐺:ω⟶𝐴))
96	17, 95	syl 17	. . . . . 6 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → 𝐺:ω⟶𝐴))
97	96	impcom 408	. . . . 5 ⊢ ((∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝐺:ω⟶𝐴)
98		fveq2 6774	. . . . . . . . . 10 ⊢ (𝑥 = 𝑘 → (ℎ‘𝑥) = (ℎ‘𝑘))
99		fvex 6787	. . . . . . . . . 10 ⊢ (ℎ‘𝑘) ∈ V
100	98, 93, 99	fvmpt 6875	. . . . . . . . 9 ⊢ (𝑘 ∈ ω → (𝐺‘𝑘) = (ℎ‘𝑘))
101		peano2 7737	. . . . . . . . . 10 ⊢ (𝑘 ∈ ω → suc 𝑘 ∈ ω)
102		fvex 6787	. . . . . . . . . 10 ⊢ (ℎ‘suc 𝑘) ∈ V
103		fveq2 6774	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑘 → (ℎ‘𝑥) = (ℎ‘suc 𝑘))
104	103, 93	fvmptg 6873	. . . . . . . . . 10 ⊢ ((suc 𝑘 ∈ ω ∧ (ℎ‘suc 𝑘) ∈ V) → (𝐺‘suc 𝑘) = (ℎ‘suc 𝑘))
105	101, 102, 104	sylancl 586	. . . . . . . . 9 ⊢ (𝑘 ∈ ω → (𝐺‘suc 𝑘) = (ℎ‘suc 𝑘))
106	100, 105	breq12d 5087	. . . . . . . 8 ⊢ (𝑘 ∈ ω → ((𝐺‘𝑘)𝑅(𝐺‘suc 𝑘) ↔ (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
107		fvex 6787	. . . . . . . . . 10 ⊢ (𝐺‘𝑘) ∈ V
108		fvex 6787	. . . . . . . . . 10 ⊢ (𝐺‘suc 𝑘) ∈ V
109		eleq1 2826	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐺‘𝑘) → (𝑥 ∈ 𝐴 ↔ (𝐺‘𝑘) ∈ 𝐴))
110		fveq2 6774	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐺‘𝑘) → (𝐹‘𝑥) = (𝐹‘(𝐺‘𝑘)))
111	110	eleq2d 2824	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐺‘𝑘) → (𝑦 ∈ (𝐹‘𝑥) ↔ 𝑦 ∈ (𝐹‘(𝐺‘𝑘))))
112	109, 111	anbi12d 631	. . . . . . . . . 10 ⊢ (𝑥 = (𝐺‘𝑘) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) ↔ ((𝐺‘𝑘) ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘(𝐺‘𝑘)))))
113		eleq1 2826	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐺‘suc 𝑘) → (𝑦 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))
114	113	anbi2d 629	. . . . . . . . . 10 ⊢ (𝑦 = (𝐺‘suc 𝑘) → (((𝐺‘𝑘) ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘(𝐺‘𝑘))) ↔ ((𝐺‘𝑘) ∈ 𝐴 ∧ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))))
115	107, 108, 112, 114, 1	brab 5456	. . . . . . . . 9 ⊢ ((𝐺‘𝑘)𝑅(𝐺‘suc 𝑘) ↔ ((𝐺‘𝑘) ∈ 𝐴 ∧ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))
116	115	simprbi 497	. . . . . . . 8 ⊢ ((𝐺‘𝑘)𝑅(𝐺‘suc 𝑘) → (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))
117	106, 116	syl6bir 253	. . . . . . 7 ⊢ (𝑘 ∈ ω → ((ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))
118	117	ralimia 3085	. . . . . 6 ⊢ (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))
119	118	adantr 481	. . . . 5 ⊢ ((∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))
120		fvrn0 6802	. . . . . . . . . 10 ⊢ (ℎ‘𝑥) ∈ (ran ℎ ∪ {∅})
121	120	rgenw 3076	. . . . . . . . 9 ⊢ ∀𝑥 ∈ ω (ℎ‘𝑥) ∈ (ran ℎ ∪ {∅})
122		eqid 2738	. . . . . . . . . 10 ⊢ (𝑥 ∈ ω ↦ (ℎ‘𝑥)) = (𝑥 ∈ ω ↦ (ℎ‘𝑥))
123	122	fmpt 6984	. . . . . . . . 9 ⊢ (∀𝑥 ∈ ω (ℎ‘𝑥) ∈ (ran ℎ ∪ {∅}) ↔ (𝑥 ∈ ω ↦ (ℎ‘𝑥)):ω⟶(ran ℎ ∪ {∅}))
124	121, 123	mpbi 229	. . . . . . . 8 ⊢ (𝑥 ∈ ω ↦ (ℎ‘𝑥)):ω⟶(ran ℎ ∪ {∅})
125		dcomex 10203	. . . . . . . 8 ⊢ ω ∈ V
126		vex 3436	. . . . . . . . . 10 ⊢ ℎ ∈ V
127	126	rnex 7759	. . . . . . . . 9 ⊢ ran ℎ ∈ V
128	127, 51	unex 7596	. . . . . . . 8 ⊢ (ran ℎ ∪ {∅}) ∈ V
129		fex2 7780	. . . . . . . 8 ⊢ (((𝑥 ∈ ω ↦ (ℎ‘𝑥)):ω⟶(ran ℎ ∪ {∅}) ∧ ω ∈ V ∧ (ran ℎ ∪ {∅}) ∈ V) → (𝑥 ∈ ω ↦ (ℎ‘𝑥)) ∈ V)
130	124, 125, 128, 129	mp3an 1460	. . . . . . 7 ⊢ (𝑥 ∈ ω ↦ (ℎ‘𝑥)) ∈ V
131	93, 130	eqeltri 2835	. . . . . 6 ⊢ 𝐺 ∈ V
132		feq1 6581	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (𝑔:ω⟶𝐴 ↔ 𝐺:ω⟶𝐴))
133		fveq1 6773	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (𝑔‘suc 𝑘) = (𝐺‘suc 𝑘))
134		fveq1 6773	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → (𝑔‘𝑘) = (𝐺‘𝑘))
135	134	fveq2d 6778	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (𝐹‘(𝑔‘𝑘)) = (𝐹‘(𝐺‘𝑘)))
136	133, 135	eleq12d 2833	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → ((𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))
137	136	ralbidv 3112	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))
138	132, 137	anbi12d 631	. . . . . 6 ⊢ (𝑔 = 𝐺 → ((𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))) ↔ (𝐺:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))))
139	131, 138	spcev 3545	. . . . 5 ⊢ ((𝐺:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))
140	97, 119, 139	syl2anc 584	. . . 4 ⊢ ((∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))
141	140	ex 413	. . 3 ⊢ (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))))
142	141	exlimiv 1933	. 2 ⊢ (∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))))
143	77, 78, 142	sylc 65	1 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1537   = wceq 1539  ∃wex 1782   ∈ wcel 2106  {cab 2715   ≠ wne 2943  ∀wral 3064  {crab 3068  Vcvv 3432   ∖ cdif 3884   ∪ cun 3885   ⊆ wss 3887  ∅c0 4256  𝒫 cpw 4533  {csn 4561  ∪ cuni 4839   class class class wbr 5074  {copab 5136   ↦ cmpt 5157   × cxp 5587  dom cdm 5589  ran crn 5590  suc csuc 6268  ⟶wf 6429  ‘cfv 6433  ωcom 7712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-dc 10202

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-fv 6441  df-om 7713  df-1o 8297

This theorem is referenced by:  axdc2  10205