Step |
Hyp |
Ref |
Expression |
1 |
|
cflem |
⊢ ( 𝐴 ∈ On → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ) |
2 |
|
intexab |
⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ↔ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ∈ V ) |
3 |
1 2
|
sylib |
⊢ ( 𝐴 ∈ On → ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ∈ V ) |
4 |
|
sseq2 |
⊢ ( 𝑣 = 𝐴 → ( 𝑦 ⊆ 𝑣 ↔ 𝑦 ⊆ 𝐴 ) ) |
5 |
|
raleq |
⊢ ( 𝑣 = 𝐴 → ( ∀ 𝑧 ∈ 𝑣 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) |
6 |
4 5
|
anbi12d |
⊢ ( 𝑣 = 𝐴 → ( ( 𝑦 ⊆ 𝑣 ∧ ∀ 𝑧 ∈ 𝑣 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ↔ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ) |
7 |
6
|
anbi2d |
⊢ ( 𝑣 = 𝐴 → ( ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝑣 ∧ ∀ 𝑧 ∈ 𝑣 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ↔ ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ) ) |
8 |
7
|
exbidv |
⊢ ( 𝑣 = 𝐴 → ( ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝑣 ∧ ∀ 𝑧 ∈ 𝑣 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ↔ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ) ) |
9 |
8
|
abbidv |
⊢ ( 𝑣 = 𝐴 → { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝑣 ∧ ∀ 𝑧 ∈ 𝑣 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ) |
10 |
9
|
inteqd |
⊢ ( 𝑣 = 𝐴 → ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝑣 ∧ ∀ 𝑧 ∈ 𝑣 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } = ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ) |
11 |
|
df-cf |
⊢ cf = ( 𝑣 ∈ On ↦ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝑣 ∧ ∀ 𝑧 ∈ 𝑣 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ) |
12 |
10 11
|
fvmptg |
⊢ ( ( 𝐴 ∈ On ∧ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ∈ V ) → ( cf ‘ 𝐴 ) = ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ) |
13 |
3 12
|
mpdan |
⊢ ( 𝐴 ∈ On → ( cf ‘ 𝐴 ) = ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ) |