Step |
Hyp |
Ref |
Expression |
1 |
|
fin23lem26 |
⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ 𝑖 ∈ ω ) → ∃ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ) |
2 |
|
ensym |
⊢ ( ( 𝑎 ∩ 𝑆 ) ≈ 𝑖 → 𝑖 ≈ ( 𝑎 ∩ 𝑆 ) ) |
3 |
|
entr |
⊢ ( ( ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ∧ 𝑖 ≈ ( 𝑎 ∩ 𝑆 ) ) → ( 𝑗 ∩ 𝑆 ) ≈ ( 𝑎 ∩ 𝑆 ) ) |
4 |
2 3
|
sylan2 |
⊢ ( ( ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ∧ ( 𝑎 ∩ 𝑆 ) ≈ 𝑖 ) → ( 𝑗 ∩ 𝑆 ) ≈ ( 𝑎 ∩ 𝑆 ) ) |
5 |
|
simpl |
⊢ ( ( 𝑆 ⊆ ω ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑎 ∈ 𝑆 ) ) → 𝑆 ⊆ ω ) |
6 |
|
simprl |
⊢ ( ( 𝑆 ⊆ ω ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑎 ∈ 𝑆 ) ) → 𝑗 ∈ 𝑆 ) |
7 |
5 6
|
sseldd |
⊢ ( ( 𝑆 ⊆ ω ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑎 ∈ 𝑆 ) ) → 𝑗 ∈ ω ) |
8 |
|
nnfi |
⊢ ( 𝑗 ∈ ω → 𝑗 ∈ Fin ) |
9 |
|
inss1 |
⊢ ( 𝑗 ∩ 𝑆 ) ⊆ 𝑗 |
10 |
|
ssfi |
⊢ ( ( 𝑗 ∈ Fin ∧ ( 𝑗 ∩ 𝑆 ) ⊆ 𝑗 ) → ( 𝑗 ∩ 𝑆 ) ∈ Fin ) |
11 |
8 9 10
|
sylancl |
⊢ ( 𝑗 ∈ ω → ( 𝑗 ∩ 𝑆 ) ∈ Fin ) |
12 |
7 11
|
syl |
⊢ ( ( 𝑆 ⊆ ω ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑎 ∈ 𝑆 ) ) → ( 𝑗 ∩ 𝑆 ) ∈ Fin ) |
13 |
|
simprr |
⊢ ( ( 𝑆 ⊆ ω ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑎 ∈ 𝑆 ) ) → 𝑎 ∈ 𝑆 ) |
14 |
5 13
|
sseldd |
⊢ ( ( 𝑆 ⊆ ω ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑎 ∈ 𝑆 ) ) → 𝑎 ∈ ω ) |
15 |
|
nnfi |
⊢ ( 𝑎 ∈ ω → 𝑎 ∈ Fin ) |
16 |
|
inss1 |
⊢ ( 𝑎 ∩ 𝑆 ) ⊆ 𝑎 |
17 |
|
ssfi |
⊢ ( ( 𝑎 ∈ Fin ∧ ( 𝑎 ∩ 𝑆 ) ⊆ 𝑎 ) → ( 𝑎 ∩ 𝑆 ) ∈ Fin ) |
18 |
15 16 17
|
sylancl |
⊢ ( 𝑎 ∈ ω → ( 𝑎 ∩ 𝑆 ) ∈ Fin ) |
19 |
14 18
|
syl |
⊢ ( ( 𝑆 ⊆ ω ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑎 ∈ 𝑆 ) ) → ( 𝑎 ∩ 𝑆 ) ∈ Fin ) |
20 |
|
nnord |
⊢ ( 𝑗 ∈ ω → Ord 𝑗 ) |
21 |
|
nnord |
⊢ ( 𝑎 ∈ ω → Ord 𝑎 ) |
22 |
|
ordtri2or2 |
⊢ ( ( Ord 𝑗 ∧ Ord 𝑎 ) → ( 𝑗 ⊆ 𝑎 ∨ 𝑎 ⊆ 𝑗 ) ) |
23 |
20 21 22
|
syl2an |
⊢ ( ( 𝑗 ∈ ω ∧ 𝑎 ∈ ω ) → ( 𝑗 ⊆ 𝑎 ∨ 𝑎 ⊆ 𝑗 ) ) |
24 |
7 14 23
|
syl2anc |
⊢ ( ( 𝑆 ⊆ ω ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑎 ∈ 𝑆 ) ) → ( 𝑗 ⊆ 𝑎 ∨ 𝑎 ⊆ 𝑗 ) ) |
25 |
|
ssrin |
⊢ ( 𝑗 ⊆ 𝑎 → ( 𝑗 ∩ 𝑆 ) ⊆ ( 𝑎 ∩ 𝑆 ) ) |
26 |
|
ssrin |
⊢ ( 𝑎 ⊆ 𝑗 → ( 𝑎 ∩ 𝑆 ) ⊆ ( 𝑗 ∩ 𝑆 ) ) |
27 |
25 26
|
orim12i |
⊢ ( ( 𝑗 ⊆ 𝑎 ∨ 𝑎 ⊆ 𝑗 ) → ( ( 𝑗 ∩ 𝑆 ) ⊆ ( 𝑎 ∩ 𝑆 ) ∨ ( 𝑎 ∩ 𝑆 ) ⊆ ( 𝑗 ∩ 𝑆 ) ) ) |
28 |
24 27
|
syl |
⊢ ( ( 𝑆 ⊆ ω ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑎 ∈ 𝑆 ) ) → ( ( 𝑗 ∩ 𝑆 ) ⊆ ( 𝑎 ∩ 𝑆 ) ∨ ( 𝑎 ∩ 𝑆 ) ⊆ ( 𝑗 ∩ 𝑆 ) ) ) |
29 |
|
fin23lem25 |
⊢ ( ( ( 𝑗 ∩ 𝑆 ) ∈ Fin ∧ ( 𝑎 ∩ 𝑆 ) ∈ Fin ∧ ( ( 𝑗 ∩ 𝑆 ) ⊆ ( 𝑎 ∩ 𝑆 ) ∨ ( 𝑎 ∩ 𝑆 ) ⊆ ( 𝑗 ∩ 𝑆 ) ) ) → ( ( 𝑗 ∩ 𝑆 ) ≈ ( 𝑎 ∩ 𝑆 ) ↔ ( 𝑗 ∩ 𝑆 ) = ( 𝑎 ∩ 𝑆 ) ) ) |
30 |
12 19 28 29
|
syl3anc |
⊢ ( ( 𝑆 ⊆ ω ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑎 ∈ 𝑆 ) ) → ( ( 𝑗 ∩ 𝑆 ) ≈ ( 𝑎 ∩ 𝑆 ) ↔ ( 𝑗 ∩ 𝑆 ) = ( 𝑎 ∩ 𝑆 ) ) ) |
31 |
|
ordom |
⊢ Ord ω |
32 |
|
fin23lem24 |
⊢ ( ( ( Ord ω ∧ 𝑆 ⊆ ω ) ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑎 ∈ 𝑆 ) ) → ( ( 𝑗 ∩ 𝑆 ) = ( 𝑎 ∩ 𝑆 ) ↔ 𝑗 = 𝑎 ) ) |
33 |
31 32
|
mpanl1 |
⊢ ( ( 𝑆 ⊆ ω ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑎 ∈ 𝑆 ) ) → ( ( 𝑗 ∩ 𝑆 ) = ( 𝑎 ∩ 𝑆 ) ↔ 𝑗 = 𝑎 ) ) |
34 |
30 33
|
bitrd |
⊢ ( ( 𝑆 ⊆ ω ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑎 ∈ 𝑆 ) ) → ( ( 𝑗 ∩ 𝑆 ) ≈ ( 𝑎 ∩ 𝑆 ) ↔ 𝑗 = 𝑎 ) ) |
35 |
4 34
|
syl5ib |
⊢ ( ( 𝑆 ⊆ ω ∧ ( 𝑗 ∈ 𝑆 ∧ 𝑎 ∈ 𝑆 ) ) → ( ( ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ∧ ( 𝑎 ∩ 𝑆 ) ≈ 𝑖 ) → 𝑗 = 𝑎 ) ) |
36 |
35
|
ralrimivva |
⊢ ( 𝑆 ⊆ ω → ∀ 𝑗 ∈ 𝑆 ∀ 𝑎 ∈ 𝑆 ( ( ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ∧ ( 𝑎 ∩ 𝑆 ) ≈ 𝑖 ) → 𝑗 = 𝑎 ) ) |
37 |
36
|
ad2antrr |
⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ 𝑖 ∈ ω ) → ∀ 𝑗 ∈ 𝑆 ∀ 𝑎 ∈ 𝑆 ( ( ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ∧ ( 𝑎 ∩ 𝑆 ) ≈ 𝑖 ) → 𝑗 = 𝑎 ) ) |
38 |
|
ineq1 |
⊢ ( 𝑗 = 𝑎 → ( 𝑗 ∩ 𝑆 ) = ( 𝑎 ∩ 𝑆 ) ) |
39 |
38
|
breq1d |
⊢ ( 𝑗 = 𝑎 → ( ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ↔ ( 𝑎 ∩ 𝑆 ) ≈ 𝑖 ) ) |
40 |
39
|
reu4 |
⊢ ( ∃! 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ↔ ( ∃ 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ∧ ∀ 𝑗 ∈ 𝑆 ∀ 𝑎 ∈ 𝑆 ( ( ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ∧ ( 𝑎 ∩ 𝑆 ) ≈ 𝑖 ) → 𝑗 = 𝑎 ) ) ) |
41 |
1 37 40
|
sylanbrc |
⊢ ( ( ( 𝑆 ⊆ ω ∧ ¬ 𝑆 ∈ Fin ) ∧ 𝑖 ∈ ω ) → ∃! 𝑗 ∈ 𝑆 ( 𝑗 ∩ 𝑆 ) ≈ 𝑖 ) |