heiborlem3

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

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

Proof

Step	Hyp	Ref	Expression
1		heibor.1	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2		heibor.3	⊢ 𝐾 = { 𝑢 ∣ ¬ ∃ 𝑣 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑢 ⊆ ∪ 𝑣 }
3		heibor.4	⊢ 𝐺 = { ⟨ 𝑦 , 𝑛 ⟩ ∣ ( 𝑛 ∈ ℕ₀ ∧ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ∧ ( 𝑦 𝐵 𝑛 ) ∈ 𝐾 ) }
4		heibor.5	⊢ 𝐵 = ( 𝑧 ∈ 𝑋 , 𝑚 ∈ ℕ₀ ↦ ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) )
5		heibor.6	⊢ ( 𝜑 → 𝐷 ∈ ( CMet ‘ 𝑋 ) )
6		heibor.7	⊢ ( 𝜑 → 𝐹 : ℕ₀ ⟶ ( 𝒫 𝑋 ∩ Fin ) )
7		heibor.8	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ₀ 𝑋 = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ( 𝑦 𝐵 𝑛 ) )
8		nn0ex	⊢ ℕ₀ ∈ V
9		fvex	⊢ ( 𝐹 ‘ 𝑡 ) ∈ V
10		snex	⊢ { 𝑡 } ∈ V
11	9 10	xpex	⊢ ( ( 𝐹 ‘ 𝑡 ) × { 𝑡 } ) ∈ V
12	8 11	iunex	⊢ ∪ 𝑡 ∈ ℕ₀ ( ( 𝐹 ‘ 𝑡 ) × { 𝑡 } ) ∈ V
13	3	relopabiv	⊢ Rel 𝐺
14		1st2nd	⊢ ( ( Rel 𝐺 ∧ 𝑥 ∈ 𝐺 ) → 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
15	13 14	mpan	⊢ ( 𝑥 ∈ 𝐺 → 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
16	15	eleq1d	⊢ ( 𝑥 ∈ 𝐺 → ( 𝑥 ∈ 𝐺 ↔ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∈ 𝐺 ) )
17		df-br	⊢ ( ( 1^st ‘ 𝑥 ) 𝐺 ( 2^nd ‘ 𝑥 ) ↔ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∈ 𝐺 )
18	16 17	bitr4di	⊢ ( 𝑥 ∈ 𝐺 → ( 𝑥 ∈ 𝐺 ↔ ( 1^st ‘ 𝑥 ) 𝐺 ( 2^nd ‘ 𝑥 ) ) )
19		fvex	⊢ ( 1^st ‘ 𝑥 ) ∈ V
20		fvex	⊢ ( 2^nd ‘ 𝑥 ) ∈ V
21	1 2 3 19 20	heiborlem2	⊢ ( ( 1^st ‘ 𝑥 ) 𝐺 ( 2^nd ‘ 𝑥 ) ↔ ( ( 2^nd ‘ 𝑥 ) ∈ ℕ₀ ∧ ( 1^st ‘ 𝑥 ) ∈ ( 𝐹 ‘ ( 2^nd ‘ 𝑥 ) ) ∧ ( ( 1^st ‘ 𝑥 ) 𝐵 ( 2^nd ‘ 𝑥 ) ) ∈ 𝐾 ) )
22	18 21	bitrdi	⊢ ( 𝑥 ∈ 𝐺 → ( 𝑥 ∈ 𝐺 ↔ ( ( 2^nd ‘ 𝑥 ) ∈ ℕ₀ ∧ ( 1^st ‘ 𝑥 ) ∈ ( 𝐹 ‘ ( 2^nd ‘ 𝑥 ) ) ∧ ( ( 1^st ‘ 𝑥 ) 𝐵 ( 2^nd ‘ 𝑥 ) ) ∈ 𝐾 ) ) )
23	22	ibi	⊢ ( 𝑥 ∈ 𝐺 → ( ( 2^nd ‘ 𝑥 ) ∈ ℕ₀ ∧ ( 1^st ‘ 𝑥 ) ∈ ( 𝐹 ‘ ( 2^nd ‘ 𝑥 ) ) ∧ ( ( 1^st ‘ 𝑥 ) 𝐵 ( 2^nd ‘ 𝑥 ) ) ∈ 𝐾 ) )
24	20	snid	⊢ ( 2^nd ‘ 𝑥 ) ∈ { ( 2^nd ‘ 𝑥 ) }
25		opelxp	⊢ ( ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∈ ( ( 𝐹 ‘ ( 2^nd ‘ 𝑥 ) ) × { ( 2^nd ‘ 𝑥 ) } ) ↔ ( ( 1^st ‘ 𝑥 ) ∈ ( 𝐹 ‘ ( 2^nd ‘ 𝑥 ) ) ∧ ( 2^nd ‘ 𝑥 ) ∈ { ( 2^nd ‘ 𝑥 ) } ) )
26	24 25	mpbiran2	⊢ ( ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∈ ( ( 𝐹 ‘ ( 2^nd ‘ 𝑥 ) ) × { ( 2^nd ‘ 𝑥 ) } ) ↔ ( 1^st ‘ 𝑥 ) ∈ ( 𝐹 ‘ ( 2^nd ‘ 𝑥 ) ) )
27		fveq2	⊢ ( 𝑡 = ( 2^nd ‘ 𝑥 ) → ( 𝐹 ‘ 𝑡 ) = ( 𝐹 ‘ ( 2^nd ‘ 𝑥 ) ) )
28		sneq	⊢ ( 𝑡 = ( 2^nd ‘ 𝑥 ) → { 𝑡 } = { ( 2^nd ‘ 𝑥 ) } )
29	27 28	xpeq12d	⊢ ( 𝑡 = ( 2^nd ‘ 𝑥 ) → ( ( 𝐹 ‘ 𝑡 ) × { 𝑡 } ) = ( ( 𝐹 ‘ ( 2^nd ‘ 𝑥 ) ) × { ( 2^nd ‘ 𝑥 ) } ) )
30	29	eleq2d	⊢ ( 𝑡 = ( 2^nd ‘ 𝑥 ) → ( ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∈ ( ( 𝐹 ‘ 𝑡 ) × { 𝑡 } ) ↔ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∈ ( ( 𝐹 ‘ ( 2^nd ‘ 𝑥 ) ) × { ( 2^nd ‘ 𝑥 ) } ) ) )
31	30	rspcev	⊢ ( ( ( 2^nd ‘ 𝑥 ) ∈ ℕ₀ ∧ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∈ ( ( 𝐹 ‘ ( 2^nd ‘ 𝑥 ) ) × { ( 2^nd ‘ 𝑥 ) } ) ) → ∃ 𝑡 ∈ ℕ₀ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∈ ( ( 𝐹 ‘ 𝑡 ) × { 𝑡 } ) )
32	26 31	sylan2br	⊢ ( ( ( 2^nd ‘ 𝑥 ) ∈ ℕ₀ ∧ ( 1^st ‘ 𝑥 ) ∈ ( 𝐹 ‘ ( 2^nd ‘ 𝑥 ) ) ) → ∃ 𝑡 ∈ ℕ₀ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∈ ( ( 𝐹 ‘ 𝑡 ) × { 𝑡 } ) )
33		eliun	⊢ ( ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∈ ∪ 𝑡 ∈ ℕ₀ ( ( 𝐹 ‘ 𝑡 ) × { 𝑡 } ) ↔ ∃ 𝑡 ∈ ℕ₀ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∈ ( ( 𝐹 ‘ 𝑡 ) × { 𝑡 } ) )
34	32 33	sylibr	⊢ ( ( ( 2^nd ‘ 𝑥 ) ∈ ℕ₀ ∧ ( 1^st ‘ 𝑥 ) ∈ ( 𝐹 ‘ ( 2^nd ‘ 𝑥 ) ) ) → ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∈ ∪ 𝑡 ∈ ℕ₀ ( ( 𝐹 ‘ 𝑡 ) × { 𝑡 } ) )
35	34	3adant3	⊢ ( ( ( 2^nd ‘ 𝑥 ) ∈ ℕ₀ ∧ ( 1^st ‘ 𝑥 ) ∈ ( 𝐹 ‘ ( 2^nd ‘ 𝑥 ) ) ∧ ( ( 1^st ‘ 𝑥 ) 𝐵 ( 2^nd ‘ 𝑥 ) ) ∈ 𝐾 ) → ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∈ ∪ 𝑡 ∈ ℕ₀ ( ( 𝐹 ‘ 𝑡 ) × { 𝑡 } ) )
36	23 35	syl	⊢ ( 𝑥 ∈ 𝐺 → ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∈ ∪ 𝑡 ∈ ℕ₀ ( ( 𝐹 ‘ 𝑡 ) × { 𝑡 } ) )
37	15 36	eqeltrd	⊢ ( 𝑥 ∈ 𝐺 → 𝑥 ∈ ∪ 𝑡 ∈ ℕ₀ ( ( 𝐹 ‘ 𝑡 ) × { 𝑡 } ) )
38	37	ssriv	⊢ 𝐺 ⊆ ∪ 𝑡 ∈ ℕ₀ ( ( 𝐹 ‘ 𝑡 ) × { 𝑡 } )
39		ssdomg	⊢ ( ∪ 𝑡 ∈ ℕ₀ ( ( 𝐹 ‘ 𝑡 ) × { 𝑡 } ) ∈ V → ( 𝐺 ⊆ ∪ 𝑡 ∈ ℕ₀ ( ( 𝐹 ‘ 𝑡 ) × { 𝑡 } ) → 𝐺 ≼ ∪ 𝑡 ∈ ℕ₀ ( ( 𝐹 ‘ 𝑡 ) × { 𝑡 } ) ) )
40	12 38 39	mp2	⊢ 𝐺 ≼ ∪ 𝑡 ∈ ℕ₀ ( ( 𝐹 ‘ 𝑡 ) × { 𝑡 } )
41		nn0ennn	⊢ ℕ₀ ≈ ℕ
42		nnenom	⊢ ℕ ≈ ω
43	41 42	entri	⊢ ℕ₀ ≈ ω
44		endom	⊢ ( ℕ₀ ≈ ω → ℕ₀ ≼ ω )
45	43 44	ax-mp	⊢ ℕ₀ ≼ ω
46		vex	⊢ 𝑡 ∈ V
47	9 46	xpsnen	⊢ ( ( 𝐹 ‘ 𝑡 ) × { 𝑡 } ) ≈ ( 𝐹 ‘ 𝑡 )
48		inss2	⊢ ( 𝒫 𝑋 ∩ Fin ) ⊆ Fin
49	6	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℕ₀ ) → ( 𝐹 ‘ 𝑡 ) ∈ ( 𝒫 𝑋 ∩ Fin ) )
50	48 49	sseldi	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℕ₀ ) → ( 𝐹 ‘ 𝑡 ) ∈ Fin )
51		isfinite	⊢ ( ( 𝐹 ‘ 𝑡 ) ∈ Fin ↔ ( 𝐹 ‘ 𝑡 ) ≺ ω )
52		sdomdom	⊢ ( ( 𝐹 ‘ 𝑡 ) ≺ ω → ( 𝐹 ‘ 𝑡 ) ≼ ω )
53	51 52	sylbi	⊢ ( ( 𝐹 ‘ 𝑡 ) ∈ Fin → ( 𝐹 ‘ 𝑡 ) ≼ ω )
54	50 53	syl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℕ₀ ) → ( 𝐹 ‘ 𝑡 ) ≼ ω )
55		endomtr	⊢ ( ( ( ( 𝐹 ‘ 𝑡 ) × { 𝑡 } ) ≈ ( 𝐹 ‘ 𝑡 ) ∧ ( 𝐹 ‘ 𝑡 ) ≼ ω ) → ( ( 𝐹 ‘ 𝑡 ) × { 𝑡 } ) ≼ ω )
56	47 54 55	sylancr	⊢ ( ( 𝜑 ∧ 𝑡 ∈ ℕ₀ ) → ( ( 𝐹 ‘ 𝑡 ) × { 𝑡 } ) ≼ ω )
57	56	ralrimiva	⊢ ( 𝜑 → ∀ 𝑡 ∈ ℕ₀ ( ( 𝐹 ‘ 𝑡 ) × { 𝑡 } ) ≼ ω )
58		iunctb	⊢ ( ( ℕ₀ ≼ ω ∧ ∀ 𝑡 ∈ ℕ₀ ( ( 𝐹 ‘ 𝑡 ) × { 𝑡 } ) ≼ ω ) → ∪ 𝑡 ∈ ℕ₀ ( ( 𝐹 ‘ 𝑡 ) × { 𝑡 } ) ≼ ω )
59	45 57 58	sylancr	⊢ ( 𝜑 → ∪ 𝑡 ∈ ℕ₀ ( ( 𝐹 ‘ 𝑡 ) × { 𝑡 } ) ≼ ω )
60		domtr	⊢ ( ( 𝐺 ≼ ∪ 𝑡 ∈ ℕ₀ ( ( 𝐹 ‘ 𝑡 ) × { 𝑡 } ) ∧ ∪ 𝑡 ∈ ℕ₀ ( ( 𝐹 ‘ 𝑡 ) × { 𝑡 } ) ≼ ω ) → 𝐺 ≼ ω )
61	40 59 60	sylancr	⊢ ( 𝜑 → 𝐺 ≼ ω )
62	23	simp1d	⊢ ( 𝑥 ∈ 𝐺 → ( 2^nd ‘ 𝑥 ) ∈ ℕ₀ )
63		peano2nn0	⊢ ( ( 2^nd ‘ 𝑥 ) ∈ ℕ₀ → ( ( 2^nd ‘ 𝑥 ) + 1 ) ∈ ℕ₀ )
64	62 63	syl	⊢ ( 𝑥 ∈ 𝐺 → ( ( 2^nd ‘ 𝑥 ) + 1 ) ∈ ℕ₀ )
65		ffvelrn	⊢ ( ( 𝐹 : ℕ₀ ⟶ ( 𝒫 𝑋 ∩ Fin ) ∧ ( ( 2^nd ‘ 𝑥 ) + 1 ) ∈ ℕ₀ ) → ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ∈ ( 𝒫 𝑋 ∩ Fin ) )
66	6 64 65	syl2an	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ∈ ( 𝒫 𝑋 ∩ Fin ) )
67	48 66	sseldi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ∈ Fin )
68		iunin2	⊢ ∪ 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) = ( ( 𝐵 ‘ 𝑥 ) ∩ ∪ 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) )
69		oveq1	⊢ ( 𝑦 = 𝑡 → ( 𝑦 𝐵 𝑛 ) = ( 𝑡 𝐵 𝑛 ) )
70	69	cbviunv	⊢ ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ( 𝑦 𝐵 𝑛 ) = ∪ 𝑡 ∈ ( 𝐹 ‘ 𝑛 ) ( 𝑡 𝐵 𝑛 )
71		fveq2	⊢ ( 𝑛 = ( ( 2^nd ‘ 𝑥 ) + 1 ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) )
72	71	iuneq1d	⊢ ( 𝑛 = ( ( 2^nd ‘ 𝑥 ) + 1 ) → ∪ 𝑡 ∈ ( 𝐹 ‘ 𝑛 ) ( 𝑡 𝐵 𝑛 ) = ∪ 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ( 𝑡 𝐵 𝑛 ) )
73	70 72	syl5eq	⊢ ( 𝑛 = ( ( 2^nd ‘ 𝑥 ) + 1 ) → ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ( 𝑦 𝐵 𝑛 ) = ∪ 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ( 𝑡 𝐵 𝑛 ) )
74		oveq2	⊢ ( 𝑛 = ( ( 2^nd ‘ 𝑥 ) + 1 ) → ( 𝑡 𝐵 𝑛 ) = ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) )
75	74	iuneq2d	⊢ ( 𝑛 = ( ( 2^nd ‘ 𝑥 ) + 1 ) → ∪ 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ( 𝑡 𝐵 𝑛 ) = ∪ 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) )
76	73 75	eqtrd	⊢ ( 𝑛 = ( ( 2^nd ‘ 𝑥 ) + 1 ) → ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ( 𝑦 𝐵 𝑛 ) = ∪ 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) )
77	76	eqeq2d	⊢ ( 𝑛 = ( ( 2^nd ‘ 𝑥 ) + 1 ) → ( 𝑋 = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ( 𝑦 𝐵 𝑛 ) ↔ 𝑋 = ∪ 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) )
78	77	rspccva	⊢ ( ( ∀ 𝑛 ∈ ℕ₀ 𝑋 = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑛 ) ( 𝑦 𝐵 𝑛 ) ∧ ( ( 2^nd ‘ 𝑥 ) + 1 ) ∈ ℕ₀ ) → 𝑋 = ∪ 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) )
79	7 64 78	syl2an	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → 𝑋 = ∪ 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) )
80	79	ineq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( ( 𝐵 ‘ 𝑥 ) ∩ 𝑋 ) = ( ( 𝐵 ‘ 𝑥 ) ∩ ∪ 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) )
81	15	fveq2d	⊢ ( 𝑥 ∈ 𝐺 → ( 𝐵 ‘ 𝑥 ) = ( 𝐵 ‘ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ) )
82		df-ov	⊢ ( ( 1^st ‘ 𝑥 ) 𝐵 ( 2^nd ‘ 𝑥 ) ) = ( 𝐵 ‘ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
83	81 82	eqtr4di	⊢ ( 𝑥 ∈ 𝐺 → ( 𝐵 ‘ 𝑥 ) = ( ( 1^st ‘ 𝑥 ) 𝐵 ( 2^nd ‘ 𝑥 ) ) )
84	83	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( 𝐵 ‘ 𝑥 ) = ( ( 1^st ‘ 𝑥 ) 𝐵 ( 2^nd ‘ 𝑥 ) ) )
85		inss1	⊢ ( 𝒫 𝑋 ∩ Fin ) ⊆ 𝒫 𝑋
86		ffvelrn	⊢ ( ( 𝐹 : ℕ₀ ⟶ ( 𝒫 𝑋 ∩ Fin ) ∧ ( 2^nd ‘ 𝑥 ) ∈ ℕ₀ ) → ( 𝐹 ‘ ( 2^nd ‘ 𝑥 ) ) ∈ ( 𝒫 𝑋 ∩ Fin ) )
87	6 62 86	syl2an	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( 𝐹 ‘ ( 2^nd ‘ 𝑥 ) ) ∈ ( 𝒫 𝑋 ∩ Fin ) )
88	85 87	sseldi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( 𝐹 ‘ ( 2^nd ‘ 𝑥 ) ) ∈ 𝒫 𝑋 )
89	88	elpwid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( 𝐹 ‘ ( 2^nd ‘ 𝑥 ) ) ⊆ 𝑋 )
90	23	simp2d	⊢ ( 𝑥 ∈ 𝐺 → ( 1^st ‘ 𝑥 ) ∈ ( 𝐹 ‘ ( 2^nd ‘ 𝑥 ) ) )
91	90	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( 1^st ‘ 𝑥 ) ∈ ( 𝐹 ‘ ( 2^nd ‘ 𝑥 ) ) )
92	89 91	sseldd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( 1^st ‘ 𝑥 ) ∈ 𝑋 )
93	62	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( 2^nd ‘ 𝑥 ) ∈ ℕ₀ )
94		oveq1	⊢ ( 𝑧 = ( 1^st ‘ 𝑥 ) → ( 𝑧 ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) = ( ( 1^st ‘ 𝑥 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) )
95		oveq2	⊢ ( 𝑚 = ( 2^nd ‘ 𝑥 ) → ( 2 ↑ 𝑚 ) = ( 2 ↑ ( 2^nd ‘ 𝑥 ) ) )
96	95	oveq2d	⊢ ( 𝑚 = ( 2^nd ‘ 𝑥 ) → ( 1 / ( 2 ↑ 𝑚 ) ) = ( 1 / ( 2 ↑ ( 2^nd ‘ 𝑥 ) ) ) )
97	96	oveq2d	⊢ ( 𝑚 = ( 2^nd ‘ 𝑥 ) → ( ( 1^st ‘ 𝑥 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ 𝑚 ) ) ) = ( ( 1^st ‘ 𝑥 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 2^nd ‘ 𝑥 ) ) ) ) )
98		ovex	⊢ ( ( 1^st ‘ 𝑥 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 2^nd ‘ 𝑥 ) ) ) ) ∈ V
99	94 97 4 98	ovmpo	⊢ ( ( ( 1^st ‘ 𝑥 ) ∈ 𝑋 ∧ ( 2^nd ‘ 𝑥 ) ∈ ℕ₀ ) → ( ( 1^st ‘ 𝑥 ) 𝐵 ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ 𝑥 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 2^nd ‘ 𝑥 ) ) ) ) )
100	92 93 99	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( ( 1^st ‘ 𝑥 ) 𝐵 ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ 𝑥 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 2^nd ‘ 𝑥 ) ) ) ) )
101	84 100	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( 𝐵 ‘ 𝑥 ) = ( ( 1^st ‘ 𝑥 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 2^nd ‘ 𝑥 ) ) ) ) )
102		cmetmet	⊢ ( 𝐷 ∈ ( CMet ‘ 𝑋 ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
103	5 102	syl	⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
104		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
105	103 104	syl	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
106	105	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
107		2nn	⊢ 2 ∈ ℕ
108		nnexpcl	⊢ ( ( 2 ∈ ℕ ∧ ( 2^nd ‘ 𝑥 ) ∈ ℕ₀ ) → ( 2 ↑ ( 2^nd ‘ 𝑥 ) ) ∈ ℕ )
109	107 93 108	sylancr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( 2 ↑ ( 2^nd ‘ 𝑥 ) ) ∈ ℕ )
110	109	nnrpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( 2 ↑ ( 2^nd ‘ 𝑥 ) ) ∈ ℝ⁺ )
111	110	rpreccld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( 1 / ( 2 ↑ ( 2^nd ‘ 𝑥 ) ) ) ∈ ℝ⁺ )
112	111	rpxrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( 1 / ( 2 ↑ ( 2^nd ‘ 𝑥 ) ) ) ∈ ℝ^* )
113		blssm	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ ( 1^st ‘ 𝑥 ) ∈ 𝑋 ∧ ( 1 / ( 2 ↑ ( 2^nd ‘ 𝑥 ) ) ) ∈ ℝ^* ) → ( ( 1^st ‘ 𝑥 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 2^nd ‘ 𝑥 ) ) ) ) ⊆ 𝑋 )
114	106 92 112 113	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( ( 1^st ‘ 𝑥 ) ( ball ‘ 𝐷 ) ( 1 / ( 2 ↑ ( 2^nd ‘ 𝑥 ) ) ) ) ⊆ 𝑋 )
115	101 114	eqsstrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( 𝐵 ‘ 𝑥 ) ⊆ 𝑋 )
116		df-ss	⊢ ( ( 𝐵 ‘ 𝑥 ) ⊆ 𝑋 ↔ ( ( 𝐵 ‘ 𝑥 ) ∩ 𝑋 ) = ( 𝐵 ‘ 𝑥 ) )
117	115 116	sylib	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( ( 𝐵 ‘ 𝑥 ) ∩ 𝑋 ) = ( 𝐵 ‘ 𝑥 ) )
118	80 117	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( ( 𝐵 ‘ 𝑥 ) ∩ ∪ 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) = ( 𝐵 ‘ 𝑥 ) )
119	68 118	syl5eq	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ∪ 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) = ( 𝐵 ‘ 𝑥 ) )
120		eqimss2	⊢ ( ∪ 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) = ( 𝐵 ‘ 𝑥 ) → ( 𝐵 ‘ 𝑥 ) ⊆ ∪ 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) )
121	119 120	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( 𝐵 ‘ 𝑥 ) ⊆ ∪ 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) )
122	23	simp3d	⊢ ( 𝑥 ∈ 𝐺 → ( ( 1^st ‘ 𝑥 ) 𝐵 ( 2^nd ‘ 𝑥 ) ) ∈ 𝐾 )
123	83 122	eqeltrd	⊢ ( 𝑥 ∈ 𝐺 → ( 𝐵 ‘ 𝑥 ) ∈ 𝐾 )
124	123	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( 𝐵 ‘ 𝑥 ) ∈ 𝐾 )
125		fvex	⊢ ( 𝐵 ‘ 𝑥 ) ∈ V
126	125	inex1	⊢ ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ V
127	1 2 126	heiborlem1	⊢ ( ( ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ∈ Fin ∧ ( 𝐵 ‘ 𝑥 ) ⊆ ∪ 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∧ ( 𝐵 ‘ 𝑥 ) ∈ 𝐾 ) → ∃ 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 )
128	67 121 124 127	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ∃ 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 )
129	85 66	sseldi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ∈ 𝒫 𝑋 )
130	129	elpwid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ⊆ 𝑋 )
131	1	mopnuni	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
132	105 131	syl	⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
133	132	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → 𝑋 = ∪ 𝐽 )
134	130 133	sseqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ⊆ ∪ 𝐽 )
135	134	sselda	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) ∧ 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) → 𝑡 ∈ ∪ 𝐽 )
136	135	adantrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) ∧ ( 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) → 𝑡 ∈ ∪ 𝐽 )
137	64	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( ( 2^nd ‘ 𝑥 ) + 1 ) ∈ ℕ₀ )
138		id	⊢ ( 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) → 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) )
139		snfi	⊢ { ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) } ∈ Fin
140		inss2	⊢ ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ⊆ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) )
141		ovex	⊢ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ∈ V
142	141	unisn	⊢ ∪ { ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) } = ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) )
143		uniiun	⊢ ∪ { ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) } = ∪ 𝑔 ∈ { ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) } 𝑔
144	142 143	eqtr3i	⊢ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) = ∪ 𝑔 ∈ { ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) } 𝑔
145	140 144	sseqtri	⊢ ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ⊆ ∪ 𝑔 ∈ { ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) } 𝑔
146		vex	⊢ 𝑔 ∈ V
147	1 2 146	heiborlem1	⊢ ( ( { ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) } ∈ Fin ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ⊆ ∪ 𝑔 ∈ { ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) } 𝑔 ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) → ∃ 𝑔 ∈ { ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) } 𝑔 ∈ 𝐾 )
148	139 145 147	mp3an12	⊢ ( ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 → ∃ 𝑔 ∈ { ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) } 𝑔 ∈ 𝐾 )
149		eleq1	⊢ ( 𝑔 = ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) → ( 𝑔 ∈ 𝐾 ↔ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ∈ 𝐾 ) )
150	141 149	rexsn	⊢ ( ∃ 𝑔 ∈ { ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) } 𝑔 ∈ 𝐾 ↔ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ∈ 𝐾 )
151	148 150	sylib	⊢ ( ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 → ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ∈ 𝐾 )
152		ovex	⊢ ( ( 2^nd ‘ 𝑥 ) + 1 ) ∈ V
153	1 2 3 46 152	heiborlem2	⊢ ( 𝑡 𝐺 ( ( 2^nd ‘ 𝑥 ) + 1 ) ↔ ( ( ( 2^nd ‘ 𝑥 ) + 1 ) ∈ ℕ₀ ∧ 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ∧ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ∈ 𝐾 ) )
154	153	biimpri	⊢ ( ( ( ( 2^nd ‘ 𝑥 ) + 1 ) ∈ ℕ₀ ∧ 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ∧ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ∈ 𝐾 ) → 𝑡 𝐺 ( ( 2^nd ‘ 𝑥 ) + 1 ) )
155	137 138 151 154	syl3an	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) ∧ 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) → 𝑡 𝐺 ( ( 2^nd ‘ 𝑥 ) + 1 ) )
156	155	3expb	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) ∧ ( 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) → 𝑡 𝐺 ( ( 2^nd ‘ 𝑥 ) + 1 ) )
157		simprr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) ∧ ( 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) → ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 )
158	136 156 157	jca32	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) ∧ ( 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) → ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝑡 𝐺 ( ( 2^nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) )
159	158	ex	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( ( 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) → ( 𝑡 ∈ ∪ 𝐽 ∧ ( 𝑡 𝐺 ( ( 2^nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) ) )
160	159	reximdv2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ( ∃ 𝑡 ∈ ( 𝐹 ‘ ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 → ∃ 𝑡 ∈ ∪ 𝐽 ( 𝑡 𝐺 ( ( 2^nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) )
161	128 160	mpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐺 ) → ∃ 𝑡 ∈ ∪ 𝐽 ( 𝑡 𝐺 ( ( 2^nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) )
162	161	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐺 ∃ 𝑡 ∈ ∪ 𝐽 ( 𝑡 𝐺 ( ( 2^nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) )
163	1	fvexi	⊢ 𝐽 ∈ V
164	163	uniex	⊢ ∪ 𝐽 ∈ V
165		breq1	⊢ ( 𝑡 = ( 𝑔 ‘ 𝑥 ) → ( 𝑡 𝐺 ( ( 2^nd ‘ 𝑥 ) + 1 ) ↔ ( 𝑔 ‘ 𝑥 ) 𝐺 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) )
166		oveq1	⊢ ( 𝑡 = ( 𝑔 ‘ 𝑥 ) → ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) = ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) )
167	166	ineq2d	⊢ ( 𝑡 = ( 𝑔 ‘ 𝑥 ) → ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) = ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) )
168	167	eleq1d	⊢ ( 𝑡 = ( 𝑔 ‘ 𝑥 ) → ( ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ↔ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) )
169	165 168	anbi12d	⊢ ( 𝑡 = ( 𝑔 ‘ 𝑥 ) → ( ( 𝑡 𝐺 ( ( 2^nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ↔ ( ( 𝑔 ‘ 𝑥 ) 𝐺 ( ( 2^nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) )
170	164 169	axcc4dom	⊢ ( ( 𝐺 ≼ ω ∧ ∀ 𝑥 ∈ 𝐺 ∃ 𝑡 ∈ ∪ 𝐽 ( 𝑡 𝐺 ( ( 2^nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( 𝑡 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) → ∃ 𝑔 ( 𝑔 : 𝐺 ⟶ ∪ 𝐽 ∧ ∀ 𝑥 ∈ 𝐺 ( ( 𝑔 ‘ 𝑥 ) 𝐺 ( ( 2^nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) )
171	61 162 170	syl2anc	⊢ ( 𝜑 → ∃ 𝑔 ( 𝑔 : 𝐺 ⟶ ∪ 𝐽 ∧ ∀ 𝑥 ∈ 𝐺 ( ( 𝑔 ‘ 𝑥 ) 𝐺 ( ( 2^nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) )
172		exsimpr	⊢ ( ∃ 𝑔 ( 𝑔 : 𝐺 ⟶ ∪ 𝐽 ∧ ∀ 𝑥 ∈ 𝐺 ( ( 𝑔 ‘ 𝑥 ) 𝐺 ( ( 2^nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) ) → ∃ 𝑔 ∀ 𝑥 ∈ 𝐺 ( ( 𝑔 ‘ 𝑥 ) 𝐺 ( ( 2^nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) )
173	171 172	syl	⊢ ( 𝜑 → ∃ 𝑔 ∀ 𝑥 ∈ 𝐺 ( ( 𝑔 ‘ 𝑥 ) 𝐺 ( ( 2^nd ‘ 𝑥 ) + 1 ) ∧ ( ( 𝐵 ‘ 𝑥 ) ∩ ( ( 𝑔 ‘ 𝑥 ) 𝐵 ( ( 2^nd ‘ 𝑥 ) + 1 ) ) ) ∈ 𝐾 ) )

Metamath Proof Explorer

Theorem heiborlem3

Proof