Theorem axdc2lem 10443

Description: Lemma for axdc2 10444. We construct a relation 𝑅 based on 𝐹 such that 𝑥𝑅𝑦 iff 𝑦 ∈ (𝐹‘𝑥), and show that the "function" described by ax-dc 10441 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 5905	. . . . . . 7 ⊢ dom 𝑅 = dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
3		19.42v 1958	. . . . . . . . 9 ⊢ (∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)))
4	3	abbii 2803	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))}
5		dmopab 5916	. . . . . . . 8 ⊢ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
6		df-rab 3434	. . . . . . . 8 ⊢ {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))}
7	4, 5, 6	3eqtr4i 2771	. . . . . . 7 ⊢ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)}
8	2, 7	eqtri 2761	. . . . . 6 ⊢ dom 𝑅 = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)}
9		ffvelcdm 7084	. . . . . . . . 9 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}))
10		eldifsni 4794	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹‘𝑥) ≠ ∅)
11		n0 4347	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝐹‘𝑥))
12	10, 11	sylib 217	. . . . . . . . 9 ⊢ ((𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → ∃𝑦 𝑦 ∈ (𝐹‘𝑥))
13	9, 12	syl 17	. . . . . . . 8 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝐴) → ∃𝑦 𝑦 ∈ (𝐹‘𝑥))
14	13	ralrimiva 3147	. . . . . . 7 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 ∈ (𝐹‘𝑥))
15		rabid2 3465	. . . . . . 7 ⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)} ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 ∈ (𝐹‘𝑥))
16	14, 15	sylibr 233	. . . . . 6 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → 𝐴 = {𝑥 ∈ 𝐴 ∣ ∃𝑦 𝑦 ∈ (𝐹‘𝑥)})
17	8, 16	eqtr4id 2792	. . . . 5 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → dom 𝑅 = 𝐴)
18	17	neeq1d 3001	. . . 4 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (dom 𝑅 ≠ ∅ ↔ 𝐴 ≠ ∅))
19	18	biimparc 481	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → dom 𝑅 ≠ ∅)
20		eldifi 4127	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ∈ (𝒫 𝐴 ∖ {∅}) → (𝐹‘𝑥) ∈ 𝒫 𝐴)
21		elelpwi 4613	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ (𝐹‘𝑥) ∧ (𝐹‘𝑥) ∈ 𝒫 𝐴) → 𝑦 ∈ 𝐴)
22	21	expcom 415	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ∈ 𝒫 𝐴 → (𝑦 ∈ (𝐹‘𝑥) → 𝑦 ∈ 𝐴))
23	9, 20, 22	3syl 18	. . . . . . . . 9 ⊢ ((𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ (𝐹‘𝑥) → 𝑦 ∈ 𝐴))
24	23	expimpd 455	. . . . . . . 8 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴))
25	24	exlimdv 1937	. . . . . . 7 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴))
26	25	alrimiv 1931	. . . . . 6 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∀𝑦(∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴))
27	1	rneqi 5937	. . . . . . . . 9 ⊢ ran 𝑅 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
28		rnopab 5954	. . . . . . . . 9 ⊢ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
29	27, 28	eqtri 2761	. . . . . . . 8 ⊢ ran 𝑅 = {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))}
30	29	sseq1i 4011	. . . . . . 7 ⊢ (ran 𝑅 ⊆ 𝐴 ↔ {𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ⊆ 𝐴)
31		abss 4058	. . . . . . 7 ⊢ ({𝑦 ∣ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ⊆ 𝐴 ↔ ∀𝑦(∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴))
32	30, 31	bitri 275	. . . . . 6 ⊢ (ran 𝑅 ⊆ 𝐴 ↔ ∀𝑦(∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → 𝑦 ∈ 𝐴))
33	26, 32	sylibr 233	. . . . 5 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝑅 ⊆ 𝐴)
34	33, 17	sseqtrrd 4024	. . . 4 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝑅 ⊆ dom 𝑅)
35	34	adantl 483	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝑅 ⊆ dom 𝑅)
36		fvrn0 6922	. . . . . . . . . 10 ⊢ (𝐹‘𝑥) ∈ (ran 𝐹 ∪ {∅})
37		elssuni 4942	. . . . . . . . . 10 ⊢ ((𝐹‘𝑥) ∈ (ran 𝐹 ∪ {∅}) → (𝐹‘𝑥) ⊆ ∪ (ran 𝐹 ∪ {∅}))
38	36, 37	ax-mp 5	. . . . . . . . 9 ⊢ (𝐹‘𝑥) ⊆ ∪ (ran 𝐹 ∪ {∅})
39	38	sseli 3979	. . . . . . . 8 ⊢ (𝑦 ∈ (𝐹‘𝑥) → 𝑦 ∈ ∪ (ran 𝐹 ∪ {∅}))
40	39	anim2i 618	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∪ (ran 𝐹 ∪ {∅})))
41	40	ssopab2i 5551	. . . . . 6 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∪ (ran 𝐹 ∪ {∅}))}
42		df-xp 5683	. . . . . 6 ⊢ (𝐴 × ∪ (ran 𝐹 ∪ {∅})) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ∪ (ran 𝐹 ∪ {∅}))}
43	41, 1, 42	3sstr4i 4026	. . . . 5 ⊢ 𝑅 ⊆ (𝐴 × ∪ (ran 𝐹 ∪ {∅}))
44		axdc2lem.1	. . . . . 6 ⊢ 𝐴 ∈ V
45		frn 6725	. . . . . . . . . 10 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}))
46	45	adantl 483	. . . . . . . . 9 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}))
47	44	pwex 5379	. . . . . . . . . . 11 ⊢ 𝒫 𝐴 ∈ V
48	47	difexi 5329	. . . . . . . . . 10 ⊢ (𝒫 𝐴 ∖ {∅}) ∈ V
49	48	ssex 5322	. . . . . . . . 9 ⊢ (ran 𝐹 ⊆ (𝒫 𝐴 ∖ {∅}) → ran 𝐹 ∈ V)
50	46, 49	syl 17	. . . . . . . 8 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ran 𝐹 ∈ V)
51		p0ex 5383	. . . . . . . 8 ⊢ {∅} ∈ V
52		unexg 7736	. . . . . . . 8 ⊢ ((ran 𝐹 ∈ V ∧ {∅} ∈ V) → (ran 𝐹 ∪ {∅}) ∈ V)
53	50, 51, 52	sylancl 587	. . . . . . 7 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (ran 𝐹 ∪ {∅}) ∈ V)
54	53	uniexd 7732	. . . . . 6 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∪ (ran 𝐹 ∪ {∅}) ∈ V)
55		xpexg 7737	. . . . . 6 ⊢ ((𝐴 ∈ V ∧ ∪ (ran 𝐹 ∪ {∅}) ∈ V) → (𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∈ V)
56	44, 54, 55	sylancr 588	. . . . 5 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → (𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∈ V)
57		ssexg 5324	. . . . 5 ⊢ ((𝑅 ⊆ (𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∧ (𝐴 × ∪ (ran 𝐹 ∪ {∅})) ∈ V) → 𝑅 ∈ V)
58	43, 56, 57	sylancr 588	. . . 4 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝑅 ∈ V)
59		n0 4347	. . . . . . . . 9 ⊢ (dom 𝑟 ≠ ∅ ↔ ∃𝑥 𝑥 ∈ dom 𝑟)
60		vex 3479	. . . . . . . . . . 11 ⊢ 𝑥 ∈ V
61	60	eldm 5901	. . . . . . . . . 10 ⊢ (𝑥 ∈ dom 𝑟 ↔ ∃𝑦 𝑥𝑟𝑦)
62	61	exbii 1851	. . . . . . . . 9 ⊢ (∃𝑥 𝑥 ∈ dom 𝑟 ↔ ∃𝑥∃𝑦 𝑥𝑟𝑦)
63	59, 62	bitr2i 276	. . . . . . . 8 ⊢ (∃𝑥∃𝑦 𝑥𝑟𝑦 ↔ dom 𝑟 ≠ ∅)
64		dmeq 5904	. . . . . . . . 9 ⊢ (𝑟 = 𝑅 → dom 𝑟 = dom 𝑅)
65	64	neeq1d 3001	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → (dom 𝑟 ≠ ∅ ↔ dom 𝑅 ≠ ∅))
66	63, 65	bitrid 283	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (∃𝑥∃𝑦 𝑥𝑟𝑦 ↔ dom 𝑅 ≠ ∅))
67		rneq 5936	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → ran 𝑟 = ran 𝑅)
68	67, 64	sseq12d 4016	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (ran 𝑟 ⊆ dom 𝑟 ↔ ran 𝑅 ⊆ dom 𝑅))
69	66, 68	anbi12d 632	. . . . . 6 ⊢ (𝑟 = 𝑅 → ((∃𝑥∃𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) ↔ (dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅)))
70		breq 5151	. . . . . . . 8 ⊢ (𝑟 = 𝑅 → ((ℎ‘𝑘)𝑟(ℎ‘suc 𝑘) ↔ (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
71	70	ralbidv 3178	. . . . . . 7 ⊢ (𝑟 = 𝑅 → (∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘) ↔ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
72	71	exbidv 1925	. . . . . 6 ⊢ (𝑟 = 𝑅 → (∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘) ↔ ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
73	69, 72	imbi12d 345	. . . . 5 ⊢ (𝑟 = 𝑅 → (((∃𝑥∃𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘)) ↔ ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))))
74		ax-dc 10441	. . . . 5 ⊢ ((∃𝑥∃𝑦 𝑥𝑟𝑦 ∧ ran 𝑟 ⊆ dom 𝑟) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑟(ℎ‘suc 𝑘))
75	73, 74	vtoclg 3557	. . . 4 ⊢ (𝑅 ∈ V → ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
76	58, 75	syl 17	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ((dom 𝑅 ≠ ∅ ∧ ran 𝑅 ⊆ dom 𝑅) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
77	19, 35, 76	mp2and 698	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘))
78		simpr 486	. 2 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}))
79		fveq2 6892	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → (ℎ‘𝑘) = (ℎ‘𝑥))
80		suceq 6431	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 = 𝑥 → suc 𝑘 = suc 𝑥)
81	80	fveq2d 6896	. . . . . . . . . . . . . . 15 ⊢ (𝑘 = 𝑥 → (ℎ‘suc 𝑘) = (ℎ‘suc 𝑥))
82	79, 81	breq12d 5162	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑥 → ((ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ↔ (ℎ‘𝑥)𝑅(ℎ‘suc 𝑥)))
83	82	rspccv 3610	. . . . . . . . . . . . 13 ⊢ (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝑥 ∈ ω → (ℎ‘𝑥)𝑅(ℎ‘suc 𝑥)))
84		fvex 6905	. . . . . . . . . . . . . 14 ⊢ (ℎ‘𝑥) ∈ V
85		fvex 6905	. . . . . . . . . . . . . 14 ⊢ (ℎ‘suc 𝑥) ∈ V
86	84, 85	breldm 5909	. . . . . . . . . . . . 13 ⊢ ((ℎ‘𝑥)𝑅(ℎ‘suc 𝑥) → (ℎ‘𝑥) ∈ dom 𝑅)
87	83, 86	syl6 35	. . . . . . . . . . . 12 ⊢ (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝑥 ∈ ω → (ℎ‘𝑥) ∈ dom 𝑅))
88	87	imp 408	. . . . . . . . . . 11 ⊢ ((∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝑥 ∈ ω) → (ℎ‘𝑥) ∈ dom 𝑅)
89	88	adantll 713	. . . . . . . . . 10 ⊢ (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) ∧ 𝑥 ∈ ω) → (ℎ‘𝑥) ∈ dom 𝑅)
90		eleq2 2823	. . . . . . . . . . 11 ⊢ (dom 𝑅 = 𝐴 → ((ℎ‘𝑥) ∈ dom 𝑅 ↔ (ℎ‘𝑥) ∈ 𝐴))
91	90	ad2antrr 725	. . . . . . . . . 10 ⊢ (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) ∧ 𝑥 ∈ ω) → ((ℎ‘𝑥) ∈ dom 𝑅 ↔ (ℎ‘𝑥) ∈ 𝐴))
92	89, 91	mpbid 231	. . . . . . . . 9 ⊢ (((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) ∧ 𝑥 ∈ ω) → (ℎ‘𝑥) ∈ 𝐴)
93		axdc2lem.3	. . . . . . . . 9 ⊢ 𝐺 = (𝑥 ∈ ω ↦ (ℎ‘𝑥))
94	92, 93	fmptd 7114	. . . . . . . 8 ⊢ ((dom 𝑅 = 𝐴 ∧ ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)) → 𝐺:ω⟶𝐴)
95	94	ex 414	. . . . . . 7 ⊢ (dom 𝑅 = 𝐴 → (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → 𝐺:ω⟶𝐴))
96	17, 95	syl 17	. . . . . 6 ⊢ (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → 𝐺:ω⟶𝐴))
97	96	impcom 409	. . . . 5 ⊢ ((∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → 𝐺:ω⟶𝐴)
98		fveq2 6892	. . . . . . . . . 10 ⊢ (𝑥 = 𝑘 → (ℎ‘𝑥) = (ℎ‘𝑘))
99		fvex 6905	. . . . . . . . . 10 ⊢ (ℎ‘𝑘) ∈ V
100	98, 93, 99	fvmpt 6999	. . . . . . . . 9 ⊢ (𝑘 ∈ ω → (𝐺‘𝑘) = (ℎ‘𝑘))
101		peano2 7881	. . . . . . . . . 10 ⊢ (𝑘 ∈ ω → suc 𝑘 ∈ ω)
102		fvex 6905	. . . . . . . . . 10 ⊢ (ℎ‘suc 𝑘) ∈ V
103		fveq2 6892	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑘 → (ℎ‘𝑥) = (ℎ‘suc 𝑘))
104	103, 93	fvmptg 6997	. . . . . . . . . 10 ⊢ ((suc 𝑘 ∈ ω ∧ (ℎ‘suc 𝑘) ∈ V) → (𝐺‘suc 𝑘) = (ℎ‘suc 𝑘))
105	101, 102, 104	sylancl 587	. . . . . . . . 9 ⊢ (𝑘 ∈ ω → (𝐺‘suc 𝑘) = (ℎ‘suc 𝑘))
106	100, 105	breq12d 5162	. . . . . . . 8 ⊢ (𝑘 ∈ ω → ((𝐺‘𝑘)𝑅(𝐺‘suc 𝑘) ↔ (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘)))
107		fvex 6905	. . . . . . . . . 10 ⊢ (𝐺‘𝑘) ∈ V
108		fvex 6905	. . . . . . . . . 10 ⊢ (𝐺‘suc 𝑘) ∈ V
109		eleq1 2822	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐺‘𝑘) → (𝑥 ∈ 𝐴 ↔ (𝐺‘𝑘) ∈ 𝐴))
110		fveq2 6892	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝐺‘𝑘) → (𝐹‘𝑥) = (𝐹‘(𝐺‘𝑘)))
111	110	eleq2d 2820	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐺‘𝑘) → (𝑦 ∈ (𝐹‘𝑥) ↔ 𝑦 ∈ (𝐹‘(𝐺‘𝑘))))
112	109, 111	anbi12d 632	. . . . . . . . . 10 ⊢ (𝑥 = (𝐺‘𝑘) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘𝑥)) ↔ ((𝐺‘𝑘) ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘(𝐺‘𝑘)))))
113		eleq1 2822	. . . . . . . . . . 11 ⊢ (𝑦 = (𝐺‘suc 𝑘) → (𝑦 ∈ (𝐹‘(𝐺‘𝑘)) ↔ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))
114	113	anbi2d 630	. . . . . . . . . 10 ⊢ (𝑦 = (𝐺‘suc 𝑘) → (((𝐺‘𝑘) ∈ 𝐴 ∧ 𝑦 ∈ (𝐹‘(𝐺‘𝑘))) ↔ ((𝐺‘𝑘) ∈ 𝐴 ∧ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))))
115	107, 108, 112, 114, 1	brab 5544	. . . . . . . . 9 ⊢ ((𝐺‘𝑘)𝑅(𝐺‘suc 𝑘) ↔ ((𝐺‘𝑘) ∈ 𝐴 ∧ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))
116	115	simprbi 498	. . . . . . . 8 ⊢ ((𝐺‘𝑘)𝑅(𝐺‘suc 𝑘) → (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))
117	106, 116	syl6bir 254	. . . . . . 7 ⊢ (𝑘 ∈ ω → ((ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))
118	117	ralimia 3081	. . . . . 6 ⊢ (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))
119	118	adantr 482	. . . . 5 ⊢ ((∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))
120		fvrn0 6922	. . . . . . . . . 10 ⊢ (ℎ‘𝑥) ∈ (ran ℎ ∪ {∅})
121	120	rgenw 3066	. . . . . . . . 9 ⊢ ∀𝑥 ∈ ω (ℎ‘𝑥) ∈ (ran ℎ ∪ {∅})
122		eqid 2733	. . . . . . . . . 10 ⊢ (𝑥 ∈ ω ↦ (ℎ‘𝑥)) = (𝑥 ∈ ω ↦ (ℎ‘𝑥))
123	122	fmpt 7110	. . . . . . . . 9 ⊢ (∀𝑥 ∈ ω (ℎ‘𝑥) ∈ (ran ℎ ∪ {∅}) ↔ (𝑥 ∈ ω ↦ (ℎ‘𝑥)):ω⟶(ran ℎ ∪ {∅}))
124	121, 123	mpbi 229	. . . . . . . 8 ⊢ (𝑥 ∈ ω ↦ (ℎ‘𝑥)):ω⟶(ran ℎ ∪ {∅})
125		dcomex 10442	. . . . . . . 8 ⊢ ω ∈ V
126		vex 3479	. . . . . . . . . 10 ⊢ ℎ ∈ V
127	126	rnex 7903	. . . . . . . . 9 ⊢ ran ℎ ∈ V
128	127, 51	unex 7733	. . . . . . . 8 ⊢ (ran ℎ ∪ {∅}) ∈ V
129		fex2 7924	. . . . . . . 8 ⊢ (((𝑥 ∈ ω ↦ (ℎ‘𝑥)):ω⟶(ran ℎ ∪ {∅}) ∧ ω ∈ V ∧ (ran ℎ ∪ {∅}) ∈ V) → (𝑥 ∈ ω ↦ (ℎ‘𝑥)) ∈ V)
130	124, 125, 128, 129	mp3an 1462	. . . . . . 7 ⊢ (𝑥 ∈ ω ↦ (ℎ‘𝑥)) ∈ V
131	93, 130	eqeltri 2830	. . . . . 6 ⊢ 𝐺 ∈ V
132		feq1 6699	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (𝑔:ω⟶𝐴 ↔ 𝐺:ω⟶𝐴))
133		fveq1 6891	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (𝑔‘suc 𝑘) = (𝐺‘suc 𝑘))
134		fveq1 6891	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → (𝑔‘𝑘) = (𝐺‘𝑘))
135	134	fveq2d 6896	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → (𝐹‘(𝑔‘𝑘)) = (𝐹‘(𝐺‘𝑘)))
136	133, 135	eleq12d 2828	. . . . . . . 8 ⊢ (𝑔 = 𝐺 → ((𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))
137	136	ralbidv 3178	. . . . . . 7 ⊢ (𝑔 = 𝐺 → (∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)) ↔ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))))
138	132, 137	anbi12d 632	. . . . . 6 ⊢ (𝑔 = 𝐺 → ((𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))) ↔ (𝐺:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘)))))
139	131, 138	spcev 3597	. . . . 5 ⊢ ((𝐺:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝐺‘suc 𝑘) ∈ (𝐹‘(𝐺‘𝑘))) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))
140	97, 119, 139	syl2anc 585	. . . 4 ⊢ ((∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))
141	140	ex 414	. . 3 ⊢ (∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))))
142	141	exlimiv 1934	. 2 ⊢ (∃ℎ∀𝑘 ∈ ω (ℎ‘𝑘)𝑅(ℎ‘suc 𝑘) → (𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅}) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘)))))
143	77, 78, 142	sylc 65	1 ⊢ ((𝐴 ≠ ∅ ∧ 𝐹:𝐴⟶(𝒫 𝐴 ∖ {∅})) → ∃𝑔(𝑔:ω⟶𝐴 ∧ ∀𝑘 ∈ ω (𝑔‘suc 𝑘) ∈ (𝐹‘(𝑔‘𝑘))))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397  ∀wal 1540   = wceq 1542  ∃wex 1782   ∈ wcel 2107  {cab 2710   ≠ wne 2941  ∀wral 3062  {crab 3433  Vcvv 3475   ∖ cdif 3946   ∪ cun 3947   ⊆ wss 3949  ∅c0 4323  𝒫 cpw 4603  {csn 4629  ∪ cuni 4909   class class class wbr 5149  {copab 5211   ↦ cmpt 5232   × cxp 5675  dom cdm 5677  ran crn 5678  suc csuc 6367  ⟶wf 6540  ‘cfv 6544  ωcom 7855

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-dc 10441

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552  df-om 7856  df-1o 8466

This theorem is referenced by:  axdc2  10444