Step | Hyp | Ref
| Expression |
1 | | domtriomlem.2 |
. . . . 5
⊢ 𝐵 = {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} |
2 | | domtriomlem.1 |
. . . . . . 7
⊢ 𝐴 ∈ V |
3 | 2 | pwex 4982 |
. . . . . 6
⊢ 𝒫
𝐴 ∈ V |
4 | | simpl 468 |
. . . . . . . 8
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛) → 𝑦 ⊆ 𝐴) |
5 | 4 | ss2abi 3824 |
. . . . . . 7
⊢ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ⊆ {𝑦 ∣ 𝑦 ⊆ 𝐴} |
6 | | df-pw 4300 |
. . . . . . 7
⊢ 𝒫
𝐴 = {𝑦 ∣ 𝑦 ⊆ 𝐴} |
7 | 5, 6 | sseqtr4i 3788 |
. . . . . 6
⊢ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ⊆ 𝒫 𝐴 |
8 | 3, 7 | ssexi 4938 |
. . . . 5
⊢ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ∈ V |
9 | 1, 8 | eqeltri 2846 |
. . . 4
⊢ 𝐵 ∈ V |
10 | | omex 8705 |
. . . . 5
⊢ ω
∈ V |
11 | 10 | enref 8143 |
. . . 4
⊢ ω
≈ ω |
12 | 9, 11 | axcc3 9463 |
. . 3
⊢
∃𝑏(𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) |
13 | | nfv 1995 |
. . . . . . . 8
⊢
Ⅎ𝑛 ¬ 𝐴 ∈ Fin |
14 | | nfra1 3090 |
. . . . . . . 8
⊢
Ⅎ𝑛∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵) |
15 | 13, 14 | nfan 1980 |
. . . . . . 7
⊢
Ⅎ𝑛(¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) |
16 | | nnfi 8310 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ω → 𝑛 ∈ Fin) |
17 | | pwfi 8418 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ Fin ↔ 𝒫
𝑛 ∈
Fin) |
18 | 16, 17 | sylib 208 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ω → 𝒫
𝑛 ∈
Fin) |
19 | | ficardom 8988 |
. . . . . . . . . . . . 13
⊢
(𝒫 𝑛 ∈
Fin → (card‘𝒫 𝑛) ∈ ω) |
20 | | isinf 8330 |
. . . . . . . . . . . . . 14
⊢ (¬
𝐴 ∈ Fin →
∀𝑚 ∈ ω
∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚)) |
21 | | breq2 4791 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = (card‘𝒫 𝑛) → (𝑦 ≈ 𝑚 ↔ 𝑦 ≈ (card‘𝒫 𝑛))) |
22 | 21 | anbi2d 608 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = (card‘𝒫 𝑛) → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)))) |
23 | 22 | exbidv 2002 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = (card‘𝒫 𝑛) → (∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚) ↔ ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)))) |
24 | 23 | rspcv 3457 |
. . . . . . . . . . . . . 14
⊢
((card‘𝒫 𝑛) ∈ ω → (∀𝑚 ∈ ω ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)))) |
25 | 20, 24 | syl5 34 |
. . . . . . . . . . . . 13
⊢
((card‘𝒫 𝑛) ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)))) |
26 | 18, 19, 25 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ω → (¬
𝐴 ∈ Fin →
∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)))) |
27 | | finnum 8975 |
. . . . . . . . . . . . . . 15
⊢
(𝒫 𝑛 ∈
Fin → 𝒫 𝑛
∈ dom card) |
28 | | cardid2 8980 |
. . . . . . . . . . . . . . 15
⊢
(𝒫 𝑛 ∈
dom card → (card‘𝒫 𝑛) ≈ 𝒫 𝑛) |
29 | | entr 8162 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ≈ (card‘𝒫
𝑛) ∧
(card‘𝒫 𝑛)
≈ 𝒫 𝑛) →
𝑦 ≈ 𝒫 𝑛) |
30 | 29 | expcom 398 |
. . . . . . . . . . . . . . 15
⊢
((card‘𝒫 𝑛) ≈ 𝒫 𝑛 → (𝑦 ≈ (card‘𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛)) |
31 | 18, 27, 28, 30 | 4syl 19 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ω → (𝑦 ≈ (card‘𝒫
𝑛) → 𝑦 ≈ 𝒫 𝑛)) |
32 | 31 | anim2d 593 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ω → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)) → (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛))) |
33 | 32 | eximdv 1998 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ω →
(∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛))) |
34 | 26, 33 | syld 47 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ω → (¬
𝐴 ∈ Fin →
∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛))) |
35 | 1 | neeq1i 3007 |
. . . . . . . . . . . 12
⊢ (𝐵 ≠ ∅ ↔ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ≠ ∅) |
36 | | abn0 4102 |
. . . . . . . . . . . 12
⊢ ({𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ≠ ∅ ↔ ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)) |
37 | 35, 36 | bitri 264 |
. . . . . . . . . . 11
⊢ (𝐵 ≠ ∅ ↔
∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)) |
38 | 34, 37 | syl6ibr 242 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ω → (¬
𝐴 ∈ Fin → 𝐵 ≠ ∅)) |
39 | 38 | com12 32 |
. . . . . . . . 9
⊢ (¬
𝐴 ∈ Fin → (𝑛 ∈ ω → 𝐵 ≠ ∅)) |
40 | 39 | adantr 466 |
. . . . . . . 8
⊢ ((¬
𝐴 ∈ Fin ∧
∀𝑛 ∈ ω
(𝐵 ≠ ∅ →
(𝑏‘𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → 𝐵 ≠ ∅)) |
41 | | rsp 3078 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
ω (𝐵 ≠ ∅
→ (𝑏‘𝑛) ∈ 𝐵) → (𝑛 ∈ ω → (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵))) |
42 | 41 | adantl 467 |
. . . . . . . 8
⊢ ((¬
𝐴 ∈ Fin ∧
∀𝑛 ∈ ω
(𝐵 ≠ ∅ →
(𝑏‘𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵))) |
43 | 40, 42 | mpdd 43 |
. . . . . . 7
⊢ ((¬
𝐴 ∈ Fin ∧
∀𝑛 ∈ ω
(𝐵 ≠ ∅ →
(𝑏‘𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → (𝑏‘𝑛) ∈ 𝐵)) |
44 | 15, 43 | ralrimi 3106 |
. . . . . 6
⊢ ((¬
𝐴 ∈ Fin ∧
∀𝑛 ∈ ω
(𝐵 ≠ ∅ →
(𝑏‘𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵) |
45 | 44 | 3adant2 1125 |
. . . . 5
⊢ ((¬
𝐴 ∈ Fin ∧ 𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵) |
46 | 45 | 3expib 1116 |
. . . 4
⊢ (¬
𝐴 ∈ Fin → ((𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵)) |
47 | 46 | eximdv 1998 |
. . 3
⊢ (¬
𝐴 ∈ Fin →
(∃𝑏(𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∃𝑏∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵)) |
48 | 12, 47 | mpi 20 |
. 2
⊢ (¬
𝐴 ∈ Fin →
∃𝑏∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵) |
49 | | axcc2 9462 |
. . . . 5
⊢
∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) |
50 | | simp2 1131 |
. . . . . . . 8
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → 𝑐 Fn ω) |
51 | | nfra1 3090 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 |
52 | | nfra1 3090 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛)) |
53 | 51, 52 | nfan 1980 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) |
54 | | fvex 6343 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏‘𝑛) ∈ V |
55 | | sseq1 3776 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝑏‘𝑛) → (𝑦 ⊆ 𝐴 ↔ (𝑏‘𝑛) ⊆ 𝐴)) |
56 | | breq1 4790 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝑏‘𝑛) → (𝑦 ≈ 𝒫 𝑛 ↔ (𝑏‘𝑛) ≈ 𝒫 𝑛)) |
57 | 55, 56 | anbi12d 610 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑏‘𝑛) → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛) ↔ ((𝑏‘𝑛) ⊆ 𝐴 ∧ (𝑏‘𝑛) ≈ 𝒫 𝑛))) |
58 | 54, 57, 1 | elab2 3506 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏‘𝑛) ∈ 𝐵 ↔ ((𝑏‘𝑛) ⊆ 𝐴 ∧ (𝑏‘𝑛) ≈ 𝒫 𝑛)) |
59 | 58 | simprbi 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑏‘𝑛) ∈ 𝐵 → (𝑏‘𝑛) ≈ 𝒫 𝑛) |
60 | 59 | ralimi 3101 |
. . . . . . . . . . . . 13
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → ∀𝑛 ∈ ω (𝑏‘𝑛) ≈ 𝒫 𝑛) |
61 | | fveq2 6333 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑘 → (𝑏‘𝑛) = (𝑏‘𝑘)) |
62 | | pweq 4301 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑘 → 𝒫 𝑛 = 𝒫 𝑘) |
63 | 61, 62 | breq12d 4800 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑘 → ((𝑏‘𝑛) ≈ 𝒫 𝑛 ↔ (𝑏‘𝑘) ≈ 𝒫 𝑘)) |
64 | 63 | cbvralv 3320 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ≈ 𝒫 𝑛 ↔ ∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘) |
65 | | peano2 7234 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ω → suc 𝑛 ∈
ω) |
66 | | omelon 8708 |
. . . . . . . . . . . . . . . . . . 19
⊢ ω
∈ On |
67 | 66 | onelssi 5980 |
. . . . . . . . . . . . . . . . . 18
⊢ (suc
𝑛 ∈ ω → suc
𝑛 ⊆
ω) |
68 | | ssralv 3816 |
. . . . . . . . . . . . . . . . . 18
⊢ (suc
𝑛 ⊆ ω →
(∀𝑘 ∈ ω
(𝑏‘𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘)) |
69 | 65, 67, 68 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ω →
(∀𝑘 ∈ ω
(𝑏‘𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘)) |
70 | | pwsdompw 9229 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ω ∧
∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘) → ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛)) |
71 | 70 | ex 397 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ω →
(∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘 → ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛))) |
72 | 69, 71 | syld 47 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ω →
(∀𝑘 ∈ ω
(𝑏‘𝑘) ≈ 𝒫 𝑘 → ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛))) |
73 | | sdomdif 8265 |
. . . . . . . . . . . . . . . 16
⊢ (∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛) → ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅) |
74 | 72, 73 | syl6 35 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ω →
(∀𝑘 ∈ ω
(𝑏‘𝑘) ≈ 𝒫 𝑘 → ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅)) |
75 | 64, 74 | syl5bi 232 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ω →
(∀𝑛 ∈ ω
(𝑏‘𝑛) ≈ 𝒫 𝑛 → ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅)) |
76 | | difss 3889 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) ⊆ (𝑏‘𝑛) |
77 | 54, 76 | ssexi 4938 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) ∈ V |
78 | | domtriomlem.3 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐶 = (𝑛 ∈ ω ↦ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘))) |
79 | 78 | fvmpt2 6434 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ω ∧ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) ∈ V) → (𝐶‘𝑛) = ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘))) |
80 | 77, 79 | mpan2 665 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ω → (𝐶‘𝑛) = ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘))) |
81 | 80 | neeq1d 3002 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ω → ((𝐶‘𝑛) ≠ ∅ ↔ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅)) |
82 | 75, 81 | sylibrd 249 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ω →
(∀𝑛 ∈ ω
(𝑏‘𝑛) ≈ 𝒫 𝑛 → (𝐶‘𝑛) ≠ ∅)) |
83 | 60, 82 | syl5com 31 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → (𝑛 ∈ ω → (𝐶‘𝑛) ≠ ∅)) |
84 | 83 | adantr 466 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑛 ∈ ω → (𝐶‘𝑛) ≠ ∅)) |
85 | | rsp 3078 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑛 ∈ ω → ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))) |
86 | 85 | adantl 467 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑛 ∈ ω → ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))) |
87 | 84, 86 | mpdd 43 |
. . . . . . . . . 10
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) |
88 | 53, 87 | ralrimi 3106 |
. . . . . . . . 9
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) |
89 | 88 | 3adant2 1125 |
. . . . . . . 8
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) |
90 | 50, 89 | jca 497 |
. . . . . . 7
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))) |
91 | 90 | 3expib 1116 |
. . . . . 6
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → ((𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)))) |
92 | 91 | eximdv 1998 |
. . . . 5
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → (∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)))) |
93 | 49, 92 | mpi 20 |
. . . 4
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))) |
94 | | simp2 1131 |
. . . . . . . . . 10
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑐 Fn ω) |
95 | | nfra1 3090 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) |
96 | 51, 95 | nfan 1980 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) |
97 | | rsp 3078 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑛 ∈
ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) |
98 | 97 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ω →
(∀𝑛 ∈ ω
(𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) |
99 | | rsp 3078 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → (𝑛 ∈ ω → (𝑏‘𝑛) ∈ 𝐵)) |
100 | 99 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ω →
(∀𝑛 ∈ ω
(𝑏‘𝑛) ∈ 𝐵 → (𝑏‘𝑛) ∈ 𝐵)) |
101 | 80 | eleq2d 2836 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ω → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) ↔ (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)))) |
102 | | eldifi 3884 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) → (𝑐‘𝑛) ∈ (𝑏‘𝑛)) |
103 | 101, 102 | syl6bi 243 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ω → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ (𝑏‘𝑛))) |
104 | 58 | simplbi 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑏‘𝑛) ∈ 𝐵 → (𝑏‘𝑛) ⊆ 𝐴) |
105 | 104 | sseld 3752 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑏‘𝑛) ∈ 𝐵 → ((𝑐‘𝑛) ∈ (𝑏‘𝑛) → (𝑐‘𝑛) ∈ 𝐴)) |
106 | 103, 105 | syl9 77 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ω → ((𝑏‘𝑛) ∈ 𝐵 → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ 𝐴))) |
107 | 100, 106 | syld 47 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ω →
(∀𝑛 ∈ ω
(𝑏‘𝑛) ∈ 𝐵 → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ 𝐴))) |
108 | 107 | com23 86 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ω → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) → (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (𝑐‘𝑛) ∈ 𝐴))) |
109 | 98, 108 | syld 47 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ω →
(∀𝑛 ∈ ω
(𝑐‘𝑛) ∈ (𝐶‘𝑛) → (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (𝑐‘𝑛) ∈ 𝐴))) |
110 | 109 | com13 88 |
. . . . . . . . . . . . 13
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ 𝐴))) |
111 | 110 | imp 393 |
. . . . . . . . . . . 12
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ 𝐴)) |
112 | 96, 111 | ralrimi 3106 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ 𝐴) |
113 | 112 | 3adant2 1125 |
. . . . . . . . . 10
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ 𝐴) |
114 | | ffnfv 6531 |
. . . . . . . . . 10
⊢ (𝑐:ω⟶𝐴 ↔ (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ 𝐴)) |
115 | 94, 113, 114 | sylanbrc 566 |
. . . . . . . . 9
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑐:ω⟶𝐴) |
116 | | nfv 1995 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛 𝑘 ∈ ω |
117 | | nnord 7221 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ω → Ord 𝑘) |
118 | | nnord 7221 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ω → Ord 𝑛) |
119 | | ordtri3or 5899 |
. . . . . . . . . . . . . . . 16
⊢ ((Ord
𝑘 ∧ Ord 𝑛) → (𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘)) |
120 | 117, 118,
119 | syl2an 577 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → (𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘)) |
121 | | fveq2 6333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 = 𝑘 → (𝑐‘𝑛) = (𝑐‘𝑘)) |
122 | | fveq2 6333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑘 = 𝑗 → (𝑏‘𝑘) = (𝑏‘𝑗)) |
123 | 122 | cbviunv 4694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) = ∪ 𝑗 ∈ 𝑛 (𝑏‘𝑗) |
124 | | iuneq1 4669 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑛 = 𝑘 → ∪
𝑗 ∈ 𝑛 (𝑏‘𝑗) = ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) |
125 | 123, 124 | syl5eq 2817 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑛 = 𝑘 → ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘) = ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) |
126 | 61, 125 | difeq12d 3881 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 = 𝑘 → ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) = ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗))) |
127 | 121, 126 | eleq12d 2844 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 = 𝑘 → ((𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) ↔ (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)))) |
128 | 127 | rspccv 3458 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(∀𝑛 ∈
ω (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) → (𝑘 ∈ ω → (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)))) |
129 | 97, 101 | mpbidi 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∀𝑛 ∈
ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)))) |
130 | 95, 129 | ralrimi 3106 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(∀𝑛 ∈
ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘))) |
131 | 128, 130 | syl11 33 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈ ω →
(∀𝑛 ∈ ω
(𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)))) |
132 | 131 | 3ad2ant1 1127 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)))) |
133 | | eldifi 3884 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) → (𝑐‘𝑘) ∈ (𝑏‘𝑘)) |
134 | | eleq1 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ (𝑏‘𝑘) ↔ (𝑐‘𝑛) ∈ (𝑏‘𝑘))) |
135 | 133, 134 | syl5ib 234 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) → (𝑐‘𝑛) ∈ (𝑏‘𝑘))) |
136 | 135 | 3ad2ant3 1129 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) → (𝑐‘𝑛) ∈ (𝑏‘𝑘))) |
137 | 132, 136 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ (𝑏‘𝑘))) |
138 | 137 | imp 393 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ (𝑏‘𝑘)) |
139 | | ssiun2 4698 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ 𝑛 → (𝑏‘𝑘) ⊆ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) |
140 | 139 | sseld 3752 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ 𝑛 → ((𝑐‘𝑛) ∈ (𝑏‘𝑘) → (𝑐‘𝑛) ∈ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘))) |
141 | 138, 140 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ 𝑛 → (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘))) |
142 | 141 | 3impib 1108 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ 𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) |
143 | 129 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ ω →
(∀𝑛 ∈ ω
(𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)))) |
144 | 143 | 3ad2ant2 1128 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)))) |
145 | 144 | imp 393 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘))) |
146 | 145 | eldifbd 3737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ¬ (𝑐‘𝑛) ∈ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) |
147 | 146 | 3adant1 1124 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ 𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ¬ (𝑐‘𝑛) ∈ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) |
148 | 142, 147 | pm2.21dd 186 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ 𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑘 = 𝑛) |
149 | 148 | 3exp 1112 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ 𝑛 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛))) |
150 | | 2a1 28 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑛 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛))) |
151 | | fveq2 6333 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 = 𝑛 → (𝑏‘𝑗) = (𝑏‘𝑛)) |
152 | 151 | ssiun2s 4699 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ 𝑘 → (𝑏‘𝑛) ⊆ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) |
153 | 152 | sseld 3752 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ 𝑘 → ((𝑐‘𝑛) ∈ (𝑏‘𝑛) → (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗))) |
154 | 102, 153 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈ 𝑘 → ((𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) → (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗))) |
155 | 145, 154 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ 𝑘 → (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗))) |
156 | 155 | 3impib 1108 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ 𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) |
157 | | eleq1 2838 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) ↔ (𝑐‘𝑛) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)))) |
158 | | eldifn 3885 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑐‘𝑛) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) → ¬ (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) |
159 | 157, 158 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) → ¬ (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗))) |
160 | 159 | 3ad2ant3 1129 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) → ¬ (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗))) |
161 | 132, 160 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ¬ (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗))) |
162 | 161 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ 𝑘 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ¬ (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)))) |
163 | 162 | 3imp 1101 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ 𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ¬ (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) |
164 | 156, 163 | pm2.21dd 186 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ 𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑘 = 𝑛) |
165 | 164 | 3exp 1112 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ 𝑘 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛))) |
166 | 149, 150,
165 | 3jaoi 1539 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘) → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛))) |
167 | 166 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → ((𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛))) |
168 | 167 | 3expia 1114 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))) |
169 | 120, 168 | mpid 44 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐‘𝑘) = (𝑐‘𝑛) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛))) |
170 | 169 | com3r 87 |
. . . . . . . . . . . . 13
⊢
(∀𝑛 ∈
ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛))) |
171 | 170 | expd 400 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑘 ∈ ω → (𝑛 ∈ ω → ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛)))) |
172 | 95, 116, 171 | ralrimd 3108 |
. . . . . . . . . . 11
⊢
(∀𝑛 ∈
ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑘 ∈ ω → ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛))) |
173 | 172 | ralrimiv 3114 |
. . . . . . . . . 10
⊢
(∀𝑛 ∈
ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛)) |
174 | 173 | 3ad2ant3 1129 |
. . . . . . . . 9
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛)) |
175 | | dff13 6656 |
. . . . . . . . 9
⊢ (𝑐:ω–1-1→𝐴 ↔ (𝑐:ω⟶𝐴 ∧ ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛))) |
176 | 115, 174,
175 | sylanbrc 566 |
. . . . . . . 8
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑐:ω–1-1→𝐴) |
177 | | 19.8a 2206 |
. . . . . . . 8
⊢ (𝑐:ω–1-1→𝐴 → ∃𝑐 𝑐:ω–1-1→𝐴) |
178 | 176, 177 | syl 17 |
. . . . . . 7
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∃𝑐 𝑐:ω–1-1→𝐴) |
179 | 2 | brdom 8122 |
. . . . . . 7
⊢ (ω
≼ 𝐴 ↔
∃𝑐 𝑐:ω–1-1→𝐴) |
180 | 178, 179 | sylibr 224 |
. . . . . 6
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ω ≼ 𝐴) |
181 | 180 | 3expib 1116 |
. . . . 5
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → ((𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ω ≼ 𝐴)) |
182 | 181 | exlimdv 2013 |
. . . 4
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → (∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ω ≼ 𝐴)) |
183 | 93, 182 | mpd 15 |
. . 3
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → ω ≼ 𝐴) |
184 | 183 | exlimiv 2010 |
. 2
⊢
(∃𝑏∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ω ≼ 𝐴) |
185 | 48, 184 | syl 17 |
1
⊢ (¬
𝐴 ∈ Fin → ω
≼ 𝐴) |