Step | Hyp | Ref
| Expression |
1 | | domtriomlem.2 |
. . . . 5
⊢ 𝐵 = {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} |
2 | | domtriomlem.1 |
. . . . . . 7
⊢ 𝐴 ∈ V |
3 | 2 | pwex 5306 |
. . . . . 6
⊢ 𝒫
𝐴 ∈ V |
4 | | simpl 482 |
. . . . . . . 8
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛) → 𝑦 ⊆ 𝐴) |
5 | 4 | ss2abi 4004 |
. . . . . . 7
⊢ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ⊆ {𝑦 ∣ 𝑦 ⊆ 𝐴} |
6 | | df-pw 4540 |
. . . . . . 7
⊢ 𝒫
𝐴 = {𝑦 ∣ 𝑦 ⊆ 𝐴} |
7 | 5, 6 | sseqtrri 3962 |
. . . . . 6
⊢ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ⊆ 𝒫 𝐴 |
8 | 3, 7 | ssexi 5249 |
. . . . 5
⊢ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ∈ V |
9 | 1, 8 | eqeltri 2836 |
. . . 4
⊢ 𝐵 ∈ V |
10 | | omex 9362 |
. . . . 5
⊢ ω
∈ V |
11 | 10 | enref 8744 |
. . . 4
⊢ ω
≈ ω |
12 | 9, 11 | axcc3 10178 |
. . 3
⊢
∃𝑏(𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) |
13 | | nfv 1920 |
. . . . . . . 8
⊢
Ⅎ𝑛 ¬ 𝐴 ∈ Fin |
14 | | nfra1 3144 |
. . . . . . . 8
⊢
Ⅎ𝑛∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵) |
15 | 13, 14 | nfan 1905 |
. . . . . . 7
⊢
Ⅎ𝑛(¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) |
16 | | nnfi 8915 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ω → 𝑛 ∈ Fin) |
17 | | pwfi 8926 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ Fin ↔ 𝒫
𝑛 ∈
Fin) |
18 | 16, 17 | sylib 217 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ω → 𝒫
𝑛 ∈
Fin) |
19 | | ficardom 9703 |
. . . . . . . . . . . . 13
⊢
(𝒫 𝑛 ∈
Fin → (card‘𝒫 𝑛) ∈ ω) |
20 | | isinf 8997 |
. . . . . . . . . . . . . 14
⊢ (¬
𝐴 ∈ Fin →
∀𝑚 ∈ ω
∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚)) |
21 | | breq2 5082 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = (card‘𝒫 𝑛) → (𝑦 ≈ 𝑚 ↔ 𝑦 ≈ (card‘𝒫 𝑛))) |
22 | 21 | anbi2d 628 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = (card‘𝒫 𝑛) → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)))) |
23 | 22 | exbidv 1927 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = (card‘𝒫 𝑛) → (∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚) ↔ ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)))) |
24 | 23 | rspcv 3555 |
. . . . . . . . . . . . . 14
⊢
((card‘𝒫 𝑛) ∈ ω → (∀𝑚 ∈ ω ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)))) |
25 | 20, 24 | syl5 34 |
. . . . . . . . . . . . 13
⊢
((card‘𝒫 𝑛) ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)))) |
26 | 18, 19, 25 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ω → (¬
𝐴 ∈ Fin →
∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)))) |
27 | | finnum 9690 |
. . . . . . . . . . . . . . 15
⊢
(𝒫 𝑛 ∈
Fin → 𝒫 𝑛
∈ dom card) |
28 | | cardid2 9695 |
. . . . . . . . . . . . . . 15
⊢
(𝒫 𝑛 ∈
dom card → (card‘𝒫 𝑛) ≈ 𝒫 𝑛) |
29 | | entr 8763 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ≈ (card‘𝒫
𝑛) ∧
(card‘𝒫 𝑛)
≈ 𝒫 𝑛) →
𝑦 ≈ 𝒫 𝑛) |
30 | 29 | expcom 413 |
. . . . . . . . . . . . . . 15
⊢
((card‘𝒫 𝑛) ≈ 𝒫 𝑛 → (𝑦 ≈ (card‘𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛)) |
31 | 18, 27, 28, 30 | 4syl 19 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ω → (𝑦 ≈ (card‘𝒫
𝑛) → 𝑦 ≈ 𝒫 𝑛)) |
32 | 31 | anim2d 611 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ω → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)) → (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛))) |
33 | 32 | eximdv 1923 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ω →
(∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛))) |
34 | 26, 33 | syld 47 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ω → (¬
𝐴 ∈ Fin →
∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛))) |
35 | 1 | neeq1i 3009 |
. . . . . . . . . . . 12
⊢ (𝐵 ≠ ∅ ↔ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ≠ ∅) |
36 | | abn0 4319 |
. . . . . . . . . . . 12
⊢ ({𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ≠ ∅ ↔ ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)) |
37 | 35, 36 | bitri 274 |
. . . . . . . . . . 11
⊢ (𝐵 ≠ ∅ ↔
∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)) |
38 | 34, 37 | syl6ibr 251 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ω → (¬
𝐴 ∈ Fin → 𝐵 ≠ ∅)) |
39 | 38 | com12 32 |
. . . . . . . . 9
⊢ (¬
𝐴 ∈ Fin → (𝑛 ∈ ω → 𝐵 ≠ ∅)) |
40 | 39 | adantr 480 |
. . . . . . . 8
⊢ ((¬
𝐴 ∈ Fin ∧
∀𝑛 ∈ ω
(𝐵 ≠ ∅ →
(𝑏‘𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → 𝐵 ≠ ∅)) |
41 | | rsp 3131 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
ω (𝐵 ≠ ∅
→ (𝑏‘𝑛) ∈ 𝐵) → (𝑛 ∈ ω → (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵))) |
42 | 41 | adantl 481 |
. . . . . . . 8
⊢ ((¬
𝐴 ∈ Fin ∧
∀𝑛 ∈ ω
(𝐵 ≠ ∅ →
(𝑏‘𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵))) |
43 | 40, 42 | mpdd 43 |
. . . . . . 7
⊢ ((¬
𝐴 ∈ Fin ∧
∀𝑛 ∈ ω
(𝐵 ≠ ∅ →
(𝑏‘𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → (𝑏‘𝑛) ∈ 𝐵)) |
44 | 15, 43 | ralrimi 3141 |
. . . . . 6
⊢ ((¬
𝐴 ∈ Fin ∧
∀𝑛 ∈ ω
(𝐵 ≠ ∅ →
(𝑏‘𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵) |
45 | 44 | 3adant2 1129 |
. . . . 5
⊢ ((¬
𝐴 ∈ Fin ∧ 𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵) |
46 | 45 | 3expib 1120 |
. . . 4
⊢ (¬
𝐴 ∈ Fin → ((𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵)) |
47 | 46 | eximdv 1923 |
. . 3
⊢ (¬
𝐴 ∈ Fin →
(∃𝑏(𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∃𝑏∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵)) |
48 | 12, 47 | mpi 20 |
. 2
⊢ (¬
𝐴 ∈ Fin →
∃𝑏∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵) |
49 | | axcc2 10177 |
. . . . 5
⊢
∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) |
50 | | simp2 1135 |
. . . . . . . 8
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → 𝑐 Fn ω) |
51 | | nfra1 3144 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 |
52 | | nfra1 3144 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛)) |
53 | 51, 52 | nfan 1905 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) |
54 | | fvex 6781 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏‘𝑛) ∈ V |
55 | | sseq1 3950 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝑏‘𝑛) → (𝑦 ⊆ 𝐴 ↔ (𝑏‘𝑛) ⊆ 𝐴)) |
56 | | breq1 5081 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝑏‘𝑛) → (𝑦 ≈ 𝒫 𝑛 ↔ (𝑏‘𝑛) ≈ 𝒫 𝑛)) |
57 | 55, 56 | anbi12d 630 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑏‘𝑛) → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛) ↔ ((𝑏‘𝑛) ⊆ 𝐴 ∧ (𝑏‘𝑛) ≈ 𝒫 𝑛))) |
58 | 54, 57, 1 | elab2 3614 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏‘𝑛) ∈ 𝐵 ↔ ((𝑏‘𝑛) ⊆ 𝐴 ∧ (𝑏‘𝑛) ≈ 𝒫 𝑛)) |
59 | 58 | simprbi 496 |
. . . . . . . . . . . . . 14
⊢ ((𝑏‘𝑛) ∈ 𝐵 → (𝑏‘𝑛) ≈ 𝒫 𝑛) |
60 | 59 | ralimi 3088 |
. . . . . . . . . . . . 13
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → ∀𝑛 ∈ ω (𝑏‘𝑛) ≈ 𝒫 𝑛) |
61 | | fveq2 6768 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑘 → (𝑏‘𝑛) = (𝑏‘𝑘)) |
62 | | pweq 4554 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑘 → 𝒫 𝑛 = 𝒫 𝑘) |
63 | 61, 62 | breq12d 5091 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑘 → ((𝑏‘𝑛) ≈ 𝒫 𝑛 ↔ (𝑏‘𝑘) ≈ 𝒫 𝑘)) |
64 | 63 | cbvralvw 3380 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ≈ 𝒫 𝑛 ↔ ∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘) |
65 | | peano2 7724 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ω → suc 𝑛 ∈
ω) |
66 | | omelon 9365 |
. . . . . . . . . . . . . . . . . . 19
⊢ ω
∈ On |
67 | 66 | onelssi 6372 |
. . . . . . . . . . . . . . . . . 18
⊢ (suc
𝑛 ∈ ω → suc
𝑛 ⊆
ω) |
68 | | ssralv 3991 |
. . . . . . . . . . . . . . . . . 18
⊢ (suc
𝑛 ⊆ ω →
(∀𝑘 ∈ ω
(𝑏‘𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘)) |
69 | 65, 67, 68 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ω →
(∀𝑘 ∈ ω
(𝑏‘𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘)) |
70 | | pwsdompw 9944 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ω ∧
∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘) → ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛)) |
71 | 70 | ex 412 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ω →
(∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘 → ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛))) |
72 | 69, 71 | syld 47 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ω →
(∀𝑘 ∈ ω
(𝑏‘𝑘) ≈ 𝒫 𝑘 → ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛))) |
73 | | sdomdif 8877 |
. . . . . . . . . . . . . . . 16
⊢ (∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛) → ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅) |
74 | 72, 73 | syl6 35 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ω →
(∀𝑘 ∈ ω
(𝑏‘𝑘) ≈ 𝒫 𝑘 → ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅)) |
75 | 64, 74 | syl5bi 241 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ω →
(∀𝑛 ∈ ω
(𝑏‘𝑛) ≈ 𝒫 𝑛 → ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅)) |
76 | 54 | difexi 5255 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) ∈ V |
77 | | domtriomlem.3 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐶 = (𝑛 ∈ ω ↦ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘))) |
78 | 77 | fvmpt2 6880 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ω ∧ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) ∈ V) → (𝐶‘𝑛) = ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘))) |
79 | 76, 78 | mpan2 687 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ω → (𝐶‘𝑛) = ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘))) |
80 | 79 | neeq1d 3004 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ω → ((𝐶‘𝑛) ≠ ∅ ↔ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅)) |
81 | 75, 80 | sylibrd 258 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ω →
(∀𝑛 ∈ ω
(𝑏‘𝑛) ≈ 𝒫 𝑛 → (𝐶‘𝑛) ≠ ∅)) |
82 | 60, 81 | syl5com 31 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → (𝑛 ∈ ω → (𝐶‘𝑛) ≠ ∅)) |
83 | 82 | adantr 480 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑛 ∈ ω → (𝐶‘𝑛) ≠ ∅)) |
84 | | rsp 3131 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑛 ∈ ω → ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))) |
85 | 84 | adantl 481 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑛 ∈ ω → ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))) |
86 | 83, 85 | mpdd 43 |
. . . . . . . . . 10
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) |
87 | 53, 86 | ralrimi 3141 |
. . . . . . . . 9
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) |
88 | 87 | 3adant2 1129 |
. . . . . . . 8
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) |
89 | 50, 88 | jca 511 |
. . . . . . 7
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))) |
90 | 89 | 3expib 1120 |
. . . . . 6
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → ((𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)))) |
91 | 90 | eximdv 1923 |
. . . . 5
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → (∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)))) |
92 | 49, 91 | mpi 20 |
. . . 4
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))) |
93 | | simp2 1135 |
. . . . . . . . . 10
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑐 Fn ω) |
94 | | nfra1 3144 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) |
95 | 51, 94 | nfan 1905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) |
96 | | rsp 3131 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑛 ∈
ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) |
97 | 96 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ω →
(∀𝑛 ∈ ω
(𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) |
98 | | rsp 3131 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → (𝑛 ∈ ω → (𝑏‘𝑛) ∈ 𝐵)) |
99 | 98 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ω →
(∀𝑛 ∈ ω
(𝑏‘𝑛) ∈ 𝐵 → (𝑏‘𝑛) ∈ 𝐵)) |
100 | 79 | eleq2d 2825 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ω → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) ↔ (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)))) |
101 | | eldifi 4065 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) → (𝑐‘𝑛) ∈ (𝑏‘𝑛)) |
102 | 100, 101 | syl6bi 252 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ω → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ (𝑏‘𝑛))) |
103 | 58 | simplbi 497 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑏‘𝑛) ∈ 𝐵 → (𝑏‘𝑛) ⊆ 𝐴) |
104 | 103 | sseld 3924 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑏‘𝑛) ∈ 𝐵 → ((𝑐‘𝑛) ∈ (𝑏‘𝑛) → (𝑐‘𝑛) ∈ 𝐴)) |
105 | 102, 104 | syl9 77 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ω → ((𝑏‘𝑛) ∈ 𝐵 → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ 𝐴))) |
106 | 99, 105 | syld 47 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ω →
(∀𝑛 ∈ ω
(𝑏‘𝑛) ∈ 𝐵 → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ 𝐴))) |
107 | 106 | com23 86 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ω → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) → (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (𝑐‘𝑛) ∈ 𝐴))) |
108 | 97, 107 | syld 47 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ω →
(∀𝑛 ∈ ω
(𝑐‘𝑛) ∈ (𝐶‘𝑛) → (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (𝑐‘𝑛) ∈ 𝐴))) |
109 | 108 | com13 88 |
. . . . . . . . . . . . 13
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ 𝐴))) |
110 | 109 | imp 406 |
. . . . . . . . . . . 12
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ 𝐴)) |
111 | 95, 110 | ralrimi 3141 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ 𝐴) |
112 | 111 | 3adant2 1129 |
. . . . . . . . . 10
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ 𝐴) |
113 | | ffnfv 6986 |
. . . . . . . . . 10
⊢ (𝑐:ω⟶𝐴 ↔ (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ 𝐴)) |
114 | 93, 112, 113 | sylanbrc 582 |
. . . . . . . . 9
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑐:ω⟶𝐴) |
115 | | nfv 1920 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛 𝑘 ∈ ω |
116 | | nnord 7708 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ω → Ord 𝑘) |
117 | | nnord 7708 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ω → Ord 𝑛) |
118 | | ordtri3or 6295 |
. . . . . . . . . . . . . . . 16
⊢ ((Ord
𝑘 ∧ Ord 𝑛) → (𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘)) |
119 | 116, 117,
118 | syl2an 595 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → (𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘)) |
120 | | fveq2 6768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 = 𝑘 → (𝑐‘𝑛) = (𝑐‘𝑘)) |
121 | | fveq2 6768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑘 = 𝑗 → (𝑏‘𝑘) = (𝑏‘𝑗)) |
122 | 121 | cbviunv 4974 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) = ∪ 𝑗 ∈ 𝑛 (𝑏‘𝑗) |
123 | | iuneq1 4945 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑛 = 𝑘 → ∪
𝑗 ∈ 𝑛 (𝑏‘𝑗) = ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) |
124 | 122, 123 | eqtrid 2791 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑛 = 𝑘 → ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘) = ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) |
125 | 61, 124 | difeq12d 4062 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 = 𝑘 → ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) = ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗))) |
126 | 120, 125 | eleq12d 2834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑛 = 𝑘 → ((𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) ↔ (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)))) |
127 | 126 | rspccv 3557 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(∀𝑛 ∈
ω (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) → (𝑘 ∈ ω → (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)))) |
128 | 96, 100 | mpbidi 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∀𝑛 ∈
ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)))) |
129 | 94, 128 | ralrimi 3141 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(∀𝑛 ∈
ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘))) |
130 | 127, 129 | syl11 33 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈ ω →
(∀𝑛 ∈ ω
(𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)))) |
131 | 130 | 3ad2ant1 1131 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)))) |
132 | | eldifi 4065 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) → (𝑐‘𝑘) ∈ (𝑏‘𝑘)) |
133 | | eleq1 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ (𝑏‘𝑘) ↔ (𝑐‘𝑛) ∈ (𝑏‘𝑘))) |
134 | 132, 133 | syl5ib 243 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) → (𝑐‘𝑛) ∈ (𝑏‘𝑘))) |
135 | 134 | 3ad2ant3 1133 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) → (𝑐‘𝑛) ∈ (𝑏‘𝑘))) |
136 | 131, 135 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ (𝑏‘𝑘))) |
137 | 136 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ (𝑏‘𝑘)) |
138 | | ssiun2 4981 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ 𝑛 → (𝑏‘𝑘) ⊆ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) |
139 | 138 | sseld 3924 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ 𝑛 → ((𝑐‘𝑛) ∈ (𝑏‘𝑘) → (𝑐‘𝑛) ∈ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘))) |
140 | 137, 139 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ 𝑛 → (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘))) |
141 | 140 | 3impib 1114 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ 𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) |
142 | 128 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ ω →
(∀𝑛 ∈ ω
(𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)))) |
143 | 142 | 3ad2ant2 1132 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)))) |
144 | 143 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘))) |
145 | 144 | eldifbd 3904 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ¬ (𝑐‘𝑛) ∈ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) |
146 | 145 | 3adant1 1128 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ 𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ¬ (𝑐‘𝑛) ∈ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) |
147 | 141, 146 | pm2.21dd 194 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ 𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑘 = 𝑛) |
148 | 147 | 3exp 1117 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ 𝑛 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛))) |
149 | | 2a1 28 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑛 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛))) |
150 | | fveq2 6768 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 = 𝑛 → (𝑏‘𝑗) = (𝑏‘𝑛)) |
151 | 150 | ssiun2s 4982 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ 𝑘 → (𝑏‘𝑛) ⊆ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) |
152 | 151 | sseld 3924 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ 𝑘 → ((𝑐‘𝑛) ∈ (𝑏‘𝑛) → (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗))) |
153 | 101, 152 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈ 𝑘 → ((𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) → (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗))) |
154 | 144, 153 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ 𝑘 → (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗))) |
155 | 154 | 3impib 1114 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ 𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) |
156 | | eleq1 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) ↔ (𝑐‘𝑛) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)))) |
157 | | eldifn 4066 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑐‘𝑛) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) → ¬ (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) |
158 | 156, 157 | syl6bi 252 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) → ¬ (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗))) |
159 | 158 | 3ad2ant3 1133 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) → ¬ (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗))) |
160 | 131, 159 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ¬ (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗))) |
161 | 160 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ 𝑘 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ¬ (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)))) |
162 | 161 | 3imp 1109 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ 𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ¬ (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) |
163 | 155, 162 | pm2.21dd 194 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ 𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑘 = 𝑛) |
164 | 163 | 3exp 1117 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ 𝑘 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛))) |
165 | 148, 149,
164 | 3jaoi 1425 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘) → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛))) |
166 | 165 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → ((𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛))) |
167 | 166 | 3expia 1119 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))) |
168 | 119, 167 | mpid 44 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐‘𝑘) = (𝑐‘𝑛) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛))) |
169 | 168 | com3r 87 |
. . . . . . . . . . . . 13
⊢
(∀𝑛 ∈
ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛))) |
170 | 169 | expd 415 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑘 ∈ ω → (𝑛 ∈ ω → ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛)))) |
171 | 94, 115, 170 | ralrimd 3143 |
. . . . . . . . . . 11
⊢
(∀𝑛 ∈
ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑘 ∈ ω → ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛))) |
172 | 171 | ralrimiv 3108 |
. . . . . . . . . 10
⊢
(∀𝑛 ∈
ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛)) |
173 | 172 | 3ad2ant3 1133 |
. . . . . . . . 9
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛)) |
174 | | dff13 7122 |
. . . . . . . . 9
⊢ (𝑐:ω–1-1→𝐴 ↔ (𝑐:ω⟶𝐴 ∧ ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛))) |
175 | 114, 173,
174 | sylanbrc 582 |
. . . . . . . 8
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑐:ω–1-1→𝐴) |
176 | 175 | 19.8ad 2178 |
. . . . . . 7
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∃𝑐 𝑐:ω–1-1→𝐴) |
177 | 2 | brdom 8721 |
. . . . . . 7
⊢ (ω
≼ 𝐴 ↔
∃𝑐 𝑐:ω–1-1→𝐴) |
178 | 176, 177 | sylibr 233 |
. . . . . 6
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ω ≼ 𝐴) |
179 | 178 | 3expib 1120 |
. . . . 5
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → ((𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ω ≼ 𝐴)) |
180 | 179 | exlimdv 1939 |
. . . 4
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → (∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ω ≼ 𝐴)) |
181 | 92, 180 | mpd 15 |
. . 3
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → ω ≼ 𝐴) |
182 | 181 | exlimiv 1936 |
. 2
⊢
(∃𝑏∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ω ≼ 𝐴) |
183 | 48, 182 | syl 17 |
1
⊢ (¬
𝐴 ∈ Fin → ω
≼ 𝐴) |