Theorem heiborlem3 37842

Description: Lemma for heibor 37850. Using countable choice ax-cc 10454, 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 37840 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 10454 via iunctb 10593), and so we can apply ax-cc 10454 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 12512	. . . . . 6 ⊢ ℕ0 ∈ V
2		fvex 6894	. . . . . . 7 ⊢ (𝐹‘𝑡) ∈ V
3		vsnex 5409	. . . . . . 7 ⊢ {𝑡} ∈ V
4	2, 3	xpex 7752	. . . . . 6 ⊢ ((𝐹‘𝑡) × {𝑡}) ∈ V
5	1, 4	iunex 7972	. . . . 5 ⊢ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ∈ V
6		heibor.4	. . . . . . . . 9 ⊢ 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}
7	6	relopabiv 5804	. . . . . . . 8 ⊢ Rel 𝐺
8		1st2nd 8043	. . . . . . . 8 ⊢ ((Rel 𝐺 ∧ 𝑥 ∈ 𝐺) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
9	7, 8	mpan 690	. . . . . . 7 ⊢ (𝑥 ∈ 𝐺 → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
10	9	eleq1d 2820	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐺 → (𝑥 ∈ 𝐺 ↔ ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ 𝐺))
11		df-br 5125	. . . . . . . . . . 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 6894	. . . . . . . . . . 11 ⊢ (1st ‘𝑥) ∈ V
16		fvex 6894	. . . . . . . . . . 11 ⊢ (2nd ‘𝑥) ∈ V
17	13, 14, 6, 15, 16	heiborlem2 37841	. . . . . . . . . 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 4643	. . . . . . . . . . . 12 ⊢ (2nd ‘𝑥) ∈ {(2nd ‘𝑥)}
21		opelxp 5695	. . . . . . . . . . . 12 ⊢ (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ((𝐹‘(2nd ‘𝑥)) × {(2nd ‘𝑥)}) ↔ ((1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)) ∧ (2nd ‘𝑥) ∈ {(2nd ‘𝑥)}))
22	20, 21	mpbiran2 710	. . . . . . . . . . 11 ⊢ (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ((𝐹‘(2nd ‘𝑥)) × {(2nd ‘𝑥)}) ↔ (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)))
23		fveq2 6881	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (2nd ‘𝑥) → (𝐹‘𝑡) = (𝐹‘(2nd ‘𝑥)))
24		sneq 4616	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (2nd ‘𝑥) → {𝑡} = {(2nd ‘𝑥)})
25	23, 24	xpeq12d 5690	. . . . . . . . . . . . 13 ⊢ (𝑡 = (2nd ‘𝑥) → ((𝐹‘𝑡) × {𝑡}) = ((𝐹‘(2nd ‘𝑥)) × {(2nd ‘𝑥)}))
26	25	eleq2d 2821	. . . . . . . . . . . 12 ⊢ (𝑡 = (2nd ‘𝑥) → (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ((𝐹‘𝑡) × {𝑡}) ↔ ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ((𝐹‘(2nd ‘𝑥)) × {(2nd ‘𝑥)})))
27	26	rspcev 3606	. . . . . . . . . . 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 4976	. . . . . . . . . 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 2835	. . . . . 6 ⊢ (𝑥 ∈ 𝐺 → 𝑥 ∈ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}))
34	33	ssriv 3967	. . . . 5 ⊢ 𝐺 ⊆ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡})
35		ssdomg 9019	. . . . 5 ⊢ (∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ∈ V → (𝐺 ⊆ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) → 𝐺 ≼ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡})))
36	5, 34, 35	mp2 9	. . . 4 ⊢ 𝐺 ≼ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡})
37		nn0ennn 14002	. . . . . . 7 ⊢ ℕ0 ≈ ℕ
38		nnenom 14003	. . . . . . 7 ⊢ ℕ ≈ ω
39	37, 38	entri 9027	. . . . . 6 ⊢ ℕ0 ≈ ω
40		endom 8998	. . . . . 6 ⊢ (ℕ0 ≈ ω → ℕ0 ≼ ω)
41	39, 40	ax-mp 5	. . . . 5 ⊢ ℕ0 ≼ ω
42		vex 3468	. . . . . . . 8 ⊢ 𝑡 ∈ V
43	2, 42	xpsnen 9074	. . . . . . 7 ⊢ ((𝐹‘𝑡) × {𝑡}) ≈ (𝐹‘𝑡)
44		inss2 4218	. . . . . . . . 9 ⊢ (𝒫 𝑋 ∩ Fin) ⊆ Fin
45		heibor.7	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))
46	45	ffvelcdmda 7079	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ ℕ0) → (𝐹‘𝑡) ∈ (𝒫 𝑋 ∩ Fin))
47	44, 46	sselid 3961	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ ℕ0) → (𝐹‘𝑡) ∈ Fin)
48		isfinite 9671	. . . . . . . . 9 ⊢ ((𝐹‘𝑡) ∈ Fin ↔ (𝐹‘𝑡) ≺ ω)
49		sdomdom 8999	. . . . . . . . 9 ⊢ ((𝐹‘𝑡) ≺ ω → (𝐹‘𝑡) ≼ ω)
50	48, 49	sylbi 217	. . . . . . . 8 ⊢ ((𝐹‘𝑡) ∈ Fin → (𝐹‘𝑡) ≼ ω)
51	47, 50	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ ℕ0) → (𝐹‘𝑡) ≼ ω)
52		endomtr 9031	. . . . . . 7 ⊢ ((((𝐹‘𝑡) × {𝑡}) ≈ (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≼ ω) → ((𝐹‘𝑡) × {𝑡}) ≼ ω)
53	43, 51, 52	sylancr 587	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ ℕ0) → ((𝐹‘𝑡) × {𝑡}) ≼ ω)
54	53	ralrimiva 3133	. . . . 5 ⊢ (𝜑 → ∀𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω)
55		iunctb 10593	. . . . 5 ⊢ ((ℕ0 ≼ ω ∧ ∀𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω) → ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω)
56	41, 54, 55	sylancr 587	. . . 4 ⊢ (𝜑 → ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω)
57		domtr 9026	. . . 4 ⊢ ((𝐺 ≼ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ∧ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω) → 𝐺 ≼ ω)
58	36, 56, 57	sylancr 587	. . 3 ⊢ (𝜑 → 𝐺 ≼ ω)
59	19	simp1d 1142	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐺 → (2nd ‘𝑥) ∈ ℕ0)
60		peano2nn0 12546	. . . . . . . . 9 ⊢ ((2nd ‘𝑥) ∈ ℕ0 → ((2nd ‘𝑥) + 1) ∈ ℕ0)
61	59, 60	syl 17	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐺 → ((2nd ‘𝑥) + 1) ∈ ℕ0)
62		ffvelcdm 7076	. . . . . . . 8 ⊢ ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧ ((2nd ‘𝑥) + 1) ∈ ℕ0) → (𝐹‘((2nd ‘𝑥) + 1)) ∈ (𝒫 𝑋 ∩ Fin))
63	45, 61, 62	syl2an 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ∈ (𝒫 𝑋 ∩ Fin))
64	44, 63	sselid 3961	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ∈ Fin)
65		iunin2 5052	. . . . . . . 8 ⊢ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) = ((𝐵‘𝑥) ∩ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1)))
66		heibor.8	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛))
67		oveq1 7417	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑡 → (𝑦𝐵𝑛) = (𝑡𝐵𝑛))
68	67	cbviunv 5021	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘𝑛)(𝑡𝐵𝑛)
69		fveq2 6881	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → (𝐹‘𝑛) = (𝐹‘((2nd ‘𝑥) + 1)))
70	69	iuneq1d 5000	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → ∪ 𝑡 ∈ (𝐹‘𝑛)(𝑡𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵𝑛))
71	68, 70	eqtrid 2783	. . . . . . . . . . . . . 14 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵𝑛))
72		oveq2 7418	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → (𝑡𝐵𝑛) = (𝑡𝐵((2nd ‘𝑥) + 1)))
73	72	iuneq2d 5003	. . . . . . . . . . . . . 14 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1)))
74	71, 73	eqtrd 2771	. . . . . . . . . . . . 13 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1)))
75	74	eqeq2d 2747	. . . . . . . . . . . 12 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → (𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) ↔ 𝑋 = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1))))
76	75	rspccva 3605	. . . . . . . . . . 11 ⊢ ((∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) ∧ ((2nd ‘𝑥) + 1) ∈ ℕ0) → 𝑋 = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1)))
77	66, 61, 76	syl2an 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝑋 = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1)))
78	77	ineq2d 4200	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((𝐵‘𝑥) ∩ 𝑋) = ((𝐵‘𝑥) ∩ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1))))
79	9	fveq2d 6885	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐺 → (𝐵‘𝑥) = (𝐵‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩))
80		df-ov 7413	. . . . . . . . . . . . . 14 ⊢ ((1st ‘𝑥)𝐵(2nd ‘𝑥)) = (𝐵‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
81	79, 80	eqtr4di 2789	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐺 → (𝐵‘𝑥) = ((1st ‘𝑥)𝐵(2nd ‘𝑥)))
82	81	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐵‘𝑥) = ((1st ‘𝑥)𝐵(2nd ‘𝑥)))
83		inss1 4217	. . . . . . . . . . . . . . . 16 ⊢ (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋
84		ffvelcdm 7076	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧ (2nd ‘𝑥) ∈ ℕ0) → (𝐹‘(2nd ‘𝑥)) ∈ (𝒫 𝑋 ∩ Fin))
85	45, 59, 84	syl2an 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘(2nd ‘𝑥)) ∈ (𝒫 𝑋 ∩ Fin))
86	83, 85	sselid 3961	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘(2nd ‘𝑥)) ∈ 𝒫 𝑋)
87	86	elpwid 4589	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘(2nd ‘𝑥)) ⊆ 𝑋)
88	19	simp2d 1143	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝐺 → (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)))
89	88	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)))
90	87, 89	sseldd 3964	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (1st ‘𝑥) ∈ 𝑋)
91	59	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (2nd ‘𝑥) ∈ ℕ0)
92		oveq1 7417	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (1st ‘𝑥) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑𝑚))))
93		oveq2 7418	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (2nd ‘𝑥) → (2↑𝑚) = (2↑(2nd ‘𝑥)))
94	93	oveq2d 7426	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (2nd ‘𝑥) → (1 / (2↑𝑚)) = (1 / (2↑(2nd ‘𝑥))))
95	94	oveq2d 7426	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (2nd ‘𝑥) → ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑𝑚))) = ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥)))))
96		heibor.5	. . . . . . . . . . . . . 14 ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))
97		ovex 7443	. . . . . . . . . . . . . 14 ⊢ ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥)))) ∈ V
98	92, 95, 96, 97	ovmpo 7572	. . . . . . . . . . . . 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 2771	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐵‘𝑥) = ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥)))))
101		heibor.6	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))
102		cmetmet 25243	. . . . . . . . . . . . . . 15 ⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
103	101, 102	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))
104		metxmet 24278	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
105	103, 104	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
106	105	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝐷 ∈ (∞Met‘𝑋))
107		2nn 12318	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℕ
108		nnexpcl 14097	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℕ ∧ (2nd ‘𝑥) ∈ ℕ0) → (2↑(2nd ‘𝑥)) ∈ ℕ)
109	107, 91, 108	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (2↑(2nd ‘𝑥)) ∈ ℕ)
110	109	nnrpd 13054	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (2↑(2nd ‘𝑥)) ∈ ℝ+)
111	110	rpreccld 13066	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (1 / (2↑(2nd ‘𝑥))) ∈ ℝ+)
112	111	rpxrd 13057	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (1 / (2↑(2nd ‘𝑥))) ∈ ℝ*)
113		blssm 24362	. . . . . . . . . . . 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 3998	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐵‘𝑥) ⊆ 𝑋)
116		dfss2 3949	. . . . . . . . . 10 ⊢ ((𝐵‘𝑥) ⊆ 𝑋 ↔ ((𝐵‘𝑥) ∩ 𝑋) = (𝐵‘𝑥))
117	115, 116	sylib 218	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((𝐵‘𝑥) ∩ 𝑋) = (𝐵‘𝑥))
118	78, 117	eqtr3d 2773	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((𝐵‘𝑥) ∩ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1))) = (𝐵‘𝑥))
119	65, 118	eqtrid 2783	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) = (𝐵‘𝑥))
120		eqimss2 4023	. . . . . . 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 2835	. . . . . . 7 ⊢ (𝑥 ∈ 𝐺 → (𝐵‘𝑥) ∈ 𝐾)
124	123	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐵‘𝑥) ∈ 𝐾)
125		fvex 6894	. . . . . . . 8 ⊢ (𝐵‘𝑥) ∈ V
126	125	inex1 5292	. . . . . . 7 ⊢ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ V
127	13, 14, 126	heiborlem1 37840	. . . . . 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 3961	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ∈ 𝒫 𝑋)
130	129	elpwid 4589	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ⊆ 𝑋)
131	13	mopnuni 24385	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽)
132	105, 131	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
133	132	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝑋 = ∪ 𝐽)
134	130, 133	sseqtrd 4000	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ⊆ ∪ 𝐽)
135	134	sselda 3963	. . . . . . . . 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 9062	. . . . . . . . . . . 12 ⊢ {(𝑡𝐵((2nd ‘𝑥) + 1))} ∈ Fin
140		inss2 4218	. . . . . . . . . . . . 13 ⊢ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ⊆ (𝑡𝐵((2nd ‘𝑥) + 1))
141		ovex 7443	. . . . . . . . . . . . . . 15 ⊢ (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ V
142	141	unisn 4907	. . . . . . . . . . . . . 14 ⊢ ∪ {(𝑡𝐵((2nd ‘𝑥) + 1))} = (𝑡𝐵((2nd ‘𝑥) + 1))
143		uniiun 5039	. . . . . . . . . . . . . 14 ⊢ ∪ {(𝑡𝐵((2nd ‘𝑥) + 1))} = ∪ 𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔
144	142, 143	eqtr3i 2761	. . . . . . . . . . . . 13 ⊢ (𝑡𝐵((2nd ‘𝑥) + 1)) = ∪ 𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔
145	140, 144	sseqtri 4012	. . . . . . . . . . . 12 ⊢ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ⊆ ∪ 𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔
146		vex 3468	. . . . . . . . . . . . 13 ⊢ 𝑔 ∈ V
147	13, 14, 146	heiborlem1 37840	. . . . . . . . . . . 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 2823	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑡𝐵((2nd ‘𝑥) + 1)) → (𝑔 ∈ 𝐾 ↔ (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ 𝐾))
150	141, 149	rexsn 4663	. . . . . . . . . . 11 ⊢ (∃𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔 ∈ 𝐾 ↔ (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ 𝐾)
151	148, 150	sylib 218	. . . . . . . . . 10 ⊢ (((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 → (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ 𝐾)
152		ovex 7443	. . . . . . . . . . . 12 ⊢ ((2nd ‘𝑥) + 1) ∈ V
153	13, 14, 6, 42, 152	heiborlem2 37841	. . . . . . . . . . 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 3151	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (∃𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 → ∃𝑡 ∈ ∪ 𝐽(𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)))
161	128, 160	mpd 15	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ∃𝑡 ∈ ∪ 𝐽(𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))
162	161	ralrimiva 3133	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ∃𝑡 ∈ ∪ 𝐽(𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))
163	13	fvexi 6895	. . . . 5 ⊢ 𝐽 ∈ V
164	163	uniex 7740	. . . 4 ⊢ ∪ 𝐽 ∈ V
165		breq1 5127	. . . . 5 ⊢ (𝑡 = (𝑔‘𝑥) → (𝑡𝐺((2nd ‘𝑥) + 1) ↔ (𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1)))
166		oveq1 7417	. . . . . . 7 ⊢ (𝑡 = (𝑔‘𝑥) → (𝑡𝐵((2nd ‘𝑥) + 1)) = ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1)))
167	166	ineq2d 4200	. . . . . 6 ⊢ (𝑡 = (𝑔‘𝑥) → ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) = ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))))
168	167	eleq1d 2820	. . . . 5 ⊢ (𝑡 = (𝑔‘𝑥) → (((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 ↔ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))
169	165, 168	anbi12d 632	. . . 4 ⊢ (𝑡 = (𝑔‘𝑥) → ((𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) ↔ ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)))
170	164, 169	axcc4dom 10460	. . 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 2714  ∀wral 3052  ∃wrex 3061  Vcvv 3464   ∩ cin 3930   ⊆ wss 3931  𝒫 cpw 4580  {csn 4606  ⟨cop 4612  ∪ cuni 4888  ∪ ciun 4972   class class class wbr 5124  {copab 5186   × cxp 5657  Rel wrel 5664  ⟶wf 6532  ‘cfv 6536  (class class class)co 7410   ∈ cmpo 7412  ωcom 7866  1^st c1st 7991  2^nd c2nd 7992   ≈ cen 8961   ≼ cdom 8962   ≺ csdm 8963  Fincfn 8964  1c1 11135   + caddc 11137  ℝ^*cxr 11273   / cdiv 11899  ℕcn 12245  2c2 12300  ℕ₀cn0 12506  ↑cexp 14084  ∞Metcxmet 21305  Metcmet 21306  ballcbl 21307  MetOpencmopn 21310  CMetccmet 25211

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 2708  ax-rep 5254  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-inf2 9660  ax-cc 10454  ax-cnex 11190  ax-resscn 11191  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-mulcom 11198  ax-addass 11199  ax-mulass 11200  ax-distr 11201  ax-i2m1 11202  ax-1ne0 11203  ax-1rid 11204  ax-rnegex 11205  ax-rrecex 11206  ax-cnre 11207  ax-pre-lttri 11208  ax-pre-lttrn 11209  ax-pre-ltadd 11210  ax-pre-mulgt0 11211  ax-pre-sup 11212

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 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rmo 3364  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-int 4928  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-se 5612  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7867  df-1st 7993  df-2nd 7994  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-er 8724  df-map 8847  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-sup 9459  df-inf 9460  df-oi 9529  df-card 9958  df-acn 9961  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280  df-sub 11473  df-neg 11474  df-div 11900  df-nn 12246  df-2 12308  df-n0 12507  df-z 12594  df-uz 12858  df-q 12970  df-rp 13014  df-xneg 13133  df-xadd 13134  df-xmul 13135  df-seq 14025  df-exp 14085  df-topgen 17462  df-psmet 21312  df-xmet 21313  df-met 21314  df-bl 21315  df-mopn 21316  df-top 22837  df-topon 22854  df-bases 22889  df-cmet 25214

This theorem is referenced by:  heiborlem10  37849