Theorem heiborlem3 38016

Description: Lemma for heibor 38024. Using countable choice ax-cc 10349, 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 38014 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 10349 via iunctb 10489), and so we can apply ax-cc 10349 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 12411	. . . . . 6 ⊢ ℕ0 ∈ V
2		fvex 6848	. . . . . . 7 ⊢ (𝐹‘𝑡) ∈ V
3		vsnex 5380	. . . . . . 7 ⊢ {𝑡} ∈ V
4	2, 3	xpex 7700	. . . . . 6 ⊢ ((𝐹‘𝑡) × {𝑡}) ∈ V
5	1, 4	iunex 7914	. . . . 5 ⊢ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ∈ V
6		heibor.4	. . . . . . . . 9 ⊢ 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}
7	6	relopabiv 5770	. . . . . . . 8 ⊢ Rel 𝐺
8		1st2nd 7985	. . . . . . . 8 ⊢ ((Rel 𝐺 ∧ 𝑥 ∈ 𝐺) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
9	7, 8	mpan 691	. . . . . . 7 ⊢ (𝑥 ∈ 𝐺 → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
10	9	eleq1d 2822	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐺 → (𝑥 ∈ 𝐺 ↔ ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ 𝐺))
11		df-br 5100	. . . . . . . . . . 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 6848	. . . . . . . . . . 11 ⊢ (1st ‘𝑥) ∈ V
16		fvex 6848	. . . . . . . . . . 11 ⊢ (2nd ‘𝑥) ∈ V
17	13, 14, 6, 15, 16	heiborlem2 38015	. . . . . . . . . 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 4620	. . . . . . . . . . . 12 ⊢ (2nd ‘𝑥) ∈ {(2nd ‘𝑥)}
21		opelxp 5661	. . . . . . . . . . . 12 ⊢ (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ((𝐹‘(2nd ‘𝑥)) × {(2nd ‘𝑥)}) ↔ ((1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)) ∧ (2nd ‘𝑥) ∈ {(2nd ‘𝑥)}))
22	20, 21	mpbiran2 711	. . . . . . . . . . 11 ⊢ (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ((𝐹‘(2nd ‘𝑥)) × {(2nd ‘𝑥)}) ↔ (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)))
23		fveq2 6835	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (2nd ‘𝑥) → (𝐹‘𝑡) = (𝐹‘(2nd ‘𝑥)))
24		sneq 4591	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (2nd ‘𝑥) → {𝑡} = {(2nd ‘𝑥)})
25	23, 24	xpeq12d 5656	. . . . . . . . . . . . 13 ⊢ (𝑡 = (2nd ‘𝑥) → ((𝐹‘𝑡) × {𝑡}) = ((𝐹‘(2nd ‘𝑥)) × {(2nd ‘𝑥)}))
26	25	eleq2d 2823	. . . . . . . . . . . 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 596	. . . . . . . . . 10 ⊢ (((2nd ‘𝑥) ∈ ℕ0 ∧ (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥))) → ∃𝑡 ∈ ℕ0 ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ((𝐹‘𝑡) × {𝑡}))
29		eliun 4951	. . . . . . . . . 10 ⊢ (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ↔ ∃𝑡 ∈ ℕ0 ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ((𝐹‘𝑡) × {𝑡}))
30	28, 29	sylibr 234	. . . . . . . . 9 ⊢ (((2nd ‘𝑥) ∈ ℕ0 ∧ (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥))) → ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}))
31	30	3adant3 1133	. . . . . . . 8 ⊢ (((2nd ‘𝑥) ∈ ℕ0 ∧ (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)) ∧ ((1st ‘𝑥)𝐵(2nd ‘𝑥)) ∈ 𝐾) → ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}))
32	19, 31	syl 17	. . . . . . 7 ⊢ (𝑥 ∈ 𝐺 → ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}))
33	9, 32	eqeltrd 2837	. . . . . 6 ⊢ (𝑥 ∈ 𝐺 → 𝑥 ∈ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}))
34	33	ssriv 3938	. . . . 5 ⊢ 𝐺 ⊆ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡})
35		ssdomg 8941	. . . . 5 ⊢ (∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ∈ V → (𝐺 ⊆ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) → 𝐺 ≼ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡})))
36	5, 34, 35	mp2 9	. . . 4 ⊢ 𝐺 ≼ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡})
37		nn0ennn 13906	. . . . . . 7 ⊢ ℕ0 ≈ ℕ
38		nnenom 13907	. . . . . . 7 ⊢ ℕ ≈ ω
39	37, 38	entri 8949	. . . . . 6 ⊢ ℕ0 ≈ ω
40		endom 8920	. . . . . 6 ⊢ (ℕ0 ≈ ω → ℕ0 ≼ ω)
41	39, 40	ax-mp 5	. . . . 5 ⊢ ℕ0 ≼ ω
42		vex 3445	. . . . . . . 8 ⊢ 𝑡 ∈ V
43	2, 42	xpsnen 8993	. . . . . . 7 ⊢ ((𝐹‘𝑡) × {𝑡}) ≈ (𝐹‘𝑡)
44		inss2 4191	. . . . . . . . 9 ⊢ (𝒫 𝑋 ∩ Fin) ⊆ Fin
45		heibor.7	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))
46	45	ffvelcdmda 7031	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ ℕ0) → (𝐹‘𝑡) ∈ (𝒫 𝑋 ∩ Fin))
47	44, 46	sselid 3932	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ ℕ0) → (𝐹‘𝑡) ∈ Fin)
48		isfinite 9565	. . . . . . . . 9 ⊢ ((𝐹‘𝑡) ∈ Fin ↔ (𝐹‘𝑡) ≺ ω)
49		sdomdom 8921	. . . . . . . . 9 ⊢ ((𝐹‘𝑡) ≺ ω → (𝐹‘𝑡) ≼ ω)
50	48, 49	sylbi 217	. . . . . . . 8 ⊢ ((𝐹‘𝑡) ∈ Fin → (𝐹‘𝑡) ≼ ω)
51	47, 50	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ ℕ0) → (𝐹‘𝑡) ≼ ω)
52		endomtr 8953	. . . . . . 7 ⊢ ((((𝐹‘𝑡) × {𝑡}) ≈ (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≼ ω) → ((𝐹‘𝑡) × {𝑡}) ≼ ω)
53	43, 51, 52	sylancr 588	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ ℕ0) → ((𝐹‘𝑡) × {𝑡}) ≼ ω)
54	53	ralrimiva 3129	. . . . 5 ⊢ (𝜑 → ∀𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω)
55		iunctb 10489	. . . . 5 ⊢ ((ℕ0 ≼ ω ∧ ∀𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω) → ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω)
56	41, 54, 55	sylancr 588	. . . 4 ⊢ (𝜑 → ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω)
57		domtr 8948	. . . 4 ⊢ ((𝐺 ≼ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ∧ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω) → 𝐺 ≼ ω)
58	36, 56, 57	sylancr 588	. . 3 ⊢ (𝜑 → 𝐺 ≼ ω)
59	19	simp1d 1143	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐺 → (2nd ‘𝑥) ∈ ℕ0)
60		peano2nn0 12445	. . . . . . . . 9 ⊢ ((2nd ‘𝑥) ∈ ℕ0 → ((2nd ‘𝑥) + 1) ∈ ℕ0)
61	59, 60	syl 17	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐺 → ((2nd ‘𝑥) + 1) ∈ ℕ0)
62		ffvelcdm 7028	. . . . . . . 8 ⊢ ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧ ((2nd ‘𝑥) + 1) ∈ ℕ0) → (𝐹‘((2nd ‘𝑥) + 1)) ∈ (𝒫 𝑋 ∩ Fin))
63	45, 61, 62	syl2an 597	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ∈ (𝒫 𝑋 ∩ Fin))
64	44, 63	sselid 3932	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ∈ Fin)
65		iunin2 5027	. . . . . . . 8 ⊢ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) = ((𝐵‘𝑥) ∩ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1)))
66		heibor.8	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛))
67		oveq1 7367	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑡 → (𝑦𝐵𝑛) = (𝑡𝐵𝑛))
68	67	cbviunv 4995	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘𝑛)(𝑡𝐵𝑛)
69		fveq2 6835	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → (𝐹‘𝑛) = (𝐹‘((2nd ‘𝑥) + 1)))
70	69	iuneq1d 4975	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → ∪ 𝑡 ∈ (𝐹‘𝑛)(𝑡𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵𝑛))
71	68, 70	eqtrid 2784	. . . . . . . . . . . . . 14 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵𝑛))
72		oveq2 7368	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → (𝑡𝐵𝑛) = (𝑡𝐵((2nd ‘𝑥) + 1)))
73	72	iuneq2d 4978	. . . . . . . . . . . . . 14 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1)))
74	71, 73	eqtrd 2772	. . . . . . . . . . . . 13 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1)))
75	74	eqeq2d 2748	. . . . . . . . . . . 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 597	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝑋 = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1)))
78	77	ineq2d 4173	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((𝐵‘𝑥) ∩ 𝑋) = ((𝐵‘𝑥) ∩ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1))))
79	9	fveq2d 6839	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐺 → (𝐵‘𝑥) = (𝐵‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩))
80		df-ov 7363	. . . . . . . . . . . . . 14 ⊢ ((1st ‘𝑥)𝐵(2nd ‘𝑥)) = (𝐵‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
81	79, 80	eqtr4di 2790	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐺 → (𝐵‘𝑥) = ((1st ‘𝑥)𝐵(2nd ‘𝑥)))
82	81	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐵‘𝑥) = ((1st ‘𝑥)𝐵(2nd ‘𝑥)))
83		inss1 4190	. . . . . . . . . . . . . . . 16 ⊢ (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋
84		ffvelcdm 7028	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧ (2nd ‘𝑥) ∈ ℕ0) → (𝐹‘(2nd ‘𝑥)) ∈ (𝒫 𝑋 ∩ Fin))
85	45, 59, 84	syl2an 597	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘(2nd ‘𝑥)) ∈ (𝒫 𝑋 ∩ Fin))
86	83, 85	sselid 3932	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘(2nd ‘𝑥)) ∈ 𝒫 𝑋)
87	86	elpwid 4564	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘(2nd ‘𝑥)) ⊆ 𝑋)
88	19	simp2d 1144	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝐺 → (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)))
89	88	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)))
90	87, 89	sseldd 3935	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (1st ‘𝑥) ∈ 𝑋)
91	59	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (2nd ‘𝑥) ∈ ℕ0)
92		oveq1 7367	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (1st ‘𝑥) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑𝑚))))
93		oveq2 7368	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (2nd ‘𝑥) → (2↑𝑚) = (2↑(2nd ‘𝑥)))
94	93	oveq2d 7376	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (2nd ‘𝑥) → (1 / (2↑𝑚)) = (1 / (2↑(2nd ‘𝑥))))
95	94	oveq2d 7376	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (2nd ‘𝑥) → ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑𝑚))) = ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥)))))
96		heibor.5	. . . . . . . . . . . . . 14 ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))
97		ovex 7393	. . . . . . . . . . . . . 14 ⊢ ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥)))) ∈ V
98	92, 95, 96, 97	ovmpo 7520	. . . . . . . . . . . . 13 ⊢ (((1st ‘𝑥) ∈ 𝑋 ∧ (2nd ‘𝑥) ∈ ℕ0) → ((1st ‘𝑥)𝐵(2nd ‘𝑥)) = ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥)))))
99	90, 91, 98	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((1st ‘𝑥)𝐵(2nd ‘𝑥)) = ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥)))))
100	82, 99	eqtrd 2772	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐵‘𝑥) = ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥)))))
101		heibor.6	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))
102		cmetmet 25246	. . . . . . . . . . . . . . 15 ⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
103	101, 102	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))
104		metxmet 24282	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
105	103, 104	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
106	105	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝐷 ∈ (∞Met‘𝑋))
107		2nn 12222	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℕ
108		nnexpcl 14001	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℕ ∧ (2nd ‘𝑥) ∈ ℕ0) → (2↑(2nd ‘𝑥)) ∈ ℕ)
109	107, 91, 108	sylancr 588	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (2↑(2nd ‘𝑥)) ∈ ℕ)
110	109	nnrpd 12951	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (2↑(2nd ‘𝑥)) ∈ ℝ+)
111	110	rpreccld 12963	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (1 / (2↑(2nd ‘𝑥))) ∈ ℝ+)
112	111	rpxrd 12954	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (1 / (2↑(2nd ‘𝑥))) ∈ ℝ*)
113		blssm 24366	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (1st ‘𝑥) ∈ 𝑋 ∧ (1 / (2↑(2nd ‘𝑥))) ∈ ℝ*) → ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥)))) ⊆ 𝑋)
114	106, 90, 112, 113	syl3anc 1374	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥)))) ⊆ 𝑋)
115	100, 114	eqsstrd 3969	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐵‘𝑥) ⊆ 𝑋)
116		dfss2 3920	. . . . . . . . . 10 ⊢ ((𝐵‘𝑥) ⊆ 𝑋 ↔ ((𝐵‘𝑥) ∩ 𝑋) = (𝐵‘𝑥))
117	115, 116	sylib 218	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((𝐵‘𝑥) ∩ 𝑋) = (𝐵‘𝑥))
118	78, 117	eqtr3d 2774	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((𝐵‘𝑥) ∩ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1))) = (𝐵‘𝑥))
119	65, 118	eqtrid 2784	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) = (𝐵‘𝑥))
120		eqimss2 3994	. . . . . . 7 ⊢ (∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) = (𝐵‘𝑥) → (𝐵‘𝑥) ⊆ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))))
121	119, 120	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐵‘𝑥) ⊆ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))))
122	19	simp3d 1145	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐺 → ((1st ‘𝑥)𝐵(2nd ‘𝑥)) ∈ 𝐾)
123	81, 122	eqeltrd 2837	. . . . . . 7 ⊢ (𝑥 ∈ 𝐺 → (𝐵‘𝑥) ∈ 𝐾)
124	123	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐵‘𝑥) ∈ 𝐾)
125		fvex 6848	. . . . . . . 8 ⊢ (𝐵‘𝑥) ∈ V
126	125	inex1 5263	. . . . . . 7 ⊢ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ V
127	13, 14, 126	heiborlem1 38014	. . . . . 6 ⊢ (((𝐹‘((2nd ‘𝑥) + 1)) ∈ Fin ∧ (𝐵‘𝑥) ⊆ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∧ (𝐵‘𝑥) ∈ 𝐾) → ∃𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)
128	64, 121, 124, 127	syl3anc 1374	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ∃𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)
129	83, 63	sselid 3932	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ∈ 𝒫 𝑋)
130	129	elpwid 4564	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ⊆ 𝑋)
131	13	mopnuni 24389	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽)
132	105, 131	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
133	132	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝑋 = ∪ 𝐽)
134	130, 133	sseqtrd 3971	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ⊆ ∪ 𝐽)
135	134	sselda 3934	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))) → 𝑡 ∈ ∪ 𝐽)
136	135	adantrr 718	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ (𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) → 𝑡 ∈ ∪ 𝐽)
137	61	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((2nd ‘𝑥) + 1) ∈ ℕ0)
138		id 22	. . . . . . . . . 10 ⊢ (𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)) → 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)))
139		snfi 8984	. . . . . . . . . . . 12 ⊢ {(𝑡𝐵((2nd ‘𝑥) + 1))} ∈ Fin
140		inss2 4191	. . . . . . . . . . . . 13 ⊢ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ⊆ (𝑡𝐵((2nd ‘𝑥) + 1))
141		ovex 7393	. . . . . . . . . . . . . . 15 ⊢ (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ V
142	141	unisn 4883	. . . . . . . . . . . . . 14 ⊢ ∪ {(𝑡𝐵((2nd ‘𝑥) + 1))} = (𝑡𝐵((2nd ‘𝑥) + 1))
143		uniiun 5015	. . . . . . . . . . . . . 14 ⊢ ∪ {(𝑡𝐵((2nd ‘𝑥) + 1))} = ∪ 𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔
144	142, 143	eqtr3i 2762	. . . . . . . . . . . . 13 ⊢ (𝑡𝐵((2nd ‘𝑥) + 1)) = ∪ 𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔
145	140, 144	sseqtri 3983	. . . . . . . . . . . 12 ⊢ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ⊆ ∪ 𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔
146		vex 3445	. . . . . . . . . . . . 13 ⊢ 𝑔 ∈ V
147	13, 14, 146	heiborlem1 38014	. . . . . . . . . . . 12 ⊢ (({(𝑡𝐵((2nd ‘𝑥) + 1))} ∈ Fin ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ⊆ ∪ 𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔 ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) → ∃𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔 ∈ 𝐾)
148	139, 145, 147	mp3an12 1454	. . . . . . . . . . 11 ⊢ (((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 → ∃𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔 ∈ 𝐾)
149		eleq1 2825	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑡𝐵((2nd ‘𝑥) + 1)) → (𝑔 ∈ 𝐾 ↔ (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ 𝐾))
150	141, 149	rexsn 4640	. . . . . . . . . . 11 ⊢ (∃𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔 ∈ 𝐾 ↔ (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ 𝐾)
151	148, 150	sylib 218	. . . . . . . . . 10 ⊢ (((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 → (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ 𝐾)
152		ovex 7393	. . . . . . . . . . . 12 ⊢ ((2nd ‘𝑥) + 1) ∈ V
153	13, 14, 6, 42, 152	heiborlem2 38015	. . . . . . . . . . 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 1161	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) → 𝑡𝐺((2nd ‘𝑥) + 1))
156	155	3expb 1121	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ (𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) → 𝑡𝐺((2nd ‘𝑥) + 1))
157		simprr 773	. . . . . . . 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 3147	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (∃𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 → ∃𝑡 ∈ ∪ 𝐽(𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)))
161	128, 160	mpd 15	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ∃𝑡 ∈ ∪ 𝐽(𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))
162	161	ralrimiva 3129	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ∃𝑡 ∈ ∪ 𝐽(𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))
163	13	fvexi 6849	. . . . 5 ⊢ 𝐽 ∈ V
164	163	uniex 7688	. . . 4 ⊢ ∪ 𝐽 ∈ V
165		breq1 5102	. . . . 5 ⊢ (𝑡 = (𝑔‘𝑥) → (𝑡𝐺((2nd ‘𝑥) + 1) ↔ (𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1)))
166		oveq1 7367	. . . . . . 7 ⊢ (𝑡 = (𝑔‘𝑥) → (𝑡𝐵((2nd ‘𝑥) + 1)) = ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1)))
167	166	ineq2d 4173	. . . . . 6 ⊢ (𝑡 = (𝑔‘𝑥) → ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) = ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))))
168	167	eleq1d 2822	. . . . 5 ⊢ (𝑡 = (𝑔‘𝑥) → (((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 ↔ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))
169	165, 168	anbi12d 633	. . . 4 ⊢ (𝑡 = (𝑔‘𝑥) → ((𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) ↔ ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)))
170	164, 169	axcc4dom 10355	. . 3 ⊢ ((𝐺 ≼ ω ∧ ∀𝑥 ∈ 𝐺 ∃𝑡 ∈ ∪ 𝐽(𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) → ∃𝑔(𝑔:𝐺⟶∪ 𝐽 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)))
171	58, 162, 170	syl2anc 585	. 2 ⊢ (𝜑 → ∃𝑔(𝑔:𝐺⟶∪ 𝐽 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)))
172		exsimpr 1871	. 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 1087   = wceq 1542  ∃wex 1781   ∈ wcel 2114  {cab 2715  ∀wral 3052  ∃wrex 3061  Vcvv 3441   ∩ cin 3901   ⊆ wss 3902  𝒫 cpw 4555  {csn 4581  ⟨cop 4587  ∪ cuni 4864  ∪ ciun 4947   class class class wbr 5099  {copab 5161   × cxp 5623  Rel wrel 5630  ⟶wf 6489  ‘cfv 6493  (class class class)co 7360   ∈ cmpo 7362  ωcom 7810  1^st c1st 7933  2^nd c2nd 7934   ≈ cen 8884   ≼ cdom 8885   ≺ csdm 8886  Fincfn 8887  1c1 11031   + caddc 11033  ℝ^*cxr 11169   / cdiv 11798  ℕcn 12149  2c2 12204  ℕ₀cn0 12405  ↑cexp 13988  ∞Metcxmet 21298  Metcmet 21299  ballcbl 21300  MetOpencmopn 21303  CMetccmet 25214

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-rep 5225  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682  ax-inf2 9554  ax-cc 10349  ax-cnex 11086  ax-resscn 11087  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-addrcl 11091  ax-mulcl 11092  ax-mulrcl 11093  ax-mulcom 11094  ax-addass 11095  ax-mulass 11096  ax-distr 11097  ax-i2m1 11098  ax-1ne0 11099  ax-1rid 11100  ax-rnegex 11101  ax-rrecex 11102  ax-cnre 11103  ax-pre-lttri 11104  ax-pre-lttrn 11105  ax-pre-ltadd 11106  ax-pre-mulgt0 11107  ax-pre-sup 11108

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-nel 3038  df-ral 3053  df-rex 3062  df-rmo 3351  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  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-int 4904  df-iun 4949  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-se 5579  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-pred 6260  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-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-isom 6502  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-1st 7935  df-2nd 7936  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-1o 8399  df-er 8637  df-map 8769  df-en 8888  df-dom 8889  df-sdom 8890  df-fin 8891  df-sup 9349  df-inf 9350  df-oi 9419  df-card 9855  df-acn 9858  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-div 11799  df-nn 12150  df-2 12212  df-n0 12406  df-z 12493  df-uz 12756  df-q 12866  df-rp 12910  df-xneg 13030  df-xadd 13031  df-xmul 13032  df-seq 13929  df-exp 13989  df-topgen 17367  df-psmet 21305  df-xmet 21306  df-met 21307  df-bl 21308  df-mopn 21309  df-top 22842  df-topon 22859  df-bases 22894  df-cmet 25217

This theorem is referenced by:  heiborlem10  38023