Step | Hyp | Ref
| Expression |
1 | | fveq2 6919 |
. . 3
⊢ (𝑥 = 𝑦 → ( M ‘𝑥) = ( M ‘𝑦)) |
2 | 1 | eleq1d 2823 |
. 2
⊢ (𝑥 = 𝑦 → (( M ‘𝑥) ∈ Fin ↔ ( M ‘𝑦) ∈ Fin)) |
3 | | fveq2 6919 |
. . 3
⊢ (𝑥 = 𝐴 → ( M ‘𝑥) = ( M ‘𝐴)) |
4 | 3 | eleq1d 2823 |
. 2
⊢ (𝑥 = 𝐴 → (( M ‘𝑥) ∈ Fin ↔ ( M ‘𝐴) ∈ Fin)) |
5 | | nnon 7905 |
. . . . . 6
⊢ (𝑥 ∈ ω → 𝑥 ∈ On) |
6 | | madeval 27900 |
. . . . . 6
⊢ (𝑥 ∈ On → ( M
‘𝑥) = ( |s “
(𝒫 ∪ ( M “ 𝑥) × 𝒫 ∪ ( M “ 𝑥)))) |
7 | 5, 6 | syl 17 |
. . . . 5
⊢ (𝑥 ∈ ω → ( M
‘𝑥) = ( |s “
(𝒫 ∪ ( M “ 𝑥) × 𝒫 ∪ ( M “ 𝑥)))) |
8 | 7 | adantr 480 |
. . . 4
⊢ ((𝑥 ∈ ω ∧
∀𝑦 ∈ 𝑥 ( M ‘𝑦) ∈ Fin) → ( M ‘𝑥) = ( |s “ (𝒫
∪ ( M “ 𝑥) × 𝒫 ∪ ( M “ 𝑥)))) |
9 | | madef 27904 |
. . . . . . . . . . 11
⊢ M
:On⟶𝒫 No |
10 | | ffun 6749 |
. . . . . . . . . . 11
⊢ ( M
:On⟶𝒫 No → Fun M
) |
11 | 9, 10 | ax-mp 5 |
. . . . . . . . . 10
⊢ Fun
M |
12 | | nnfi 9229 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ω → 𝑥 ∈ Fin) |
13 | | imafi 9377 |
. . . . . . . . . 10
⊢ ((Fun M
∧ 𝑥 ∈ Fin) →
( M “ 𝑥) ∈
Fin) |
14 | 11, 12, 13 | sylancr 586 |
. . . . . . . . 9
⊢ (𝑥 ∈ ω → ( M
“ 𝑥) ∈
Fin) |
15 | 14 | adantr 480 |
. . . . . . . 8
⊢ ((𝑥 ∈ ω ∧
∀𝑦 ∈ 𝑥 ( M ‘𝑦) ∈ Fin) → ( M “ 𝑥) ∈ Fin) |
16 | | onss 7816 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ On → 𝑥 ⊆ On) |
17 | 5, 16 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ω → 𝑥 ⊆ On) |
18 | 9 | fdmi 6757 |
. . . . . . . . . . 11
⊢ dom M =
On |
19 | 17, 18 | sseqtrrdi 4054 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ω → 𝑥 ⊆ dom M
) |
20 | | funimass4 6985 |
. . . . . . . . . 10
⊢ ((Fun M
∧ 𝑥 ⊆ dom M )
→ (( M “ 𝑥)
⊆ Fin ↔ ∀𝑦 ∈ 𝑥 ( M ‘𝑦) ∈ Fin)) |
21 | 11, 19, 20 | sylancr 586 |
. . . . . . . . 9
⊢ (𝑥 ∈ ω → (( M
“ 𝑥) ⊆ Fin
↔ ∀𝑦 ∈
𝑥 ( M ‘𝑦) ∈ Fin)) |
22 | 21 | biimpar 477 |
. . . . . . . 8
⊢ ((𝑥 ∈ ω ∧
∀𝑦 ∈ 𝑥 ( M ‘𝑦) ∈ Fin) → ( M “ 𝑥) ⊆ Fin) |
23 | | unifi 9408 |
. . . . . . . 8
⊢ ((( M
“ 𝑥) ∈ Fin ∧
( M “ 𝑥) ⊆ Fin)
→ ∪ ( M “ 𝑥) ∈ Fin) |
24 | 15, 22, 23 | syl2anc 583 |
. . . . . . 7
⊢ ((𝑥 ∈ ω ∧
∀𝑦 ∈ 𝑥 ( M ‘𝑦) ∈ Fin) → ∪ ( M “ 𝑥) ∈ Fin) |
25 | | pwfi 9381 |
. . . . . . 7
⊢ (∪ ( M “ 𝑥) ∈ Fin ↔ 𝒫 ∪ ( M “ 𝑥) ∈ Fin) |
26 | 24, 25 | sylib 218 |
. . . . . 6
⊢ ((𝑥 ∈ ω ∧
∀𝑦 ∈ 𝑥 ( M ‘𝑦) ∈ Fin) → 𝒫 ∪ ( M “ 𝑥) ∈ Fin) |
27 | | xpfi 9382 |
. . . . . 6
⊢
((𝒫 ∪ ( M “ 𝑥) ∈ Fin ∧ 𝒫 ∪ ( M “ 𝑥) ∈ Fin) → (𝒫 ∪ ( M “ 𝑥) × 𝒫 ∪ ( M “ 𝑥)) ∈ Fin) |
28 | 26, 26, 27 | syl2anc 583 |
. . . . 5
⊢ ((𝑥 ∈ ω ∧
∀𝑦 ∈ 𝑥 ( M ‘𝑦) ∈ Fin) → (𝒫 ∪ ( M “ 𝑥) × 𝒫 ∪ ( M “ 𝑥)) ∈ Fin) |
29 | | vex 3486 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
30 | 29 | funimaex 6665 |
. . . . . . . . . 10
⊢ (Fun M
→ ( M “ 𝑥)
∈ V) |
31 | 11, 30 | ax-mp 5 |
. . . . . . . . 9
⊢ ( M
“ 𝑥) ∈
V |
32 | 31 | uniex 7772 |
. . . . . . . 8
⊢ ∪ ( M “ 𝑥) ∈ V |
33 | 32 | pwex 5401 |
. . . . . . 7
⊢ 𝒫
∪ ( M “ 𝑥) ∈ V |
34 | 33, 33 | xpex 7784 |
. . . . . 6
⊢
(𝒫 ∪ ( M “ 𝑥) × 𝒫 ∪ ( M “ 𝑥)) ∈ V |
35 | | scutf 27866 |
. . . . . . 7
⊢ |s :
<<s ⟶ No |
36 | | ffun 6749 |
. . . . . . 7
⊢ ( |s :
<<s ⟶ No → Fun |s
) |
37 | 35, 36 | ax-mp 5 |
. . . . . 6
⊢ Fun
|s |
38 | | imadomg 10599 |
. . . . . 6
⊢
((𝒫 ∪ ( M “ 𝑥) × 𝒫 ∪ ( M “ 𝑥)) ∈ V → (Fun |s → ( |s
“ (𝒫 ∪ ( M “ 𝑥) × 𝒫 ∪ ( M “ 𝑥))) ≼ (𝒫 ∪ ( M “ 𝑥) × 𝒫 ∪ ( M “ 𝑥)))) |
39 | 34, 37, 38 | mp2 9 |
. . . . 5
⊢ ( |s
“ (𝒫 ∪ ( M “ 𝑥) × 𝒫 ∪ ( M “ 𝑥))) ≼ (𝒫 ∪ ( M “ 𝑥) × 𝒫 ∪ ( M “ 𝑥)) |
40 | | domfi 9251 |
. . . . 5
⊢
(((𝒫 ∪ ( M “ 𝑥) × 𝒫 ∪ ( M “ 𝑥)) ∈ Fin ∧ ( |s “ (𝒫
∪ ( M “ 𝑥) × 𝒫 ∪ ( M “ 𝑥))) ≼ (𝒫 ∪ ( M “ 𝑥) × 𝒫 ∪ ( M “ 𝑥))) → ( |s “ (𝒫 ∪ ( M “ 𝑥) × 𝒫 ∪ ( M “ 𝑥))) ∈ Fin) |
41 | 28, 39, 40 | sylancl 585 |
. . . 4
⊢ ((𝑥 ∈ ω ∧
∀𝑦 ∈ 𝑥 ( M ‘𝑦) ∈ Fin) → ( |s “ (𝒫
∪ ( M “ 𝑥) × 𝒫 ∪ ( M “ 𝑥))) ∈ Fin) |
42 | 8, 41 | eqeltrd 2838 |
. . 3
⊢ ((𝑥 ∈ ω ∧
∀𝑦 ∈ 𝑥 ( M ‘𝑦) ∈ Fin) → ( M ‘𝑥) ∈ Fin) |
43 | 42 | ex 412 |
. 2
⊢ (𝑥 ∈ ω →
(∀𝑦 ∈ 𝑥 ( M ‘𝑦) ∈ Fin → ( M ‘𝑥) ∈ Fin)) |
44 | 2, 4, 43 | omsinds 7920 |
1
⊢ (𝐴 ∈ ω → ( M
‘𝐴) ∈
Fin) |