Step | Hyp | Ref
| Expression |
1 | | domtriomlem.2 |
. . . . 5
⊢ 𝐵 = {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} |
2 | | domtriomlem.1 |
. . . . . . 7
⊢ 𝐴 ∈ V |
3 | 2 | pwex 4774 |
. . . . . 6
⊢ 𝒫
𝐴 ∈ V |
4 | | simpl 472 |
. . . . . . . 8
⊢ ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛) → 𝑦 ⊆ 𝐴) |
5 | 4 | ss2abi 3637 |
. . . . . . 7
⊢ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ⊆ {𝑦 ∣ 𝑦 ⊆ 𝐴} |
6 | | df-pw 4110 |
. . . . . . 7
⊢ 𝒫
𝐴 = {𝑦 ∣ 𝑦 ⊆ 𝐴} |
7 | 5, 6 | sseqtr4i 3601 |
. . . . . 6
⊢ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ⊆ 𝒫 𝐴 |
8 | 3, 7 | ssexi 4731 |
. . . . 5
⊢ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ∈ V |
9 | 1, 8 | eqeltri 2684 |
. . . 4
⊢ 𝐵 ∈ V |
10 | | omex 8423 |
. . . . 5
⊢ ω
∈ V |
11 | 10 | enref 7874 |
. . . 4
⊢ ω
≈ ω |
12 | 9, 11 | axcc3 9143 |
. . 3
⊢
∃𝑏(𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) |
13 | | nfv 1830 |
. . . . . . . 8
⊢
Ⅎ𝑛 ¬ 𝐴 ∈ Fin |
14 | | nfra1 2925 |
. . . . . . . 8
⊢
Ⅎ𝑛∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵) |
15 | 13, 14 | nfan 1816 |
. . . . . . 7
⊢
Ⅎ𝑛(¬ 𝐴 ∈ Fin ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) |
16 | | nnfi 8038 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ω → 𝑛 ∈ Fin) |
17 | | pwfi 8144 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ Fin ↔ 𝒫
𝑛 ∈
Fin) |
18 | 16, 17 | sylib 207 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ω → 𝒫
𝑛 ∈
Fin) |
19 | | ficardom 8670 |
. . . . . . . . . . . . 13
⊢
(𝒫 𝑛 ∈
Fin → (card‘𝒫 𝑛) ∈ ω) |
20 | | isinf 8058 |
. . . . . . . . . . . . . 14
⊢ (¬
𝐴 ∈ Fin →
∀𝑚 ∈ ω
∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚)) |
21 | | breq2 4587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = (card‘𝒫 𝑛) → (𝑦 ≈ 𝑚 ↔ 𝑦 ≈ (card‘𝒫 𝑛))) |
22 | 21 | anbi2d 736 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = (card‘𝒫 𝑛) → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)))) |
23 | 22 | exbidv 1837 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = (card‘𝒫 𝑛) → (∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚) ↔ ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)))) |
24 | 23 | rspcv 3278 |
. . . . . . . . . . . . . 14
⊢
((card‘𝒫 𝑛) ∈ ω → (∀𝑚 ∈ ω ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝑚) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)))) |
25 | 20, 24 | syl5 33 |
. . . . . . . . . . . . 13
⊢
((card‘𝒫 𝑛) ∈ ω → (¬ 𝐴 ∈ Fin → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)))) |
26 | 18, 19, 25 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ω → (¬
𝐴 ∈ Fin →
∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)))) |
27 | | finnum 8657 |
. . . . . . . . . . . . . . 15
⊢
(𝒫 𝑛 ∈
Fin → 𝒫 𝑛
∈ dom card) |
28 | | cardid2 8662 |
. . . . . . . . . . . . . . 15
⊢
(𝒫 𝑛 ∈
dom card → (card‘𝒫 𝑛) ≈ 𝒫 𝑛) |
29 | | entr 7894 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ≈ (card‘𝒫
𝑛) ∧
(card‘𝒫 𝑛)
≈ 𝒫 𝑛) →
𝑦 ≈ 𝒫 𝑛) |
30 | 29 | expcom 450 |
. . . . . . . . . . . . . . 15
⊢
((card‘𝒫 𝑛) ≈ 𝒫 𝑛 → (𝑦 ≈ (card‘𝒫 𝑛) → 𝑦 ≈ 𝒫 𝑛)) |
31 | 18, 27, 28, 30 | 4syl 19 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ω → (𝑦 ≈ (card‘𝒫
𝑛) → 𝑦 ≈ 𝒫 𝑛)) |
32 | 31 | anim2d 587 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ω → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)) → (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛))) |
33 | 32 | eximdv 1833 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ω →
(∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ (card‘𝒫 𝑛)) → ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛))) |
34 | 26, 33 | syld 46 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ω → (¬
𝐴 ∈ Fin →
∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛))) |
35 | 1 | neeq1i 2846 |
. . . . . . . . . . . 12
⊢ (𝐵 ≠ ∅ ↔ {𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ≠ ∅) |
36 | | abn0 3908 |
. . . . . . . . . . . 12
⊢ ({𝑦 ∣ (𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)} ≠ ∅ ↔ ∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)) |
37 | 35, 36 | bitri 263 |
. . . . . . . . . . 11
⊢ (𝐵 ≠ ∅ ↔
∃𝑦(𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛)) |
38 | 34, 37 | syl6ibr 241 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ω → (¬
𝐴 ∈ Fin → 𝐵 ≠ ∅)) |
39 | 38 | com12 32 |
. . . . . . . . 9
⊢ (¬
𝐴 ∈ Fin → (𝑛 ∈ ω → 𝐵 ≠ ∅)) |
40 | 39 | adantr 480 |
. . . . . . . 8
⊢ ((¬
𝐴 ∈ Fin ∧
∀𝑛 ∈ ω
(𝐵 ≠ ∅ →
(𝑏‘𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → 𝐵 ≠ ∅)) |
41 | | rsp 2913 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
ω (𝐵 ≠ ∅
→ (𝑏‘𝑛) ∈ 𝐵) → (𝑛 ∈ ω → (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵))) |
42 | 41 | adantl 481 |
. . . . . . . 8
⊢ ((¬
𝐴 ∈ Fin ∧
∀𝑛 ∈ ω
(𝐵 ≠ ∅ →
(𝑏‘𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵))) |
43 | 40, 42 | mpdd 42 |
. . . . . . 7
⊢ ((¬
𝐴 ∈ Fin ∧
∀𝑛 ∈ ω
(𝐵 ≠ ∅ →
(𝑏‘𝑛) ∈ 𝐵)) → (𝑛 ∈ ω → (𝑏‘𝑛) ∈ 𝐵)) |
44 | 15, 43 | ralrimi 2940 |
. . . . . 6
⊢ ((¬
𝐴 ∈ Fin ∧
∀𝑛 ∈ ω
(𝐵 ≠ ∅ →
(𝑏‘𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵) |
45 | 44 | 3adant2 1073 |
. . . . 5
⊢ ((¬
𝐴 ∈ Fin ∧ 𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵) |
46 | 45 | 3expib 1260 |
. . . 4
⊢ (¬
𝐴 ∈ Fin → ((𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵)) |
47 | 46 | eximdv 1833 |
. . 3
⊢ (¬
𝐴 ∈ Fin →
(∃𝑏(𝑏 Fn ω ∧ ∀𝑛 ∈ ω (𝐵 ≠ ∅ → (𝑏‘𝑛) ∈ 𝐵)) → ∃𝑏∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵)) |
48 | 12, 47 | mpi 20 |
. 2
⊢ (¬
𝐴 ∈ Fin →
∃𝑏∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵) |
49 | | axcc2 9142 |
. . . . 5
⊢
∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) |
50 | | simp2 1055 |
. . . . . . . 8
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → 𝑐 Fn ω) |
51 | | nfra1 2925 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 |
52 | | nfra1 2925 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛)) |
53 | 51, 52 | nfan 1816 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) |
54 | | fvex 6113 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏‘𝑛) ∈ V |
55 | | sseq1 3589 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝑏‘𝑛) → (𝑦 ⊆ 𝐴 ↔ (𝑏‘𝑛) ⊆ 𝐴)) |
56 | | breq1 4586 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝑏‘𝑛) → (𝑦 ≈ 𝒫 𝑛 ↔ (𝑏‘𝑛) ≈ 𝒫 𝑛)) |
57 | 55, 56 | anbi12d 743 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑏‘𝑛) → ((𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝒫 𝑛) ↔ ((𝑏‘𝑛) ⊆ 𝐴 ∧ (𝑏‘𝑛) ≈ 𝒫 𝑛))) |
58 | 54, 57, 1 | elab2 3323 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏‘𝑛) ∈ 𝐵 ↔ ((𝑏‘𝑛) ⊆ 𝐴 ∧ (𝑏‘𝑛) ≈ 𝒫 𝑛)) |
59 | 58 | simprbi 479 |
. . . . . . . . . . . . . 14
⊢ ((𝑏‘𝑛) ∈ 𝐵 → (𝑏‘𝑛) ≈ 𝒫 𝑛) |
60 | 59 | ralimi 2936 |
. . . . . . . . . . . . 13
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → ∀𝑛 ∈ ω (𝑏‘𝑛) ≈ 𝒫 𝑛) |
61 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑘 → (𝑏‘𝑛) = (𝑏‘𝑘)) |
62 | | pweq 4111 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑘 → 𝒫 𝑛 = 𝒫 𝑘) |
63 | 61, 62 | breq12d 4596 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑘 → ((𝑏‘𝑛) ≈ 𝒫 𝑛 ↔ (𝑏‘𝑘) ≈ 𝒫 𝑘)) |
64 | 63 | cbvralv 3147 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ≈ 𝒫 𝑛 ↔ ∀𝑘 ∈ ω (𝑏‘𝑘) ≈ 𝒫 𝑘) |
65 | | peano2 6978 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ω → suc 𝑛 ∈
ω) |
66 | | omelon 8426 |
. . . . . . . . . . . . . . . . . . 19
⊢ ω
∈ On |
67 | 66 | onelssi 5753 |
. . . . . . . . . . . . . . . . . 18
⊢ (suc
𝑛 ∈ ω → suc
𝑛 ⊆
ω) |
68 | | ssralv 3629 |
. . . . . . . . . . . . . . . . . 18
⊢ (suc
𝑛 ⊆ ω →
(∀𝑘 ∈ ω
(𝑏‘𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘)) |
69 | 65, 67, 68 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ω →
(∀𝑘 ∈ ω
(𝑏‘𝑘) ≈ 𝒫 𝑘 → ∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘)) |
70 | | pwsdompw 8909 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑛 ∈ ω ∧
∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘) → ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛)) |
71 | 70 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ω →
(∀𝑘 ∈ suc 𝑛(𝑏‘𝑘) ≈ 𝒫 𝑘 → ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛))) |
72 | 69, 71 | syld 46 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ω →
(∀𝑘 ∈ ω
(𝑏‘𝑘) ≈ 𝒫 𝑘 → ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛))) |
73 | | sdomdif 7993 |
. . . . . . . . . . . . . . . 16
⊢ (∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) ≺ (𝑏‘𝑛) → ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅) |
74 | 72, 73 | syl6 34 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ω →
(∀𝑘 ∈ ω
(𝑏‘𝑘) ≈ 𝒫 𝑘 → ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅)) |
75 | 64, 74 | syl5bi 231 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ω →
(∀𝑛 ∈ ω
(𝑏‘𝑛) ≈ 𝒫 𝑛 → ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅)) |
76 | | difss 3699 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) ⊆ (𝑏‘𝑛) |
77 | 54, 76 | ssexi 4731 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) ∈ V |
78 | | domtriomlem.3 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐶 = (𝑛 ∈ ω ↦ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘))) |
79 | 78 | fvmpt2 6200 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ω ∧ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) ∈ V) → (𝐶‘𝑛) = ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘))) |
80 | 77, 79 | mpan2 703 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ω → (𝐶‘𝑛) = ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘))) |
81 | 80 | neeq1d 2841 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ω → ((𝐶‘𝑛) ≠ ∅ ↔ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) ≠ ∅)) |
82 | 75, 81 | sylibrd 248 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ω →
(∀𝑛 ∈ ω
(𝑏‘𝑛) ≈ 𝒫 𝑛 → (𝐶‘𝑛) ≠ ∅)) |
83 | 60, 82 | syl5com 31 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → (𝑛 ∈ ω → (𝐶‘𝑛) ≠ ∅)) |
84 | 83 | adantr 480 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑛 ∈ ω → (𝐶‘𝑛) ≠ ∅)) |
85 | | rsp 2913 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑛 ∈ ω → ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))) |
86 | 85 | adantl 481 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑛 ∈ ω → ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛)))) |
87 | 84, 86 | mpdd 42 |
. . . . . . . . . 10
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) |
88 | 53, 87 | ralrimi 2940 |
. . . . . . . . 9
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) |
89 | 88 | 3adant2 1073 |
. . . . . . . 8
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) |
90 | 50, 89 | jca 553 |
. . . . . . 7
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))) |
91 | 90 | 3expib 1260 |
. . . . . 6
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → ((𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)))) |
92 | 91 | eximdv 1833 |
. . . . 5
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → (∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω ((𝐶‘𝑛) ≠ ∅ → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) → ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)))) |
93 | 49, 92 | mpi 20 |
. . . 4
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → ∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛))) |
94 | | simp2 1055 |
. . . . . . . . . 10
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑐 Fn ω) |
95 | | nfra1 2925 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑛∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) |
96 | 51, 95 | nfan 1816 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛(∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) |
97 | | rsp 2913 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑛 ∈
ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) |
98 | 97 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ω →
(∀𝑛 ∈ ω
(𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ (𝐶‘𝑛))) |
99 | | rsp 2913 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → (𝑛 ∈ ω → (𝑏‘𝑛) ∈ 𝐵)) |
100 | 99 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ω →
(∀𝑛 ∈ ω
(𝑏‘𝑛) ∈ 𝐵 → (𝑏‘𝑛) ∈ 𝐵)) |
101 | 80 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ω → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) ↔ (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)))) |
102 | | eldifi 3694 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) → (𝑐‘𝑛) ∈ (𝑏‘𝑛)) |
103 | 101, 102 | syl6bi 242 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ω → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ (𝑏‘𝑛))) |
104 | 58 | simplbi 475 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑏‘𝑛) ∈ 𝐵 → (𝑏‘𝑛) ⊆ 𝐴) |
105 | 104 | sseld 3567 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑏‘𝑛) ∈ 𝐵 → ((𝑐‘𝑛) ∈ (𝑏‘𝑛) → (𝑐‘𝑛) ∈ 𝐴)) |
106 | 103, 105 | syl9 75 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ω → ((𝑏‘𝑛) ∈ 𝐵 → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ 𝐴))) |
107 | 100, 106 | syld 46 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ω →
(∀𝑛 ∈ ω
(𝑏‘𝑛) ∈ 𝐵 → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ 𝐴))) |
108 | 107 | com23 84 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ω → ((𝑐‘𝑛) ∈ (𝐶‘𝑛) → (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (𝑐‘𝑛) ∈ 𝐴))) |
109 | 98, 108 | syld 46 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ω →
(∀𝑛 ∈ ω
(𝑐‘𝑛) ∈ (𝐶‘𝑛) → (∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → (𝑐‘𝑛) ∈ 𝐴))) |
110 | 109 | com13 86 |
. . . . . . . . . . . . 13
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ 𝐴))) |
111 | 110 | imp 444 |
. . . . . . . . . . . 12
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ 𝐴)) |
112 | 96, 111 | ralrimi 2940 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ 𝐴) |
113 | 112 | 3adant2 1073 |
. . . . . . . . . 10
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ 𝐴) |
114 | | ffnfv 6295 |
. . . . . . . . . 10
⊢ (𝑐:ω⟶𝐴 ↔ (𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ 𝐴)) |
115 | 94, 113, 114 | sylanbrc 695 |
. . . . . . . . 9
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑐:ω⟶𝐴) |
116 | | nfv 1830 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛 𝑘 ∈ ω |
117 | | nnord 6965 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ω → Ord 𝑘) |
118 | | nnord 6965 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ω → Ord 𝑛) |
119 | | ordtri3or 5672 |
. . . . . . . . . . . . . . . 16
⊢ ((Ord
𝑘 ∧ Ord 𝑛) → (𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘)) |
120 | 117, 118,
119 | syl2an 493 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → (𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘)) |
121 | 97, 101 | mpbidi 230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(∀𝑛 ∈
ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑛 ∈ ω → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)))) |
122 | 95, 121 | ralrimi 2940 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∀𝑛 ∈
ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘))) |
123 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑛 = 𝑘 → (𝑐‘𝑛) = (𝑐‘𝑘)) |
124 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑘 = 𝑗 → (𝑏‘𝑘) = (𝑏‘𝑗)) |
125 | 124 | cbviunv 4495 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ∪ 𝑘 ∈ 𝑛 (𝑏‘𝑘) = ∪ 𝑗 ∈ 𝑛 (𝑏‘𝑗) |
126 | | iuneq1 4470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑛 = 𝑘 → ∪
𝑗 ∈ 𝑛 (𝑏‘𝑗) = ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) |
127 | 125, 126 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑛 = 𝑘 → ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘) = ∪ 𝑗 ∈ 𝑘 (𝑏‘𝑗)) |
128 | 61, 127 | difeq12d 3691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑛 = 𝑘 → ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) = ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗))) |
129 | 123, 128 | eleq12d 2682 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑛 = 𝑘 → ((𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) ↔ (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)))) |
130 | 129 | rspccv 3279 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∀𝑛 ∈
ω (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) → (𝑘 ∈ ω → (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)))) |
131 | 122, 130 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(∀𝑛 ∈
ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑘 ∈ ω → (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)))) |
132 | 131 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈ ω →
(∀𝑛 ∈ ω
(𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)))) |
133 | 132 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)))) |
134 | | eldifi 3694 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) → (𝑐‘𝑘) ∈ (𝑏‘𝑘)) |
135 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ (𝑏‘𝑘) ↔ (𝑐‘𝑛) ∈ (𝑏‘𝑘))) |
136 | 134, 135 | syl5ib 233 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) → (𝑐‘𝑛) ∈ (𝑏‘𝑘))) |
137 | 136 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) → (𝑐‘𝑛) ∈ (𝑏‘𝑘))) |
138 | 133, 137 | syld 46 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ (𝑏‘𝑘))) |
139 | 138 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ (𝑏‘𝑘)) |
140 | | ssiun2 4499 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ 𝑛 → (𝑏‘𝑘) ⊆ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) |
141 | 140 | sseld 3567 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ 𝑛 → ((𝑐‘𝑛) ∈ (𝑏‘𝑘) → (𝑐‘𝑛) ∈ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘))) |
142 | 139, 141 | syl5 33 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ 𝑛 → (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘))) |
143 | 142 | 3impib 1254 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ 𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) |
144 | 121 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ ω →
(∀𝑛 ∈ ω
(𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)))) |
145 | 144 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)))) |
146 | 145 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘))) |
147 | 146 | eldifbd 3553 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ¬ (𝑐‘𝑛) ∈ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) |
148 | 147 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ 𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ¬ (𝑐‘𝑛) ∈ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) |
149 | 143, 148 | pm2.21dd 185 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑘 ∈ 𝑛 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑘 = 𝑛) |
150 | 149 | 3exp 1256 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ 𝑛 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛))) |
151 | | 2a1 28 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑛 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛))) |
152 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑗 = 𝑛 → (𝑏‘𝑗) = (𝑏‘𝑛)) |
153 | 152 | ssiun2s 4500 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 ∈ 𝑘 → (𝑏‘𝑛) ⊆ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) |
154 | 153 | sseld 3567 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 ∈ 𝑘 → ((𝑐‘𝑛) ∈ (𝑏‘𝑛) → (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗))) |
155 | 102, 154 | syl5 33 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈ 𝑘 → ((𝑐‘𝑛) ∈ ((𝑏‘𝑛) ∖ ∪
𝑘 ∈ 𝑛 (𝑏‘𝑘)) → (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗))) |
156 | 146, 155 | syl5 33 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ 𝑘 → (((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗))) |
157 | 156 | 3impib 1254 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ 𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) |
158 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) ↔ (𝑐‘𝑛) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)))) |
159 | | eldifn 3695 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑐‘𝑛) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) → ¬ (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) |
160 | 158, 159 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) → ¬ (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗))) |
161 | 160 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → ((𝑐‘𝑘) ∈ ((𝑏‘𝑘) ∖ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) → ¬ (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗))) |
162 | 133, 161 | syld 46 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ¬ (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗))) |
163 | 162 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ 𝑘 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ¬ (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)))) |
164 | 163 | 3imp 1249 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ 𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ¬ (𝑐‘𝑛) ∈ ∪
𝑗 ∈ 𝑘 (𝑏‘𝑗)) |
165 | 157, 164 | pm2.21dd 185 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑛 ∈ 𝑘 ∧ (𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑘 = 𝑛) |
166 | 165 | 3exp 1256 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ 𝑘 → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛))) |
167 | 150, 151,
166 | 3jaoi 1383 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘) → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛))) |
168 | 167 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω ∧ (𝑐‘𝑘) = (𝑐‘𝑛)) → ((𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛))) |
169 | 168 | 3expia 1259 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐‘𝑘) = (𝑐‘𝑛) → ((𝑘 ∈ 𝑛 ∨ 𝑘 = 𝑛 ∨ 𝑛 ∈ 𝑘) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛)))) |
170 | 120, 169 | mpid 43 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐‘𝑘) = (𝑐‘𝑛) → (∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → 𝑘 = 𝑛))) |
171 | 170 | com3r 85 |
. . . . . . . . . . . . 13
⊢
(∀𝑛 ∈
ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ((𝑘 ∈ ω ∧ 𝑛 ∈ ω) → ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛))) |
172 | 171 | expd 451 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑘 ∈ ω → (𝑛 ∈ ω → ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛)))) |
173 | 95, 116, 172 | ralrimd 2942 |
. . . . . . . . . . 11
⊢
(∀𝑛 ∈
ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → (𝑘 ∈ ω → ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛))) |
174 | 173 | ralrimiv 2948 |
. . . . . . . . . 10
⊢
(∀𝑛 ∈
ω (𝑐‘𝑛) ∈ (𝐶‘𝑛) → ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛)) |
175 | 174 | 3ad2ant3 1077 |
. . . . . . . . 9
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛)) |
176 | | dff13 6416 |
. . . . . . . . 9
⊢ (𝑐:ω–1-1→𝐴 ↔ (𝑐:ω⟶𝐴 ∧ ∀𝑘 ∈ ω ∀𝑛 ∈ ω ((𝑐‘𝑘) = (𝑐‘𝑛) → 𝑘 = 𝑛))) |
177 | 115, 175,
176 | sylanbrc 695 |
. . . . . . . 8
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → 𝑐:ω–1-1→𝐴) |
178 | | 19.8a 2039 |
. . . . . . . 8
⊢ (𝑐:ω–1-1→𝐴 → ∃𝑐 𝑐:ω–1-1→𝐴) |
179 | 177, 178 | syl 17 |
. . . . . . 7
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ∃𝑐 𝑐:ω–1-1→𝐴) |
180 | 2 | brdom 7853 |
. . . . . . 7
⊢ (ω
≼ 𝐴 ↔
∃𝑐 𝑐:ω–1-1→𝐴) |
181 | 179, 180 | sylibr 223 |
. . . . . 6
⊢
((∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 ∧ 𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ω ≼ 𝐴) |
182 | 181 | 3expib 1260 |
. . . . 5
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → ((𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ω ≼ 𝐴)) |
183 | 182 | exlimdv 1848 |
. . . 4
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → (∃𝑐(𝑐 Fn ω ∧ ∀𝑛 ∈ ω (𝑐‘𝑛) ∈ (𝐶‘𝑛)) → ω ≼ 𝐴)) |
184 | 93, 183 | mpd 15 |
. . 3
⊢
(∀𝑛 ∈
ω (𝑏‘𝑛) ∈ 𝐵 → ω ≼ 𝐴) |
185 | 184 | exlimiv 1845 |
. 2
⊢
(∃𝑏∀𝑛 ∈ ω (𝑏‘𝑛) ∈ 𝐵 → ω ≼ 𝐴) |
186 | 48, 185 | syl 17 |
1
⊢ (¬
𝐴 ∈ Fin → ω
≼ 𝐴) |