Step |
Hyp |
Ref |
Expression |
1 |
|
ssdomg |
⊢ ( 𝐴 ∈ V → ( 𝑥 ⊆ 𝐴 → 𝑥 ≼ 𝐴 ) ) |
2 |
1
|
adantr |
⊢ ( ( 𝐴 ∈ V ∧ 𝑥 ≈ 𝑛 ) → ( 𝑥 ⊆ 𝐴 → 𝑥 ≼ 𝐴 ) ) |
3 |
|
domen1 |
⊢ ( 𝑥 ≈ 𝑛 → ( 𝑥 ≼ 𝐴 ↔ 𝑛 ≼ 𝐴 ) ) |
4 |
3
|
adantl |
⊢ ( ( 𝐴 ∈ V ∧ 𝑥 ≈ 𝑛 ) → ( 𝑥 ≼ 𝐴 ↔ 𝑛 ≼ 𝐴 ) ) |
5 |
2 4
|
sylibd |
⊢ ( ( 𝐴 ∈ V ∧ 𝑥 ≈ 𝑛 ) → ( 𝑥 ⊆ 𝐴 → 𝑛 ≼ 𝐴 ) ) |
6 |
5
|
expimpd |
⊢ ( 𝐴 ∈ V → ( ( 𝑥 ≈ 𝑛 ∧ 𝑥 ⊆ 𝐴 ) → 𝑛 ≼ 𝐴 ) ) |
7 |
6
|
ancomsd |
⊢ ( 𝐴 ∈ V → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛 ) → 𝑛 ≼ 𝐴 ) ) |
8 |
7
|
exlimdv |
⊢ ( 𝐴 ∈ V → ( ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛 ) → 𝑛 ≼ 𝐴 ) ) |
9 |
8
|
ralimdv |
⊢ ( 𝐴 ∈ V → ( ∀ 𝑛 ∈ ω ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛 ) → ∀ 𝑛 ∈ ω 𝑛 ≼ 𝐴 ) ) |
10 |
|
domalom |
⊢ ( ∀ 𝑛 ∈ ω 𝑛 ≼ 𝐴 → ¬ 𝐴 ∈ Fin ) |
11 |
9 10
|
syl6 |
⊢ ( 𝐴 ∈ V → ( ∀ 𝑛 ∈ ω ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛 ) → ¬ 𝐴 ∈ Fin ) ) |
12 |
|
prcnel |
⊢ ( ¬ 𝐴 ∈ V → ¬ 𝐴 ∈ Fin ) |
13 |
12
|
a1d |
⊢ ( ¬ 𝐴 ∈ V → ( ∀ 𝑛 ∈ ω ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛 ) → ¬ 𝐴 ∈ Fin ) ) |
14 |
11 13
|
pm2.61i |
⊢ ( ∀ 𝑛 ∈ ω ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑛 ) → ¬ 𝐴 ∈ Fin ) |