Step | Hyp | Ref
| Expression |
1 | | ordom 7654 |
. . . 4
⊢ Ord
ω |
2 | | ordwe 6226 |
. . . 4
⊢ (Ord
ω → E We ω) |
3 | | weso 5542 |
. . . 4
⊢ ( E We
ω → E Or ω) |
4 | 1, 2, 3 | mp2b 10 |
. . 3
⊢ E Or
ω |
5 | 4 | a1i 11 |
. 2
⊢ ((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) → E Or
ω) |
6 | | sopo 5487 |
. . . . 5
⊢ ( E Or
ω → E Po ω) |
7 | 4, 6 | ax-mp 5 |
. . . 4
⊢ E Po
ω |
8 | | poss 5470 |
. . . 4
⊢ (𝑆 ⊆ ω → ( E Po
ω → E Po 𝑆)) |
9 | 7, 8 | mpi 20 |
. . 3
⊢ (𝑆 ⊆ ω → E Po
𝑆) |
10 | 9 | adantr 484 |
. 2
⊢ ((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) → E Po
𝑆) |
11 | | fin23lem22.b |
. . . 4
⊢ 𝐶 = (𝑖 ∈ ω ↦ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖)) |
12 | 11 | fin23lem22 9941 |
. . 3
⊢ ((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) → 𝐶:ω–1-1-onto→𝑆) |
13 | | f1ofo 6668 |
. . 3
⊢ (𝐶:ω–1-1-onto→𝑆 → 𝐶:ω–onto→𝑆) |
14 | 12, 13 | syl 17 |
. 2
⊢ ((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) → 𝐶:ω–onto→𝑆) |
15 | | nnsdomel 9606 |
. . . . . . . 8
⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) → (𝑎 ∈ 𝑏 ↔ 𝑎 ≺ 𝑏)) |
16 | 15 | adantl 485 |
. . . . . . 7
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 ∈ 𝑏 ↔ 𝑎 ≺ 𝑏)) |
17 | 16 | biimpd 232 |
. . . . . 6
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 ∈ 𝑏 → 𝑎 ≺ 𝑏)) |
18 | | fin23lem23 9940 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ 𝑎 ∈ ω) →
∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) |
19 | 18 | adantrr 717 |
. . . . . . . . . . . 12
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) →
∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) |
20 | | ineq1 4120 |
. . . . . . . . . . . . . 14
⊢ (𝑗 = 𝑖 → (𝑗 ∩ 𝑆) = (𝑖 ∩ 𝑆)) |
21 | 20 | breq1d 5063 |
. . . . . . . . . . . . 13
⊢ (𝑗 = 𝑖 → ((𝑗 ∩ 𝑆) ≈ 𝑎 ↔ (𝑖 ∩ 𝑆) ≈ 𝑎)) |
22 | 21 | cbvreuvw 3361 |
. . . . . . . . . . . 12
⊢
(∃!𝑗 ∈
𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎 ↔ ∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑎) |
23 | 19, 22 | sylib 221 |
. . . . . . . . . . 11
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) →
∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑎) |
24 | | nfv 1922 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑖((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎 |
25 | 21 | cbvriotavw 7180 |
. . . . . . . . . . . 12
⊢
(℩𝑗
∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) = (℩𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑎) |
26 | | ineq1 4120 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) → (𝑖 ∩ 𝑆) = ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆)) |
27 | 26 | breq1d 5063 |
. . . . . . . . . . . 12
⊢ (𝑖 = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) → ((𝑖 ∩ 𝑆) ≈ 𝑎 ↔ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎)) |
28 | 24, 25, 27 | riotaprop 7198 |
. . . . . . . . . . 11
⊢
(∃!𝑖 ∈
𝑆 (𝑖 ∩ 𝑆) ≈ 𝑎 → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ 𝑆 ∧ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎)) |
29 | 23, 28 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) →
((℩𝑗 ∈
𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ 𝑆 ∧ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎)) |
30 | 29 | simprd 499 |
. . . . . . . . 9
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) →
((℩𝑗 ∈
𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎) |
31 | 30 | adantrr 717 |
. . . . . . . 8
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎 ≺ 𝑏)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎) |
32 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎 ≺ 𝑏)) → 𝑎 ≺ 𝑏) |
33 | | fin23lem23 9940 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ 𝑏 ∈ ω) →
∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) |
34 | 33 | adantrl 716 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) →
∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) |
35 | 20 | breq1d 5063 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 = 𝑖 → ((𝑗 ∩ 𝑆) ≈ 𝑏 ↔ (𝑖 ∩ 𝑆) ≈ 𝑏)) |
36 | 35 | cbvreuvw 3361 |
. . . . . . . . . . . . . 14
⊢
(∃!𝑗 ∈
𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏 ↔ ∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑏) |
37 | 34, 36 | sylib 221 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) →
∃!𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑏) |
38 | | nfv 1922 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑖((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏 |
39 | 35 | cbvriotavw 7180 |
. . . . . . . . . . . . . 14
⊢
(℩𝑗
∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) = (℩𝑖 ∈ 𝑆 (𝑖 ∩ 𝑆) ≈ 𝑏) |
40 | | ineq1 4120 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) → (𝑖 ∩ 𝑆) = ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆)) |
41 | 40 | breq1d 5063 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) → ((𝑖 ∩ 𝑆) ≈ 𝑏 ↔ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏)) |
42 | 38, 39, 41 | riotaprop 7198 |
. . . . . . . . . . . . 13
⊢
(∃!𝑖 ∈
𝑆 (𝑖 ∩ 𝑆) ≈ 𝑏 → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ 𝑆 ∧ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏)) |
43 | 37, 42 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) →
((℩𝑗 ∈
𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ 𝑆 ∧ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏)) |
44 | 43 | simprd 499 |
. . . . . . . . . . 11
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) →
((℩𝑗 ∈
𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) ≈ 𝑏) |
45 | 44 | ensymd 8679 |
. . . . . . . . . 10
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑏 ≈ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆)) |
46 | 45 | adantrr 717 |
. . . . . . . . 9
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎 ≺ 𝑏)) → 𝑏 ≈ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆)) |
47 | | sdomentr 8780 |
. . . . . . . . 9
⊢ ((𝑎 ≺ 𝑏 ∧ 𝑏 ≈ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆)) → 𝑎 ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆)) |
48 | 32, 46, 47 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎 ≺ 𝑏)) → 𝑎 ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆)) |
49 | | ensdomtr 8782 |
. . . . . . . 8
⊢
((((℩𝑗
∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≈ 𝑎 ∧ 𝑎 ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆)) |
50 | 31, 48, 49 | syl2anc 587 |
. . . . . . 7
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) ∧ 𝑎 ≺ 𝑏)) → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆)) |
51 | 50 | expr 460 |
. . . . . 6
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 ≺ 𝑏 → ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆))) |
52 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑆 ⊆
ω) |
53 | | omsson 7648 |
. . . . . . . . 9
⊢ ω
⊆ On |
54 | 52, 53 | sstrdi 3913 |
. . . . . . . 8
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑆 ⊆ On) |
55 | 29 | simpld 498 |
. . . . . . . 8
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) →
(℩𝑗 ∈
𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ 𝑆) |
56 | 54, 55 | sseldd 3902 |
. . . . . . 7
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) →
(℩𝑗 ∈
𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ On) |
57 | 43 | simpld 498 |
. . . . . . . 8
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) →
(℩𝑗 ∈
𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ 𝑆) |
58 | 54, 57 | sseldd 3902 |
. . . . . . 7
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) →
(℩𝑗 ∈
𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ On) |
59 | | onsdominel 8795 |
. . . . . . . 8
⊢
(((℩𝑗
∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ On ∧ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ On ∧ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆)) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏)) |
60 | 59 | 3expia 1123 |
. . . . . . 7
⊢
(((℩𝑗
∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ On ∧ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∈ On) → (((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏))) |
61 | 56, 58, 60 | syl2anc 587 |
. . . . . 6
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) →
(((℩𝑗 ∈
𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∩ 𝑆) ≺ ((℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏) ∩ 𝑆) → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏))) |
62 | 17, 51, 61 | 3syld 60 |
. . . . 5
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 ∈ 𝑏 → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏))) |
63 | | breq2 5057 |
. . . . . . . 8
⊢ (𝑖 = 𝑎 → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ 𝑎)) |
64 | 63 | riotabidv 7172 |
. . . . . . 7
⊢ (𝑖 = 𝑎 → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖) = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎)) |
65 | | simprl 771 |
. . . . . . 7
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑎 ∈
ω) |
66 | 11, 64, 65, 55 | fvmptd3 6841 |
. . . . . 6
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝐶‘𝑎) = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎)) |
67 | | breq2 5057 |
. . . . . . . 8
⊢ (𝑖 = 𝑏 → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑗 ∩ 𝑆) ≈ 𝑏)) |
68 | 67 | riotabidv 7172 |
. . . . . . 7
⊢ (𝑖 = 𝑏 → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖) = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏)) |
69 | | simprr 773 |
. . . . . . 7
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → 𝑏 ∈
ω) |
70 | 11, 68, 69, 57 | fvmptd3 6841 |
. . . . . 6
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝐶‘𝑏) = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏)) |
71 | 66, 70 | eleq12d 2832 |
. . . . 5
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → ((𝐶‘𝑎) ∈ (𝐶‘𝑏) ↔ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑎) ∈ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑏))) |
72 | 62, 71 | sylibrd 262 |
. . . 4
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 ∈ 𝑏 → (𝐶‘𝑎) ∈ (𝐶‘𝑏))) |
73 | | epel 5463 |
. . . 4
⊢ (𝑎 E 𝑏 ↔ 𝑎 ∈ 𝑏) |
74 | | fvex 6730 |
. . . . 5
⊢ (𝐶‘𝑏) ∈ V |
75 | 74 | epeli 5462 |
. . . 4
⊢ ((𝐶‘𝑎) E (𝐶‘𝑏) ↔ (𝐶‘𝑎) ∈ (𝐶‘𝑏)) |
76 | 72, 73, 75 | 3imtr4g 299 |
. . 3
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑎 ∈ ω ∧ 𝑏 ∈ ω)) → (𝑎 E 𝑏 → (𝐶‘𝑎) E (𝐶‘𝑏))) |
77 | 76 | ralrimivva 3112 |
. 2
⊢ ((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) →
∀𝑎 ∈ ω
∀𝑏 ∈ ω
(𝑎 E 𝑏 → (𝐶‘𝑎) E (𝐶‘𝑏))) |
78 | | soisoi 7137 |
. 2
⊢ ((( E Or
ω ∧ E Po 𝑆) ∧
(𝐶:ω–onto→𝑆 ∧ ∀𝑎 ∈ ω ∀𝑏 ∈ ω (𝑎 E 𝑏 → (𝐶‘𝑎) E (𝐶‘𝑏)))) → 𝐶 Isom E , E (ω, 𝑆)) |
79 | 5, 10, 14, 77, 78 | syl22anc 839 |
1
⊢ ((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) → 𝐶 Isom E , E (ω, 𝑆)) |