Theorem heiborlem3 36676

Description: Lemma for heibor 36684. Using countable choice ax-cc 10429, 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 36674 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 10429 via iunctb 10568), and so we can apply ax-cc 10429 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 12477	. . . . . 6 ⊢ ℕ0 ∈ V
2		fvex 6904	. . . . . . 7 ⊢ (𝐹‘𝑡) ∈ V
3		vsnex 5429	. . . . . . 7 ⊢ {𝑡} ∈ V
4	2, 3	xpex 7739	. . . . . 6 ⊢ ((𝐹‘𝑡) × {𝑡}) ∈ V
5	1, 4	iunex 7954	. . . . 5 ⊢ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ∈ V
6		heibor.4	. . . . . . . . 9 ⊢ 𝐺 = {⟨𝑦, 𝑛⟩ ∣ (𝑛 ∈ ℕ0 ∧ 𝑦 ∈ (𝐹‘𝑛) ∧ (𝑦𝐵𝑛) ∈ 𝐾)}
7	6	relopabiv 5820	. . . . . . . 8 ⊢ Rel 𝐺
8		1st2nd 8024	. . . . . . . 8 ⊢ ((Rel 𝐺 ∧ 𝑥 ∈ 𝐺) → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
9	7, 8	mpan 688	. . . . . . 7 ⊢ (𝑥 ∈ 𝐺 → 𝑥 = ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
10	9	eleq1d 2818	. . . . . . . . . . 11 ⊢ (𝑥 ∈ 𝐺 → (𝑥 ∈ 𝐺 ↔ ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ 𝐺))
11		df-br 5149	. . . . . . . . . . 11 ⊢ ((1st ‘𝑥)𝐺(2nd ‘𝑥) ↔ ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ 𝐺)
12	10, 11	bitr4di 288	. . . . . . . . . 10 ⊢ (𝑥 ∈ 𝐺 → (𝑥 ∈ 𝐺 ↔ (1st ‘𝑥)𝐺(2nd ‘𝑥)))
13		heibor.1	. . . . . . . . . . 11 ⊢ 𝐽 = (MetOpen‘𝐷)
14		heibor.3	. . . . . . . . . . 11 ⊢ 𝐾 = {𝑢 ∣ ¬ ∃𝑣 ∈ (𝒫 𝑈 ∩ Fin)𝑢 ⊆ ∪ 𝑣}
15		fvex 6904	. . . . . . . . . . 11 ⊢ (1st ‘𝑥) ∈ V
16		fvex 6904	. . . . . . . . . . 11 ⊢ (2nd ‘𝑥) ∈ V
17	13, 14, 6, 15, 16	heiborlem2 36675	. . . . . . . . . 10 ⊢ ((1st ‘𝑥)𝐺(2nd ‘𝑥) ↔ ((2nd ‘𝑥) ∈ ℕ0 ∧ (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)) ∧ ((1st ‘𝑥)𝐵(2nd ‘𝑥)) ∈ 𝐾))
18	12, 17	bitrdi 286	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐺 → (𝑥 ∈ 𝐺 ↔ ((2nd ‘𝑥) ∈ ℕ0 ∧ (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)) ∧ ((1st ‘𝑥)𝐵(2nd ‘𝑥)) ∈ 𝐾)))
19	18	ibi 266	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐺 → ((2nd ‘𝑥) ∈ ℕ0 ∧ (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)) ∧ ((1st ‘𝑥)𝐵(2nd ‘𝑥)) ∈ 𝐾))
20	16	snid 4664	. . . . . . . . . . . 12 ⊢ (2nd ‘𝑥) ∈ {(2nd ‘𝑥)}
21		opelxp 5712	. . . . . . . . . . . 12 ⊢ (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ((𝐹‘(2nd ‘𝑥)) × {(2nd ‘𝑥)}) ↔ ((1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)) ∧ (2nd ‘𝑥) ∈ {(2nd ‘𝑥)}))
22	20, 21	mpbiran2 708	. . . . . . . . . . 11 ⊢ (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ((𝐹‘(2nd ‘𝑥)) × {(2nd ‘𝑥)}) ↔ (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)))
23		fveq2 6891	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (2nd ‘𝑥) → (𝐹‘𝑡) = (𝐹‘(2nd ‘𝑥)))
24		sneq 4638	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (2nd ‘𝑥) → {𝑡} = {(2nd ‘𝑥)})
25	23, 24	xpeq12d 5707	. . . . . . . . . . . . 13 ⊢ (𝑡 = (2nd ‘𝑥) → ((𝐹‘𝑡) × {𝑡}) = ((𝐹‘(2nd ‘𝑥)) × {(2nd ‘𝑥)}))
26	25	eleq2d 2819	. . . . . . . . . . . 12 ⊢ (𝑡 = (2nd ‘𝑥) → (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ((𝐹‘𝑡) × {𝑡}) ↔ ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ((𝐹‘(2nd ‘𝑥)) × {(2nd ‘𝑥)})))
27	26	rspcev 3612	. . . . . . . . . . 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 5001	. . . . . . . . . 10 ⊢ (⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ↔ ∃𝑡 ∈ ℕ0 ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ ((𝐹‘𝑡) × {𝑡}))
30	28, 29	sylibr 233	. . . . . . . . 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 2833	. . . . . 6 ⊢ (𝑥 ∈ 𝐺 → 𝑥 ∈ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}))
34	33	ssriv 3986	. . . . 5 ⊢ 𝐺 ⊆ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡})
35		ssdomg 8995	. . . . 5 ⊢ (∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ∈ V → (𝐺 ⊆ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) → 𝐺 ≼ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡})))
36	5, 34, 35	mp2 9	. . . 4 ⊢ 𝐺 ≼ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡})
37		nn0ennn 13943	. . . . . . 7 ⊢ ℕ0 ≈ ℕ
38		nnenom 13944	. . . . . . 7 ⊢ ℕ ≈ ω
39	37, 38	entri 9003	. . . . . 6 ⊢ ℕ0 ≈ ω
40		endom 8974	. . . . . 6 ⊢ (ℕ0 ≈ ω → ℕ0 ≼ ω)
41	39, 40	ax-mp 5	. . . . 5 ⊢ ℕ0 ≼ ω
42		vex 3478	. . . . . . . 8 ⊢ 𝑡 ∈ V
43	2, 42	xpsnen 9054	. . . . . . 7 ⊢ ((𝐹‘𝑡) × {𝑡}) ≈ (𝐹‘𝑡)
44		inss2 4229	. . . . . . . . 9 ⊢ (𝒫 𝑋 ∩ Fin) ⊆ Fin
45		heibor.7	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin))
46	45	ffvelcdmda 7086	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑡 ∈ ℕ0) → (𝐹‘𝑡) ∈ (𝒫 𝑋 ∩ Fin))
47	44, 46	sselid 3980	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑡 ∈ ℕ0) → (𝐹‘𝑡) ∈ Fin)
48		isfinite 9646	. . . . . . . . 9 ⊢ ((𝐹‘𝑡) ∈ Fin ↔ (𝐹‘𝑡) ≺ ω)
49		sdomdom 8975	. . . . . . . . 9 ⊢ ((𝐹‘𝑡) ≺ ω → (𝐹‘𝑡) ≼ ω)
50	48, 49	sylbi 216	. . . . . . . 8 ⊢ ((𝐹‘𝑡) ∈ Fin → (𝐹‘𝑡) ≼ ω)
51	47, 50	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑡 ∈ ℕ0) → (𝐹‘𝑡) ≼ ω)
52		endomtr 9007	. . . . . . 7 ⊢ ((((𝐹‘𝑡) × {𝑡}) ≈ (𝐹‘𝑡) ∧ (𝐹‘𝑡) ≼ ω) → ((𝐹‘𝑡) × {𝑡}) ≼ ω)
53	43, 51, 52	sylancr 587	. . . . . 6 ⊢ ((𝜑 ∧ 𝑡 ∈ ℕ0) → ((𝐹‘𝑡) × {𝑡}) ≼ ω)
54	53	ralrimiva 3146	. . . . 5 ⊢ (𝜑 → ∀𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω)
55		iunctb 10568	. . . . 5 ⊢ ((ℕ0 ≼ ω ∧ ∀𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω) → ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω)
56	41, 54, 55	sylancr 587	. . . 4 ⊢ (𝜑 → ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω)
57		domtr 9002	. . . 4 ⊢ ((𝐺 ≼ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ∧ ∪ 𝑡 ∈ ℕ0 ((𝐹‘𝑡) × {𝑡}) ≼ ω) → 𝐺 ≼ ω)
58	36, 56, 57	sylancr 587	. . 3 ⊢ (𝜑 → 𝐺 ≼ ω)
59	19	simp1d 1142	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐺 → (2nd ‘𝑥) ∈ ℕ0)
60		peano2nn0 12511	. . . . . . . . 9 ⊢ ((2nd ‘𝑥) ∈ ℕ0 → ((2nd ‘𝑥) + 1) ∈ ℕ0)
61	59, 60	syl 17	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐺 → ((2nd ‘𝑥) + 1) ∈ ℕ0)
62		ffvelcdm 7083	. . . . . . . 8 ⊢ ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧ ((2nd ‘𝑥) + 1) ∈ ℕ0) → (𝐹‘((2nd ‘𝑥) + 1)) ∈ (𝒫 𝑋 ∩ Fin))
63	45, 61, 62	syl2an 596	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ∈ (𝒫 𝑋 ∩ Fin))
64	44, 63	sselid 3980	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ∈ Fin)
65		iunin2 5074	. . . . . . . 8 ⊢ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) = ((𝐵‘𝑥) ∩ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1)))
66		heibor.8	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛))
67		oveq1 7415	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑡 → (𝑦𝐵𝑛) = (𝑡𝐵𝑛))
68	67	cbviunv 5043	. . . . . . . . . . . . . . 15 ⊢ ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘𝑛)(𝑡𝐵𝑛)
69		fveq2 6891	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → (𝐹‘𝑛) = (𝐹‘((2nd ‘𝑥) + 1)))
70	69	iuneq1d 5024	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → ∪ 𝑡 ∈ (𝐹‘𝑛)(𝑡𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵𝑛))
71	68, 70	eqtrid 2784	. . . . . . . . . . . . . 14 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵𝑛))
72		oveq2 7416	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → (𝑡𝐵𝑛) = (𝑡𝐵((2nd ‘𝑥) + 1)))
73	72	iuneq2d 5026	. . . . . . . . . . . . . 14 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1)))
74	71, 73	eqtrd 2772	. . . . . . . . . . . . 13 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1)))
75	74	eqeq2d 2743	. . . . . . . . . . . 12 ⊢ (𝑛 = ((2nd ‘𝑥) + 1) → (𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) ↔ 𝑋 = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1))))
76	75	rspccva 3611	. . . . . . . . . . 11 ⊢ ((∀𝑛 ∈ ℕ0 𝑋 = ∪ 𝑦 ∈ (𝐹‘𝑛)(𝑦𝐵𝑛) ∧ ((2nd ‘𝑥) + 1) ∈ ℕ0) → 𝑋 = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1)))
77	66, 61, 76	syl2an 596	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝑋 = ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1)))
78	77	ineq2d 4212	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((𝐵‘𝑥) ∩ 𝑋) = ((𝐵‘𝑥) ∩ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1))))
79	9	fveq2d 6895	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ 𝐺 → (𝐵‘𝑥) = (𝐵‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩))
80		df-ov 7411	. . . . . . . . . . . . . 14 ⊢ ((1st ‘𝑥)𝐵(2nd ‘𝑥)) = (𝐵‘⟨(1st ‘𝑥), (2nd ‘𝑥)⟩)
81	79, 80	eqtr4di 2790	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐺 → (𝐵‘𝑥) = ((1st ‘𝑥)𝐵(2nd ‘𝑥)))
82	81	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐵‘𝑥) = ((1st ‘𝑥)𝐵(2nd ‘𝑥)))
83		inss1 4228	. . . . . . . . . . . . . . . 16 ⊢ (𝒫 𝑋 ∩ Fin) ⊆ 𝒫 𝑋
84		ffvelcdm 7083	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:ℕ0⟶(𝒫 𝑋 ∩ Fin) ∧ (2nd ‘𝑥) ∈ ℕ0) → (𝐹‘(2nd ‘𝑥)) ∈ (𝒫 𝑋 ∩ Fin))
85	45, 59, 84	syl2an 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘(2nd ‘𝑥)) ∈ (𝒫 𝑋 ∩ Fin))
86	83, 85	sselid 3980	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘(2nd ‘𝑥)) ∈ 𝒫 𝑋)
87	86	elpwid 4611	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘(2nd ‘𝑥)) ⊆ 𝑋)
88	19	simp2d 1143	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝐺 → (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)))
89	88	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (1st ‘𝑥) ∈ (𝐹‘(2nd ‘𝑥)))
90	87, 89	sseldd 3983	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (1st ‘𝑥) ∈ 𝑋)
91	59	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (2nd ‘𝑥) ∈ ℕ0)
92		oveq1 7415	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (1st ‘𝑥) → (𝑧(ball‘𝐷)(1 / (2↑𝑚))) = ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑𝑚))))
93		oveq2 7416	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 = (2nd ‘𝑥) → (2↑𝑚) = (2↑(2nd ‘𝑥)))
94	93	oveq2d 7424	. . . . . . . . . . . . . . 15 ⊢ (𝑚 = (2nd ‘𝑥) → (1 / (2↑𝑚)) = (1 / (2↑(2nd ‘𝑥))))
95	94	oveq2d 7424	. . . . . . . . . . . . . 14 ⊢ (𝑚 = (2nd ‘𝑥) → ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑𝑚))) = ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥)))))
96		heibor.5	. . . . . . . . . . . . . 14 ⊢ 𝐵 = (𝑧 ∈ 𝑋, 𝑚 ∈ ℕ0 ↦ (𝑧(ball‘𝐷)(1 / (2↑𝑚))))
97		ovex 7441	. . . . . . . . . . . . . 14 ⊢ ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥)))) ∈ V
98	92, 95, 96, 97	ovmpo 7567	. . . . . . . . . . . . 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 2772	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐵‘𝑥) = ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥)))))
101		heibor.6	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))
102		cmetmet 24802	. . . . . . . . . . . . . . 15 ⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋))
103	101, 102	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))
104		metxmet 23839	. . . . . . . . . . . . . 14 ⊢ (𝐷 ∈ (Met‘𝑋) → 𝐷 ∈ (∞Met‘𝑋))
105	103, 104	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))
106	105	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝐷 ∈ (∞Met‘𝑋))
107		2nn 12284	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℕ
108		nnexpcl 14039	. . . . . . . . . . . . . . . 16 ⊢ ((2 ∈ ℕ ∧ (2nd ‘𝑥) ∈ ℕ0) → (2↑(2nd ‘𝑥)) ∈ ℕ)
109	107, 91, 108	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (2↑(2nd ‘𝑥)) ∈ ℕ)
110	109	nnrpd 13013	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (2↑(2nd ‘𝑥)) ∈ ℝ+)
111	110	rpreccld 13025	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (1 / (2↑(2nd ‘𝑥))) ∈ ℝ+)
112	111	rpxrd 13016	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (1 / (2↑(2nd ‘𝑥))) ∈ ℝ*)
113		blssm 23923	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (1st ‘𝑥) ∈ 𝑋 ∧ (1 / (2↑(2nd ‘𝑥))) ∈ ℝ*) → ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥)))) ⊆ 𝑋)
114	106, 90, 112, 113	syl3anc 1371	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((1st ‘𝑥)(ball‘𝐷)(1 / (2↑(2nd ‘𝑥)))) ⊆ 𝑋)
115	100, 114	eqsstrd 4020	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐵‘𝑥) ⊆ 𝑋)
116		df-ss 3965	. . . . . . . . . 10 ⊢ ((𝐵‘𝑥) ⊆ 𝑋 ↔ ((𝐵‘𝑥) ∩ 𝑋) = (𝐵‘𝑥))
117	115, 116	sylib 217	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((𝐵‘𝑥) ∩ 𝑋) = (𝐵‘𝑥))
118	78, 117	eqtr3d 2774	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((𝐵‘𝑥) ∩ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))(𝑡𝐵((2nd ‘𝑥) + 1))) = (𝐵‘𝑥))
119	65, 118	eqtrid 2784	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) = (𝐵‘𝑥))
120		eqimss2 4041	. . . . . . 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 2833	. . . . . . 7 ⊢ (𝑥 ∈ 𝐺 → (𝐵‘𝑥) ∈ 𝐾)
124	123	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐵‘𝑥) ∈ 𝐾)
125		fvex 6904	. . . . . . . 8 ⊢ (𝐵‘𝑥) ∈ V
126	125	inex1 5317	. . . . . . 7 ⊢ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ V
127	13, 14, 126	heiborlem1 36674	. . . . . 6 ⊢ (((𝐹‘((2nd ‘𝑥) + 1)) ∈ Fin ∧ (𝐵‘𝑥) ⊆ ∪ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∧ (𝐵‘𝑥) ∈ 𝐾) → ∃𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)
128	64, 121, 124, 127	syl3anc 1371	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ∃𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)
129	83, 63	sselid 3980	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ∈ 𝒫 𝑋)
130	129	elpwid 4611	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ⊆ 𝑋)
131	13	mopnuni 23946	. . . . . . . . . . . . 13 ⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽)
132	105, 131	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 = ∪ 𝐽)
133	132	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → 𝑋 = ∪ 𝐽)
134	130, 133	sseqtrd 4022	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (𝐹‘((2nd ‘𝑥) + 1)) ⊆ ∪ 𝐽)
135	134	sselda 3982	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))) → 𝑡 ∈ ∪ 𝐽)
136	135	adantrr 715	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ (𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) → 𝑡 ∈ ∪ 𝐽)
137	61	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((2nd ‘𝑥) + 1) ∈ ℕ0)
138		id 22	. . . . . . . . . 10 ⊢ (𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)) → 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)))
139		snfi 9043	. . . . . . . . . . . 12 ⊢ {(𝑡𝐵((2nd ‘𝑥) + 1))} ∈ Fin
140		inss2 4229	. . . . . . . . . . . . 13 ⊢ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ⊆ (𝑡𝐵((2nd ‘𝑥) + 1))
141		ovex 7441	. . . . . . . . . . . . . . 15 ⊢ (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ V
142	141	unisn 4930	. . . . . . . . . . . . . 14 ⊢ ∪ {(𝑡𝐵((2nd ‘𝑥) + 1))} = (𝑡𝐵((2nd ‘𝑥) + 1))
143		uniiun 5061	. . . . . . . . . . . . . 14 ⊢ ∪ {(𝑡𝐵((2nd ‘𝑥) + 1))} = ∪ 𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔
144	142, 143	eqtr3i 2762	. . . . . . . . . . . . 13 ⊢ (𝑡𝐵((2nd ‘𝑥) + 1)) = ∪ 𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔
145	140, 144	sseqtri 4018	. . . . . . . . . . . 12 ⊢ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ⊆ ∪ 𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔
146		vex 3478	. . . . . . . . . . . . 13 ⊢ 𝑔 ∈ V
147	13, 14, 146	heiborlem1 36674	. . . . . . . . . . . 12 ⊢ (({(𝑡𝐵((2nd ‘𝑥) + 1))} ∈ Fin ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ⊆ ∪ 𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔 ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) → ∃𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔 ∈ 𝐾)
148	139, 145, 147	mp3an12 1451	. . . . . . . . . . 11 ⊢ (((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 → ∃𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔 ∈ 𝐾)
149		eleq1 2821	. . . . . . . . . . . 12 ⊢ (𝑔 = (𝑡𝐵((2nd ‘𝑥) + 1)) → (𝑔 ∈ 𝐾 ↔ (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ 𝐾))
150	141, 149	rexsn 4686	. . . . . . . . . . 11 ⊢ (∃𝑔 ∈ {(𝑡𝐵((2nd ‘𝑥) + 1))}𝑔 ∈ 𝐾 ↔ (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ 𝐾)
151	148, 150	sylib 217	. . . . . . . . . 10 ⊢ (((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 → (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ 𝐾)
152		ovex 7441	. . . . . . . . . . . 12 ⊢ ((2nd ‘𝑥) + 1) ∈ V
153	13, 14, 6, 42, 152	heiborlem2 36675	. . . . . . . . . . 11 ⊢ (𝑡𝐺((2nd ‘𝑥) + 1) ↔ (((2nd ‘𝑥) + 1) ∈ ℕ0 ∧ 𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)) ∧ (𝑡𝐵((2nd ‘𝑥) + 1)) ∈ 𝐾))
154	153	biimpri 227	. . . . . . . . . 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 771	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ (𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) → ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)
158	136, 156, 157	jca32 516	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐺) ∧ (𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) → (𝑡 ∈ ∪ 𝐽 ∧ (𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)))
159	158	ex 413	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ((𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1)) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) → (𝑡 ∈ ∪ 𝐽 ∧ (𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))))
160	159	reximdv2 3164	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → (∃𝑡 ∈ (𝐹‘((2nd ‘𝑥) + 1))((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 → ∃𝑡 ∈ ∪ 𝐽(𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)))
161	128, 160	mpd 15	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐺) → ∃𝑡 ∈ ∪ 𝐽(𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))
162	161	ralrimiva 3146	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝐺 ∃𝑡 ∈ ∪ 𝐽(𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))
163	13	fvexi 6905	. . . . 5 ⊢ 𝐽 ∈ V
164	163	uniex 7730	. . . 4 ⊢ ∪ 𝐽 ∈ V
165		breq1 5151	. . . . 5 ⊢ (𝑡 = (𝑔‘𝑥) → (𝑡𝐺((2nd ‘𝑥) + 1) ↔ (𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1)))
166		oveq1 7415	. . . . . . 7 ⊢ (𝑡 = (𝑔‘𝑥) → (𝑡𝐵((2nd ‘𝑥) + 1)) = ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1)))
167	166	ineq2d 4212	. . . . . 6 ⊢ (𝑡 = (𝑔‘𝑥) → ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) = ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))))
168	167	eleq1d 2818	. . . . 5 ⊢ (𝑡 = (𝑔‘𝑥) → (((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾 ↔ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾))
169	165, 168	anbi12d 631	. . . 4 ⊢ (𝑡 = (𝑔‘𝑥) → ((𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾) ↔ ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)))
170	164, 169	axcc4dom 10435	. . 3 ⊢ ((𝐺 ≼ ω ∧ ∀𝑥 ∈ 𝐺 ∃𝑡 ∈ ∪ 𝐽(𝑡𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ (𝑡𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)) → ∃𝑔(𝑔:𝐺⟶∪ 𝐽 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)))
171	58, 162, 170	syl2anc 584	. 2 ⊢ (𝜑 → ∃𝑔(𝑔:𝐺⟶∪ 𝐽 ∧ ∀𝑥 ∈ 𝐺 ((𝑔‘𝑥)𝐺((2nd ‘𝑥) + 1) ∧ ((𝐵‘𝑥) ∩ ((𝑔‘𝑥)𝐵((2nd ‘𝑥) + 1))) ∈ 𝐾)))
172		exsimpr 1872	. 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 396   ∧ w3a 1087   = wceq 1541  ∃wex 1781   ∈ wcel 2106  {cab 2709  ∀wral 3061  ∃wrex 3070  Vcvv 3474   ∩ cin 3947   ⊆ wss 3948  𝒫 cpw 4602  {csn 4628  ⟨cop 4634  ∪ cuni 4908  ∪ ciun 4997   class class class wbr 5148  {copab 5210   × cxp 5674  Rel wrel 5681  ⟶wf 6539  ‘cfv 6543  (class class class)co 7408   ∈ cmpo 7410  ωcom 7854  1^st c1st 7972  2^nd c2nd 7973   ≈ cen 8935   ≼ cdom 8936   ≺ csdm 8937  Fincfn 8938  1c1 11110   + caddc 11112  ℝ^*cxr 11246   / cdiv 11870  ℕcn 12211  2c2 12266  ℕ₀cn0 12471  ↑cexp 14026  ∞Metcxmet 20928  Metcmet 20929  ballcbl 20930  MetOpencmopn 20933  CMetccmet 24770

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-inf2 9635  ax-cc 10429  ax-cnex 11165  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186  ax-pre-sup 11187

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7364  df-ov 7411  df-oprab 7412  df-mpo 7413  df-om 7855  df-1st 7974  df-2nd 7975  df-frecs 8265  df-wrecs 8296  df-recs 8370  df-rdg 8409  df-1o 8465  df-er 8702  df-map 8821  df-en 8939  df-dom 8940  df-sdom 8941  df-fin 8942  df-sup 9436  df-inf 9437  df-oi 9504  df-card 9933  df-acn 9936  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11445  df-neg 11446  df-div 11871  df-nn 12212  df-2 12274  df-n0 12472  df-z 12558  df-uz 12822  df-q 12932  df-rp 12974  df-xneg 13091  df-xadd 13092  df-xmul 13093  df-seq 13966  df-exp 14027  df-topgen 17388  df-psmet 20935  df-xmet 20936  df-met 20937  df-bl 20938  df-mopn 20939  df-top 22395  df-topon 22412  df-bases 22448  df-cmet 24773

This theorem is referenced by:  heiborlem10  36683