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