Theorem heiborlem3 38152

Description: Lemma for heibor 38160. Using countable choice ax-cc 10352, 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 38150 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 10352 via iunctb 10492), and so we can apply ax-cc 10352 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 12438	. . . . . 6 ⊢ ℕ0 ∈ V
2		fvex 6849	. . . . . . 7 ⊢ (𝐹‘𝑡) ∈ V
3		vsnex 5374	. . . . . . 7 ⊢ {𝑡} ∈ V
4	2, 3	xpex 7702	. . . . . 6 ⊢ ((𝐹‘𝑡) × {𝑡}) ∈ V
5	1, 4	iunex 7916	. . . . 5 ⊢ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ∈ V
6		heibor.4	. . . . . . . . 9 ⊢ 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}
7	6	relopabiv 5771	. . . . . . . 8 ⊢ Rel 𝐺
8		1st2nd 7987	. . . . . . . 8 ⊢ ((Rel 𝐺 ∧ 𝑥 ∈ 𝐺) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
9	7, 8	mpan 691	. . . . . . 7 ⊢ (𝑥 ∈ 𝐺 → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
10	9	eleq1d 2822	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐺 → (𝑥 ∈ 𝐺 ↔ ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ 𝐺))
11		df-br 5087	. . . . . . . . . . 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 6849	. . . . . . . . . . 11 ⊢ (1st ‘𝑥) ∈ V
16		fvex 6849	. . . . . . . . . . 11 ⊢ (2nd ‘𝑥) ∈ V
17	13, 14, 6, 15, 16	heiborlem2 38151	. . . . . . . . . 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 4607	. . . . . . . . . . . 12 ⊢ (2nd ‘𝑥) ∈ {(2nd ‘𝑥)}
21		opelxp 5662	. . . . . . . . . . . 12 ⊢ (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ((𝐹‘(2nd ‘𝑥)) × {(2nd ‘𝑥)}) ↔ ((1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)) ∧ (2nd ‘𝑥) ∈ {(2nd ‘𝑥)}))
22	20, 21	mpbiran2 711	. . . . . . . . . . 11 ⊢ (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ((𝐹‘(2nd ‘𝑥)) × {(2nd ‘𝑥)}) ↔ (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)))
23		fveq2 6836	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (2nd ‘𝑥) → (𝐹‘𝑡) = (𝐹‘(2nd ‘𝑥)))
24		sneq 4578	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (2nd ‘𝑥) → {𝑡} = {(2nd ‘𝑥)})
25	23, 24	xpeq12d 5657	. . . . . . . . . . . . 13 ⊢ (𝑡 = (2nd ‘𝑥) → ((𝐹‘𝑡) × {𝑡}) = ((𝐹‘(2nd ‘𝑥)) × {(2nd ‘𝑥)}))
26	25	eleq2d 2823	. . . . . . . . . . . 12 ⊢ (𝑡 = (2nd ‘𝑥) → (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ((𝐹‘𝑡) × {𝑡}) ↔ ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ((𝐹‘(2nd ‘𝑥)) × {(2nd ‘𝑥)})))
27	26	rspcev 3565	. . . . . . . . . . 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 4938	. . . . . . . . . 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 3926	. . . . 5 ⊢ 𝐺 ⊆ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡})
35		ssdomg 8942	. . . . 5 ⊢ (∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ∈ V → (𝐺 ⊆ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) → 𝐺 ≼ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡})))
36	5, 34, 35	mp2 9	. . . 4 ⊢ 𝐺 ≼ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡})
37		nn0ennn 13936	. . . . . . 7 ⊢ ℕ0 ≈ ℕ
38		nnenom 13937	. . . . . . 7 ⊢ ℕ ≈ ω
39	37, 38	entri 8950	. . . . . 6 ⊢ ℕ0 ≈ ω
40		endom 8921	. . . . . 6 ⊢ (ℕ0 ≈ ω → ℕ0 ≼ ω)
41	39, 40	ax-mp 5	. . . . 5 ⊢ ℕ0 ≼ ω
42		vex 3434	. . . . . . . 8 ⊢ 𝑡 ∈ V
43	2, 42	xpsnen 8994	. . . . . . 7 ⊢ ((𝐹‘𝑡) × {𝑡}) ≈ (𝐹‘𝑡)
44		inss2 4179	. . . . . . . . 9 ⊢ (𝒫 𝑋 ∩ Fin) ⊆ Fin
45		heibor.7	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))
46	45	ffvelcdmda 7032	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ ℕ0) → (𝐹‘𝑡) ∈ (𝒫 𝑋 ∩ Fin))
47	44, 46	sselid 3920	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ ℕ0) → (𝐹‘𝑡) ∈ Fin)
48		isfinite 9568	. . . . . . . . 9 ⊢ ((𝐹‘𝑡) ∈ Fin ↔ (𝐹‘𝑡) ≺ ω)
49		sdomdom 8922	. . . . . . . . 9 ⊢ ((𝐹‘𝑡) ≺ ω → (𝐹‘𝑡) ≼ ω)
50	48, 49	sylbi 217	. . . . . . . 8 ⊢ ((𝐹‘𝑡) ∈ Fin → (𝐹‘𝑡) ≼ ω)
51	47, 50	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ ℕ0) → (𝐹‘𝑡) ≼ ω)
52		endomtr 8954	. . . . . . 7 ⊢ ((((𝐹‘𝑡) × {𝑡}) ≈ (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≼ ω) → ((𝐹‘𝑡) × {𝑡}) ≼ ω)
53	43, 51, 52	sylancr 588	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ ℕ0) → ((𝐹‘𝑡) × {𝑡}) ≼ ω)
54	53	ralrimiva 3130	. . . . 5 ⊢ (𝜑 → ∀𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω)
55		iunctb 10492	. . . . 5 ⊢ ((ℕ0 ≼ ω ∧ ∀𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω) → ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω)
56	41, 54, 55	sylancr 588	. . . 4 ⊢ (𝜑 → ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω)
57		domtr 8949	. . . 4 ⊢ ((𝐺 ≼ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ∧ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω) → 𝐺 ≼ ω)
58	36, 56, 57	sylancr 588	. . 3 ⊢ (𝜑 → 𝐺 ≼ ω)
59	19	simp1d 1143	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐺 → (2nd ‘𝑥) ∈ ℕ0)
60		peano2nn0 12472	. . . . . . . . 9 ⊢ ((2nd ‘𝑥) ∈ ℕ0 → ((2nd ‘𝑥) + 1) ∈ ℕ0)
61	59, 60	syl 17	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐺 → ((2nd ‘𝑥) + 1) ∈ ℕ0)
62		ffvelcdm 7029	. . . . . . . 8 ⊢ ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧ ((2nd ‘𝑥) + 1) ∈ ℕ0) → (𝐹‘((2nd ‘𝑥) + 1)) ∈ (𝒫 𝑋 ∩ Fin))
63	45, 61, 62	syl2an 597	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ∈ (𝒫 𝑋 ∩ Fin))
64	44, 63	sselid 3920	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ∈ Fin)
65		iunin2 5014	. . . . . . . 8 ⊢ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) = ((𝐵‘𝑥) ∩ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1)))
66		heibor.8	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛))
67		oveq1 7369	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑡 → (𝑦𝐵𝑛) = (𝑡𝐵𝑛))
68	67	cbviunv 4982	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘𝑛)(𝑡𝐵𝑛)
69		fveq2 6836	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → (𝐹‘𝑛) = (𝐹‘((2nd ‘𝑥) + 1)))
70	69	iuneq1d 4962	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → ∪ 𝑡 ∈ (𝐹‘𝑛)(𝑡𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵𝑛))
71	68, 70	eqtrid 2784	. . . . . . . . . . . . . 14 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵𝑛))
72		oveq2 7370	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → (𝑡𝐵𝑛) = (𝑡𝐵((2nd ‘𝑥) + 1)))
73	72	iuneq2d 4965	. . . . . . . . . . . . . 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 3564	. . . . . . . . . . 11 ⊢ ((∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) ∧ ((2nd ‘𝑥) + 1) ∈ ℕ0) → 𝑋 = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1)))
77	66, 61, 76	syl2an 597	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝑋 = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1)))
78	77	ineq2d 4161	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((𝐵‘𝑥) ∩ 𝑋) = ((𝐵‘𝑥) ∩ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1))))
79	9	fveq2d 6840	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐺 → (𝐵‘𝑥) = (𝐵‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩))
80		df-ov 7365	. . . . . . . . . . . . . 14 ⊢ ((1st ‘𝑥)𝐵(2nd ‘𝑥)) = (𝐵‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
81	79, 80	eqtr4di 2790	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐺 → (𝐵‘𝑥) = ((1st ‘𝑥)𝐵(2nd ‘𝑥)))
82	81	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐵‘𝑥) = ((1st ‘𝑥)𝐵(2nd ‘𝑥)))
83		inss1 4178	. . . . . . . . . . . . . . . 16 ⊢ (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋
84		ffvelcdm 7029	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧ (2nd ‘𝑥) ∈ ℕ0) → (𝐹‘(2nd ‘𝑥)) ∈ (𝒫 𝑋 ∩ Fin))
85	45, 59, 84	syl2an 597	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘(2nd ‘𝑥)) ∈ (𝒫 𝑋 ∩ Fin))
86	83, 85	sselid 3920	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘(2nd ‘𝑥)) ∈ 𝒫 𝑋)
87	86	elpwid 4551	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘(2nd ‘𝑥)) ⊆ 𝑋)
88	19	simp2d 1144	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝐺 → (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)))
89	88	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)))
90	87, 89	sseldd 3923	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (1st ‘𝑥) ∈ 𝑋)
91	59	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (2nd ‘𝑥) ∈ ℕ0)
92		oveq1 7369	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (1st ‘𝑥) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑𝑚))))
93		oveq2 7370	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (2nd ‘𝑥) → (2↑𝑚) = (2↑(2nd ‘𝑥)))
94	93	oveq2d 7378	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (2nd ‘𝑥) → (1 / (2↑𝑚)) = (1 / (2↑(2nd ‘𝑥))))
95	94	oveq2d 7378	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (2nd ‘𝑥) → ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑𝑚))) = ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥)))))
96		heibor.5	. . . . . . . . . . . . . 14 ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))
97		ovex 7395	. . . . . . . . . . . . . 14 ⊢ ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥)))) ∈ V
98	92, 95, 96, 97	ovmpo 7522	. . . . . . . . . . . . 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 25267	. . . . . . . . . . . . . . 15 ⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
103	101, 102	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))
104		metxmet 24313	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
105	103, 104	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
106	105	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝐷 ∈ (∞Met‘𝑋))
107		2nn 12249	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℕ
108		nnexpcl 14031	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℕ ∧ (2nd ‘𝑥) ∈ ℕ0) → (2↑(2nd ‘𝑥)) ∈ ℕ)
109	107, 91, 108	sylancr 588	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (2↑(2nd ‘𝑥)) ∈ ℕ)
110	109	nnrpd 12979	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (2↑(2nd ‘𝑥)) ∈ ℝ+)
111	110	rpreccld 12991	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (1 / (2↑(2nd ‘𝑥))) ∈ ℝ+)
112	111	rpxrd 12982	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (1 / (2↑(2nd ‘𝑥))) ∈ ℝ*)
113		blssm 24397	. . . . . . . . . . . 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 3957	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐵‘𝑥) ⊆ 𝑋)
116		dfss2 3908	. . . . . . . . . 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 3982	. . . . . . 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 6849	. . . . . . . 8 ⊢ (𝐵‘𝑥) ∈ V
126	125	inex1 5255	. . . . . . 7 ⊢ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ V
127	13, 14, 126	heiborlem1 38150	. . . . . 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 3920	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ∈ 𝒫 𝑋)
130	129	elpwid 4551	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ⊆ 𝑋)
131	13	mopnuni 24420	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽)
132	105, 131	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
133	132	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝑋 = ∪ 𝐽)
134	130, 133	sseqtrd 3959	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ⊆ ∪ 𝐽)
135	134	sselda 3922	. . . . . . . . 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 8985	. . . . . . . . . . . 12 ⊢ {(𝑡𝐵((2nd ‘𝑥) + 1))} ∈ Fin
140		inss2 4179	. . . . . . . . . . . . 13 ⊢ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ⊆ (𝑡𝐵((2nd ‘𝑥) + 1))
141		ovex 7395	. . . . . . . . . . . . . . 15 ⊢ (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ V
142	141	unisn 4870	. . . . . . . . . . . . . 14 ⊢ ∪ {(𝑡𝐵((2nd ‘𝑥) + 1))} = (𝑡𝐵((2nd ‘𝑥) + 1))
143		uniiun 5002	. . . . . . . . . . . . . 14 ⊢ ∪ {(𝑡𝐵((2nd ‘𝑥) + 1))} = ∪ 𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔
144	142, 143	eqtr3i 2762	. . . . . . . . . . . . 13 ⊢ (𝑡𝐵((2nd ‘𝑥) + 1)) = ∪ 𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔
145	140, 144	sseqtri 3971	. . . . . . . . . . . 12 ⊢ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ⊆ ∪ 𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔
146		vex 3434	. . . . . . . . . . . . 13 ⊢ 𝑔 ∈ V
147	13, 14, 146	heiborlem1 38150	. . . . . . . . . . . 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 4627	. . . . . . . . . . 11 ⊢ (∃𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔 ∈ 𝐾 ↔ (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ 𝐾)
151	148, 150	sylib 218	. . . . . . . . . 10 ⊢ (((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 → (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ 𝐾)
152		ovex 7395	. . . . . . . . . . . 12 ⊢ ((2nd ‘𝑥) + 1) ∈ V
153	13, 14, 6, 42, 152	heiborlem2 38151	. . . . . . . . . . 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 3148	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (∃𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 → ∃𝑡 ∈ ∪ 𝐽(𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)))
161	128, 160	mpd 15	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ∃𝑡 ∈ ∪ 𝐽(𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))
162	161	ralrimiva 3130	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ∃𝑡 ∈ ∪ 𝐽(𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))
163	13	fvexi 6850	. . . . 5 ⊢ 𝐽 ∈ V
164	163	uniex 7690	. . . 4 ⊢ ∪ 𝐽 ∈ V
165		breq1 5089	. . . . 5 ⊢ (𝑡 = (𝑔‘𝑥) → (𝑡𝐺((2nd ‘𝑥) + 1) ↔ (𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1)))
166		oveq1 7369	. . . . . . 7 ⊢ (𝑡 = (𝑔‘𝑥) → (𝑡𝐵((2nd ‘𝑥) + 1)) = ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1)))
167	166	ineq2d 4161	. . . . . 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 10358	. . 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 3062  Vcvv 3430   ∩ cin 3889   ⊆ wss 3890  𝒫 cpw 4542  {csn 4568  ⟨cop 4574  ∪ cuni 4851  ∪ ciun 4934   class class class wbr 5086  {copab 5148   × cxp 5624  Rel wrel 5631  ⟶wf 6490  ‘cfv 6494  (class class class)co 7362   ∈ cmpo 7364  ωcom 7812  1^st c1st 7935  2^nd c2nd 7936   ≈ cen 8885   ≼ cdom 8886   ≺ csdm 8887  Fincfn 8888  1c1 11034   + caddc 11036  ℝ^*cxr 11173   / cdiv 11802  ℕcn 12169  2c2 12231  ℕ₀cn0 12432  ↑cexp 14018  ∞Metcxmet 21333  Metcmet 21334  ballcbl 21335  MetOpencmopn 21338  CMetccmet 25235

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 5213  ax-sep 5232  ax-nul 5242  ax-pow 5304  ax-pr 5372  ax-un 7684  ax-inf2 9557  ax-cc 10352  ax-cnex 11089  ax-resscn 11090  ax-1cn 11091  ax-icn 11092  ax-addcl 11093  ax-addrcl 11094  ax-mulcl 11095  ax-mulrcl 11096  ax-mulcom 11097  ax-addass 11098  ax-mulass 11099  ax-distr 11100  ax-i2m1 11101  ax-1ne0 11102  ax-1rid 11103  ax-rnegex 11104  ax-rrecex 11105  ax-cnre 11106  ax-pre-lttri 11107  ax-pre-lttrn 11108  ax-pre-ltadd 11109  ax-pre-mulgt0 11110  ax-pre-sup 11111

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 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5521  df-eprel 5526  df-po 5534  df-so 5535  df-fr 5579  df-se 5580  df-we 5581  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-rn 5637  df-res 5638  df-ima 5639  df-pred 6261  df-ord 6322  df-on 6323  df-lim 6324  df-suc 6325  df-iota 6450  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-isom 6503  df-riota 7319  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7813  df-1st 7937  df-2nd 7938  df-frecs 8226  df-wrecs 8257  df-recs 8306  df-rdg 8344  df-1o 8400  df-er 8638  df-map 8770  df-en 8889  df-dom 8890  df-sdom 8891  df-fin 8892  df-sup 9350  df-inf 9351  df-oi 9420  df-card 9858  df-acn 9861  df-pnf 11176  df-mnf 11177  df-xr 11178  df-ltxr 11179  df-le 11180  df-sub 11374  df-neg 11375  df-div 11803  df-nn 12170  df-2 12239  df-n0 12433  df-z 12520  df-uz 12784  df-q 12894  df-rp 12938  df-xneg 13058  df-xadd 13059  df-xmul 13060  df-seq 13959  df-exp 14019  df-topgen 17401  df-psmet 21340  df-xmet 21341  df-met 21342  df-bl 21343  df-mopn 21344  df-top 22873  df-topon 22890  df-bases 22925  df-cmet 25238

This theorem is referenced by:  heiborlem10  38159