Theorem heiborlem3 37803

Description: Lemma for heibor 37811. Using countable choice ax-cc 10329, we have fixed in advance a collection of finite 2↑-𝑛 nets (𝐹‘𝑛) for 𝑋 (note that an 𝑟-net is a set of points in 𝑋 whose 𝑟 -balls cover 𝑋). The set 𝐺 is the subset of these points whose corresponding balls have no finite subcover (i.e. in the set 𝐾). If the theorem was false, then 𝑋 would be in 𝐾, and so some ball at each level would also be in 𝐾. But we can say more than this; given a ball (𝑦𝐵𝑛) on level 𝑛, since level 𝑛 + 1 covers the space and thus also (𝑦𝐵𝑛), using heiborlem1 37801 there is a ball on the next level whose intersection with (𝑦𝐵𝑛) also has no finite subcover. Now since the set 𝐺 is a countable union of finite sets, it is countable (which needs ax-cc 10329 via iunctb 10468), and so we can apply ax-cc 10329 to 𝐺 directly to get a function from 𝐺 to itself, which points from each ball in 𝐾 to a ball on the next level in 𝐾, and such that the intersection between these balls is also in 𝐾. (Contributed by Jeff Madsen, 18-Jan-2014.)

Hypotheses

Ref	Expression
heibor.1	⊢ 𝐽 = (MetOpen‘𝐷)
heibor.3	⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣}
heibor.4	⊢ 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}
heibor.5	⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))
heibor.6	⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))
heibor.7	⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))
heibor.8	⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛))

Assertion

Ref	Expression
heiborlem3	⊢ (𝜑 → ∃𝑔∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))

Distinct variable groups:   𝑥,𝑛,𝑦,𝑢,𝐹   𝑥,𝑔,𝐺   𝜑,𝑔,𝑥   𝑔,𝑚,𝑛,𝑢,𝑣,𝑦,𝑧,𝐷,𝑥   𝐵,𝑔,𝑛,𝑢,𝑣,𝑦   𝑔,𝐽,𝑚,𝑛,𝑢,𝑣,𝑥,𝑦,𝑧   𝑈,𝑔,𝑛,𝑢,𝑣,𝑥,𝑦,𝑧   𝑔,𝑋,𝑚,𝑛,𝑢,𝑣,𝑥,𝑦,𝑧   𝑔,𝐾,𝑛,𝑥,𝑦,𝑧   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑦,𝑧,𝑣,𝑢,𝑚,𝑛)   𝐵(𝑧,𝑚)   𝑈(𝑚)   𝐹(𝑧,𝑣,𝑔,𝑚)   𝐺(𝑦,𝑧,𝑣,𝑢,𝑚,𝑛)   𝐾(𝑣,𝑢,𝑚)

Proof of Theorem heiborlem3

Dummy variable 𝑡 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nn0ex 12390	. . . . . 6 ⊢ ℕ0 ∈ V
2		fvex 6835	. . . . . . 7 ⊢ (𝐹‘𝑡) ∈ V
3		vsnex 5373	. . . . . . 7 ⊢ {𝑡} ∈ V
4	2, 3	xpex 7689	. . . . . 6 ⊢ ((𝐹‘𝑡) × {𝑡}) ∈ V
5	1, 4	iunex 7903	. . . . 5 ⊢ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ∈ V
6		heibor.4	. . . . . . . . 9 ⊢ 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}
7	6	relopabiv 5763	. . . . . . . 8 ⊢ Rel 𝐺
8		1st2nd 7974	. . . . . . . 8 ⊢ ((Rel 𝐺 ∧ 𝑥 ∈ 𝐺) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
9	7, 8	mpan 690	. . . . . . 7 ⊢ (𝑥 ∈ 𝐺 → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
10	9	eleq1d 2813	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐺 → (𝑥 ∈ 𝐺 ↔ ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ 𝐺))
11		df-br 5093	. . . . . . . . . . 11 ⊢ ((1st ‘𝑥)𝐺(2nd ‘𝑥) ↔ ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ 𝐺)
12	10, 11	bitr4di 289	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐺 → (𝑥 ∈ 𝐺 ↔ (1st ‘𝑥)𝐺(2nd ‘𝑥)))
13		heibor.1	. . . . . . . . . . 11 ⊢ 𝐽 = (MetOpen‘𝐷)
14		heibor.3	. . . . . . . . . . 11 ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣}
15		fvex 6835	. . . . . . . . . . 11 ⊢ (1st ‘𝑥) ∈ V
16		fvex 6835	. . . . . . . . . . 11 ⊢ (2nd ‘𝑥) ∈ V
17	13, 14, 6, 15, 16	heiborlem2 37802	. . . . . . . . . 10 ⊢ ((1st ‘𝑥)𝐺(2nd ‘𝑥) ↔ ((2nd ‘𝑥) ∈ ℕ0 ∧ (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)) ∧ ((1st ‘𝑥)𝐵(2nd ‘𝑥)) ∈ 𝐾))
18	12, 17	bitrdi 287	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐺 → (𝑥 ∈ 𝐺 ↔ ((2nd ‘𝑥) ∈ ℕ0 ∧ (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)) ∧ ((1st ‘𝑥)𝐵(2nd ‘𝑥)) ∈ 𝐾)))
19	18	ibi 267	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐺 → ((2nd ‘𝑥) ∈ ℕ0 ∧ (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)) ∧ ((1st ‘𝑥)𝐵(2nd ‘𝑥)) ∈ 𝐾))
20	16	snid 4614	. . . . . . . . . . . 12 ⊢ (2nd ‘𝑥) ∈ {(2nd ‘𝑥)}
21		opelxp 5655	. . . . . . . . . . . 12 ⊢ (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ((𝐹‘(2nd ‘𝑥)) × {(2nd ‘𝑥)}) ↔ ((1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)) ∧ (2nd ‘𝑥) ∈ {(2nd ‘𝑥)}))
22	20, 21	mpbiran2 710	. . . . . . . . . . 11 ⊢ (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ((𝐹‘(2nd ‘𝑥)) × {(2nd ‘𝑥)}) ↔ (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)))
23		fveq2 6822	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (2nd ‘𝑥) → (𝐹‘𝑡) = (𝐹‘(2nd ‘𝑥)))
24		sneq 4587	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (2nd ‘𝑥) → {𝑡} = {(2nd ‘𝑥)})
25	23, 24	xpeq12d 5650	. . . . . . . . . . . . 13 ⊢ (𝑡 = (2nd ‘𝑥) → ((𝐹‘𝑡) × {𝑡}) = ((𝐹‘(2nd ‘𝑥)) × {(2nd ‘𝑥)}))
26	25	eleq2d 2814	. . . . . . . . . . . 12 ⊢ (𝑡 = (2nd ‘𝑥) → (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ((𝐹‘𝑡) × {𝑡}) ↔ ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ((𝐹‘(2nd ‘𝑥)) × {(2nd ‘𝑥)})))
27	26	rspcev 3577	. . . . . . . . . . 11 ⊢ (((2nd ‘𝑥) ∈ ℕ0 ∧ ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ((𝐹‘(2nd ‘𝑥)) × {(2nd ‘𝑥)})) → ∃𝑡 ∈ ℕ0 ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ((𝐹‘𝑡) × {𝑡}))
28	22, 27	sylan2br 595	. . . . . . . . . 10 ⊢ (((2nd ‘𝑥) ∈ ℕ0 ∧ (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥))) → ∃𝑡 ∈ ℕ0 ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ((𝐹‘𝑡) × {𝑡}))
29		eliun 4945	. . . . . . . . . 10 ⊢ (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ↔ ∃𝑡 ∈ ℕ0 ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ((𝐹‘𝑡) × {𝑡}))
30	28, 29	sylibr 234	. . . . . . . . 9 ⊢ (((2nd ‘𝑥) ∈ ℕ0 ∧ (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥))) → ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}))
31	30	3adant3 1132	. . . . . . . 8 ⊢ (((2nd ‘𝑥) ∈ ℕ0 ∧ (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)) ∧ ((1st ‘𝑥)𝐵(2nd ‘𝑥)) ∈ 𝐾) → ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}))
32	19, 31	syl 17	. . . . . . 7 ⊢ (𝑥 ∈ 𝐺 → ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}))
33	9, 32	eqeltrd 2828	. . . . . 6 ⊢ (𝑥 ∈ 𝐺 → 𝑥 ∈ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}))
34	33	ssriv 3939	. . . . 5 ⊢ 𝐺 ⊆ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡})
35		ssdomg 8925	. . . . 5 ⊢ (∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ∈ V → (𝐺 ⊆ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) → 𝐺 ≼ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡})))
36	5, 34, 35	mp2 9	. . . 4 ⊢ 𝐺 ≼ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡})
37		nn0ennn 13886	. . . . . . 7 ⊢ ℕ0 ≈ ℕ
38		nnenom 13887	. . . . . . 7 ⊢ ℕ ≈ ω
39	37, 38	entri 8933	. . . . . 6 ⊢ ℕ0 ≈ ω
40		endom 8904	. . . . . 6 ⊢ (ℕ0 ≈ ω → ℕ0 ≼ ω)
41	39, 40	ax-mp 5	. . . . 5 ⊢ ℕ0 ≼ ω
42		vex 3440	. . . . . . . 8 ⊢ 𝑡 ∈ V
43	2, 42	xpsnen 8978	. . . . . . 7 ⊢ ((𝐹‘𝑡) × {𝑡}) ≈ (𝐹‘𝑡)
44		inss2 4189	. . . . . . . . 9 ⊢ (𝒫 𝑋 ∩ Fin) ⊆ Fin
45		heibor.7	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))
46	45	ffvelcdmda 7018	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ ℕ0) → (𝐹‘𝑡) ∈ (𝒫 𝑋 ∩ Fin))
47	44, 46	sselid 3933	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ ℕ0) → (𝐹‘𝑡) ∈ Fin)
48		isfinite 9548	. . . . . . . . 9 ⊢ ((𝐹‘𝑡) ∈ Fin ↔ (𝐹‘𝑡) ≺ ω)
49		sdomdom 8905	. . . . . . . . 9 ⊢ ((𝐹‘𝑡) ≺ ω → (𝐹‘𝑡) ≼ ω)
50	48, 49	sylbi 217	. . . . . . . 8 ⊢ ((𝐹‘𝑡) ∈ Fin → (𝐹‘𝑡) ≼ ω)
51	47, 50	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ ℕ0) → (𝐹‘𝑡) ≼ ω)
52		endomtr 8937	. . . . . . 7 ⊢ ((((𝐹‘𝑡) × {𝑡}) ≈ (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≼ ω) → ((𝐹‘𝑡) × {𝑡}) ≼ ω)
53	43, 51, 52	sylancr 587	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ ℕ0) → ((𝐹‘𝑡) × {𝑡}) ≼ ω)
54	53	ralrimiva 3121	. . . . 5 ⊢ (𝜑 → ∀𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω)
55		iunctb 10468	. . . . 5 ⊢ ((ℕ0 ≼ ω ∧ ∀𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω) → ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω)
56	41, 54, 55	sylancr 587	. . . 4 ⊢ (𝜑 → ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω)
57		domtr 8932	. . . 4 ⊢ ((𝐺 ≼ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ∧ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω) → 𝐺 ≼ ω)
58	36, 56, 57	sylancr 587	. . 3 ⊢ (𝜑 → 𝐺 ≼ ω)
59	19	simp1d 1142	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐺 → (2nd ‘𝑥) ∈ ℕ0)
60		peano2nn0 12424	. . . . . . . . 9 ⊢ ((2nd ‘𝑥) ∈ ℕ0 → ((2nd ‘𝑥) + 1) ∈ ℕ0)
61	59, 60	syl 17	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐺 → ((2nd ‘𝑥) + 1) ∈ ℕ0)
62		ffvelcdm 7015	. . . . . . . 8 ⊢ ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧ ((2nd ‘𝑥) + 1) ∈ ℕ0) → (𝐹‘((2nd ‘𝑥) + 1)) ∈ (𝒫 𝑋 ∩ Fin))
63	45, 61, 62	syl2an 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ∈ (𝒫 𝑋 ∩ Fin))
64	44, 63	sselid 3933	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ∈ Fin)
65		iunin2 5020	. . . . . . . 8 ⊢ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) = ((𝐵‘𝑥) ∩ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1)))
66		heibor.8	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛))
67		oveq1 7356	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑡 → (𝑦𝐵𝑛) = (𝑡𝐵𝑛))
68	67	cbviunv 4989	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘𝑛)(𝑡𝐵𝑛)
69		fveq2 6822	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → (𝐹‘𝑛) = (𝐹‘((2nd ‘𝑥) + 1)))
70	69	iuneq1d 4969	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → ∪ 𝑡 ∈ (𝐹‘𝑛)(𝑡𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵𝑛))
71	68, 70	eqtrid 2776	. . . . . . . . . . . . . 14 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵𝑛))
72		oveq2 7357	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → (𝑡𝐵𝑛) = (𝑡𝐵((2nd ‘𝑥) + 1)))
73	72	iuneq2d 4972	. . . . . . . . . . . . . 14 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1)))
74	71, 73	eqtrd 2764	. . . . . . . . . . . . 13 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1)))
75	74	eqeq2d 2740	. . . . . . . . . . . 12 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → (𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) ↔ 𝑋 = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1))))
76	75	rspccva 3576	. . . . . . . . . . 11 ⊢ ((∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) ∧ ((2nd ‘𝑥) + 1) ∈ ℕ0) → 𝑋 = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1)))
77	66, 61, 76	syl2an 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝑋 = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1)))
78	77	ineq2d 4171	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((𝐵‘𝑥) ∩ 𝑋) = ((𝐵‘𝑥) ∩ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1))))
79	9	fveq2d 6826	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐺 → (𝐵‘𝑥) = (𝐵‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩))
80		df-ov 7352	. . . . . . . . . . . . . 14 ⊢ ((1st ‘𝑥)𝐵(2nd ‘𝑥)) = (𝐵‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
81	79, 80	eqtr4di 2782	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐺 → (𝐵‘𝑥) = ((1st ‘𝑥)𝐵(2nd ‘𝑥)))
82	81	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐵‘𝑥) = ((1st ‘𝑥)𝐵(2nd ‘𝑥)))
83		inss1 4188	. . . . . . . . . . . . . . . 16 ⊢ (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋
84		ffvelcdm 7015	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧ (2nd ‘𝑥) ∈ ℕ0) → (𝐹‘(2nd ‘𝑥)) ∈ (𝒫 𝑋 ∩ Fin))
85	45, 59, 84	syl2an 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘(2nd ‘𝑥)) ∈ (𝒫 𝑋 ∩ Fin))
86	83, 85	sselid 3933	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘(2nd ‘𝑥)) ∈ 𝒫 𝑋)
87	86	elpwid 4560	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘(2nd ‘𝑥)) ⊆ 𝑋)
88	19	simp2d 1143	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝐺 → (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)))
89	88	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)))
90	87, 89	sseldd 3936	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (1st ‘𝑥) ∈ 𝑋)
91	59	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (2nd ‘𝑥) ∈ ℕ0)
92		oveq1 7356	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (1st ‘𝑥) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑𝑚))))
93		oveq2 7357	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (2nd ‘𝑥) → (2↑𝑚) = (2↑(2nd ‘𝑥)))
94	93	oveq2d 7365	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (2nd ‘𝑥) → (1 / (2↑𝑚)) = (1 / (2↑(2nd ‘𝑥))))
95	94	oveq2d 7365	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (2nd ‘𝑥) → ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑𝑚))) = ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥)))))
96		heibor.5	. . . . . . . . . . . . . 14 ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))
97		ovex 7382	. . . . . . . . . . . . . 14 ⊢ ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥)))) ∈ V
98	92, 95, 96, 97	ovmpo 7509	. . . . . . . . . . . . 13 ⊢ (((1st ‘𝑥) ∈ 𝑋 ∧ (2nd ‘𝑥) ∈ ℕ0) → ((1st ‘𝑥)𝐵(2nd ‘𝑥)) = ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥)))))
99	90, 91, 98	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((1st ‘𝑥)𝐵(2nd ‘𝑥)) = ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥)))))
100	82, 99	eqtrd 2764	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐵‘𝑥) = ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥)))))
101		heibor.6	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))
102		cmetmet 25184	. . . . . . . . . . . . . . 15 ⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
103	101, 102	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))
104		metxmet 24220	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
105	103, 104	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
106	105	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝐷 ∈ (∞Met‘𝑋))
107		2nn 12201	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℕ
108		nnexpcl 13981	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℕ ∧ (2nd ‘𝑥) ∈ ℕ0) → (2↑(2nd ‘𝑥)) ∈ ℕ)
109	107, 91, 108	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (2↑(2nd ‘𝑥)) ∈ ℕ)
110	109	nnrpd 12935	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (2↑(2nd ‘𝑥)) ∈ ℝ+)
111	110	rpreccld 12947	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (1 / (2↑(2nd ‘𝑥))) ∈ ℝ+)
112	111	rpxrd 12938	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (1 / (2↑(2nd ‘𝑥))) ∈ ℝ*)
113		blssm 24304	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (1st ‘𝑥) ∈ 𝑋 ∧ (1 / (2↑(2nd ‘𝑥))) ∈ ℝ*) → ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥)))) ⊆ 𝑋)
114	106, 90, 112, 113	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥)))) ⊆ 𝑋)
115	100, 114	eqsstrd 3970	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐵‘𝑥) ⊆ 𝑋)
116		dfss2 3921	. . . . . . . . . 10 ⊢ ((𝐵‘𝑥) ⊆ 𝑋 ↔ ((𝐵‘𝑥) ∩ 𝑋) = (𝐵‘𝑥))
117	115, 116	sylib 218	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((𝐵‘𝑥) ∩ 𝑋) = (𝐵‘𝑥))
118	78, 117	eqtr3d 2766	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((𝐵‘𝑥) ∩ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1))) = (𝐵‘𝑥))
119	65, 118	eqtrid 2776	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) = (𝐵‘𝑥))
120		eqimss2 3995	. . . . . . 7 ⊢ (∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) = (𝐵‘𝑥) → (𝐵‘𝑥) ⊆ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))))
121	119, 120	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐵‘𝑥) ⊆ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))))
122	19	simp3d 1144	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐺 → ((1st ‘𝑥)𝐵(2nd ‘𝑥)) ∈ 𝐾)
123	81, 122	eqeltrd 2828	. . . . . . 7 ⊢ (𝑥 ∈ 𝐺 → (𝐵‘𝑥) ∈ 𝐾)
124	123	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐵‘𝑥) ∈ 𝐾)
125		fvex 6835	. . . . . . . 8 ⊢ (𝐵‘𝑥) ∈ V
126	125	inex1 5256	. . . . . . 7 ⊢ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ V
127	13, 14, 126	heiborlem1 37801	. . . . . 6 ⊢ (((𝐹‘((2nd ‘𝑥) + 1)) ∈ Fin ∧ (𝐵‘𝑥) ⊆ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∧ (𝐵‘𝑥) ∈ 𝐾) → ∃𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)
128	64, 121, 124, 127	syl3anc 1373	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ∃𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)
129	83, 63	sselid 3933	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ∈ 𝒫 𝑋)
130	129	elpwid 4560	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ⊆ 𝑋)
131	13	mopnuni 24327	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽)
132	105, 131	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
133	132	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝑋 = ∪ 𝐽)
134	130, 133	sseqtrd 3972	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ⊆ ∪ 𝐽)
135	134	sselda 3935	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))) → 𝑡 ∈ ∪ 𝐽)
136	135	adantrr 717	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ (𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) → 𝑡 ∈ ∪ 𝐽)
137	61	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((2nd ‘𝑥) + 1) ∈ ℕ0)
138		id 22	. . . . . . . . . 10 ⊢ (𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)) → 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)))
139		snfi 8968	. . . . . . . . . . . 12 ⊢ {(𝑡𝐵((2nd ‘𝑥) + 1))} ∈ Fin
140		inss2 4189	. . . . . . . . . . . . 13 ⊢ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ⊆ (𝑡𝐵((2nd ‘𝑥) + 1))
141		ovex 7382	. . . . . . . . . . . . . . 15 ⊢ (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ V
142	141	unisn 4877	. . . . . . . . . . . . . 14 ⊢ ∪ {(𝑡𝐵((2nd ‘𝑥) + 1))} = (𝑡𝐵((2nd ‘𝑥) + 1))
143		uniiun 5007	. . . . . . . . . . . . . 14 ⊢ ∪ {(𝑡𝐵((2nd ‘𝑥) + 1))} = ∪ 𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔
144	142, 143	eqtr3i 2754	. . . . . . . . . . . . 13 ⊢ (𝑡𝐵((2nd ‘𝑥) + 1)) = ∪ 𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔
145	140, 144	sseqtri 3984	. . . . . . . . . . . 12 ⊢ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ⊆ ∪ 𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔
146		vex 3440	. . . . . . . . . . . . 13 ⊢ 𝑔 ∈ V
147	13, 14, 146	heiborlem1 37801	. . . . . . . . . . . 12 ⊢ (({(𝑡𝐵((2nd ‘𝑥) + 1))} ∈ Fin ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ⊆ ∪ 𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔 ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) → ∃𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔 ∈ 𝐾)
148	139, 145, 147	mp3an12 1453	. . . . . . . . . . 11 ⊢ (((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 → ∃𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔 ∈ 𝐾)
149		eleq1 2816	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑡𝐵((2nd ‘𝑥) + 1)) → (𝑔 ∈ 𝐾 ↔ (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ 𝐾))
150	141, 149	rexsn 4634	. . . . . . . . . . 11 ⊢ (∃𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔 ∈ 𝐾 ↔ (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ 𝐾)
151	148, 150	sylib 218	. . . . . . . . . 10 ⊢ (((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 → (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ 𝐾)
152		ovex 7382	. . . . . . . . . . . 12 ⊢ ((2nd ‘𝑥) + 1) ∈ V
153	13, 14, 6, 42, 152	heiborlem2 37802	. . . . . . . . . . 11 ⊢ (𝑡𝐺((2nd ‘𝑥) + 1) ↔ (((2nd ‘𝑥) + 1) ∈ ℕ0 ∧ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)) ∧ (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ 𝐾))
154	153	biimpri 228	. . . . . . . . . 10 ⊢ ((((2nd ‘𝑥) + 1) ∈ ℕ0 ∧ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)) ∧ (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ 𝐾) → 𝑡𝐺((2nd ‘𝑥) + 1))
155	137, 138, 151, 154	syl3an 1160	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) → 𝑡𝐺((2nd ‘𝑥) + 1))
156	155	3expb 1120	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ (𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) → 𝑡𝐺((2nd ‘𝑥) + 1))
157		simprr 772	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ (𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) → ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)
158	136, 156, 157	jca32 515	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ (𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) → (𝑡 ∈ ∪ 𝐽 ∧ (𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)))
159	158	ex 412	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) → (𝑡 ∈ ∪ 𝐽 ∧ (𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))))
160	159	reximdv2 3139	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (∃𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 → ∃𝑡 ∈ ∪ 𝐽(𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)))
161	128, 160	mpd 15	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ∃𝑡 ∈ ∪ 𝐽(𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))
162	161	ralrimiva 3121	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ∃𝑡 ∈ ∪ 𝐽(𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))
163	13	fvexi 6836	. . . . 5 ⊢ 𝐽 ∈ V
164	163	uniex 7677	. . . 4 ⊢ ∪ 𝐽 ∈ V
165		breq1 5095	. . . . 5 ⊢ (𝑡 = (𝑔‘𝑥) → (𝑡𝐺((2nd ‘𝑥) + 1) ↔ (𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1)))
166		oveq1 7356	. . . . . . 7 ⊢ (𝑡 = (𝑔‘𝑥) → (𝑡𝐵((2nd ‘𝑥) + 1)) = ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1)))
167	166	ineq2d 4171	. . . . . 6 ⊢ (𝑡 = (𝑔‘𝑥) → ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) = ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))))
168	167	eleq1d 2813	. . . . 5 ⊢ (𝑡 = (𝑔‘𝑥) → (((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 ↔ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))
169	165, 168	anbi12d 632	. . . 4 ⊢ (𝑡 = (𝑔‘𝑥) → ((𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) ↔ ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)))
170	164, 169	axcc4dom 10335	. . 3 ⊢ ((𝐺 ≼ ω ∧ ∀𝑥 ∈ 𝐺 ∃𝑡 ∈ ∪ 𝐽(𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) → ∃𝑔(𝑔:𝐺⟶∪ 𝐽 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)))
171	58, 162, 170	syl2anc 584	. 2 ⊢ (𝜑 → ∃𝑔(𝑔:𝐺⟶∪ 𝐽 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)))
172		exsimpr 1869	. 2 ⊢ (∃𝑔(𝑔:𝐺⟶∪ 𝐽 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) → ∃𝑔∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))
173	171, 172	syl 17	1 ⊢ (𝜑 → ∃𝑔∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540  ∃wex 1779   ∈ wcel 2109  {cab 2707  ∀wral 3044  ∃wrex 3053  Vcvv 3436   ∩ cin 3902   ⊆ wss 3903  𝒫 cpw 4551  {csn 4577  ⟨cop 4583  ∪ cuni 4858  ∪ ciun 4941   class class class wbr 5092  {copab 5154   × cxp 5617  Rel wrel 5624  ⟶wf 6478  ‘cfv 6482  (class class class)co 7349   ∈ cmpo 7351  ωcom 7799  1^st c1st 7922  2^nd c2nd 7923   ≈ cen 8869   ≼ cdom 8870   ≺ csdm 8871  Fincfn 8872  1c1 11010   + caddc 11012  ℝ^*cxr 11148   / cdiv 11777  ℕcn 12128  2c2 12183  ℕ₀cn0 12384  ↑cexp 13968  ∞Metcxmet 21246  Metcmet 21247  ballcbl 21248  MetOpencmopn 21251  CMetccmet 25152

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5218  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-inf2 9537  ax-cc 10329  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086  ax-pre-sup 11087

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3343  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-int 4897  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-se 5573  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-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-isom 6491  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-om 7800  df-1st 7924  df-2nd 7925  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-1o 8388  df-er 8625  df-map 8755  df-en 8873  df-dom 8874  df-sdom 8875  df-fin 8876  df-sup 9332  df-inf 9333  df-oi 9402  df-card 9835  df-acn 9838  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-sub 11349  df-neg 11350  df-div 11778  df-nn 12129  df-2 12191  df-n0 12385  df-z 12472  df-uz 12736  df-q 12850  df-rp 12894  df-xneg 13014  df-xadd 13015  df-xmul 13016  df-seq 13909  df-exp 13969  df-topgen 17347  df-psmet 21253  df-xmet 21254  df-met 21255  df-bl 21256  df-mopn 21257  df-top 22779  df-topon 22796  df-bases 22831  df-cmet 25155

This theorem is referenced by:  heiborlem10  37810