Step |
Hyp |
Ref |
Expression |
1 |
|
chintcl.1 |
⊢ ( 𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅ ) |
2 |
1
|
simpli |
⊢ 𝐴 ⊆ Cℋ |
3 |
|
chsssh |
⊢ Cℋ ⊆ Sℋ |
4 |
2 3
|
sstri |
⊢ 𝐴 ⊆ Sℋ |
5 |
1
|
simpri |
⊢ 𝐴 ≠ ∅ |
6 |
4 5
|
pm3.2i |
⊢ ( 𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅ ) |
7 |
6
|
shintcli |
⊢ ∩ 𝐴 ∈ Sℋ |
8 |
2
|
sseli |
⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ Cℋ ) |
9 |
|
vex |
⊢ 𝑥 ∈ V |
10 |
9
|
chlimi |
⊢ ( ( 𝑦 ∈ Cℋ ∧ 𝑓 : ℕ ⟶ 𝑦 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ 𝑦 ) |
11 |
10
|
3exp |
⊢ ( 𝑦 ∈ Cℋ → ( 𝑓 : ℕ ⟶ 𝑦 → ( 𝑓 ⇝𝑣 𝑥 → 𝑥 ∈ 𝑦 ) ) ) |
12 |
11
|
com3r |
⊢ ( 𝑓 ⇝𝑣 𝑥 → ( 𝑦 ∈ Cℋ → ( 𝑓 : ℕ ⟶ 𝑦 → 𝑥 ∈ 𝑦 ) ) ) |
13 |
8 12
|
syl5 |
⊢ ( 𝑓 ⇝𝑣 𝑥 → ( 𝑦 ∈ 𝐴 → ( 𝑓 : ℕ ⟶ 𝑦 → 𝑥 ∈ 𝑦 ) ) ) |
14 |
13
|
imp |
⊢ ( ( 𝑓 ⇝𝑣 𝑥 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑓 : ℕ ⟶ 𝑦 → 𝑥 ∈ 𝑦 ) ) |
15 |
14
|
ralimdva |
⊢ ( 𝑓 ⇝𝑣 𝑥 → ( ∀ 𝑦 ∈ 𝐴 𝑓 : ℕ ⟶ 𝑦 → ∀ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ) ) |
16 |
5
|
fint |
⊢ ( 𝑓 : ℕ ⟶ ∩ 𝐴 ↔ ∀ 𝑦 ∈ 𝐴 𝑓 : ℕ ⟶ 𝑦 ) |
17 |
9
|
elint2 |
⊢ ( 𝑥 ∈ ∩ 𝐴 ↔ ∀ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ) |
18 |
15 16 17
|
3imtr4g |
⊢ ( 𝑓 ⇝𝑣 𝑥 → ( 𝑓 : ℕ ⟶ ∩ 𝐴 → 𝑥 ∈ ∩ 𝐴 ) ) |
19 |
18
|
impcom |
⊢ ( ( 𝑓 : ℕ ⟶ ∩ 𝐴 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ ∩ 𝐴 ) |
20 |
19
|
gen2 |
⊢ ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ ∩ 𝐴 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ ∩ 𝐴 ) |
21 |
|
isch2 |
⊢ ( ∩ 𝐴 ∈ Cℋ ↔ ( ∩ 𝐴 ∈ Sℋ ∧ ∀ 𝑓 ∀ 𝑥 ( ( 𝑓 : ℕ ⟶ ∩ 𝐴 ∧ 𝑓 ⇝𝑣 𝑥 ) → 𝑥 ∈ ∩ 𝐴 ) ) ) |
22 |
7 20 21
|
mpbir2an |
⊢ ∩ 𝐴 ∈ Cℋ |