Step | Hyp | Ref
| Expression |
1 | | frn 5966 |
. . . . . . 7
⊢ (𝑓:𝐵⟶𝐴 → ran 𝑓 ⊆ 𝐴) |
2 | 1 | adantr 480 |
. . . . . 6
⊢ ((𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → ran 𝑓 ⊆ 𝐴) |
3 | | ffn 5958 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐵⟶𝐴 → 𝑓 Fn 𝐵) |
4 | | fnfvelrn 6264 |
. . . . . . . . . . . 12
⊢ ((𝑓 Fn 𝐵 ∧ 𝑤 ∈ 𝐵) → (𝑓‘𝑤) ∈ ran 𝑓) |
5 | 3, 4 | sylan 487 |
. . . . . . . . . . 11
⊢ ((𝑓:𝐵⟶𝐴 ∧ 𝑤 ∈ 𝐵) → (𝑓‘𝑤) ∈ ran 𝑓) |
6 | | sseq2 3590 |
. . . . . . . . . . . 12
⊢ (𝑠 = (𝑓‘𝑤) → (𝑧 ⊆ 𝑠 ↔ 𝑧 ⊆ (𝑓‘𝑤))) |
7 | 6 | rspcev 3282 |
. . . . . . . . . . 11
⊢ (((𝑓‘𝑤) ∈ ran 𝑓 ∧ 𝑧 ⊆ (𝑓‘𝑤)) → ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠) |
8 | 5, 7 | sylan 487 |
. . . . . . . . . 10
⊢ (((𝑓:𝐵⟶𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ⊆ (𝑓‘𝑤)) → ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠) |
9 | 8 | exp31 628 |
. . . . . . . . 9
⊢ (𝑓:𝐵⟶𝐴 → (𝑤 ∈ 𝐵 → (𝑧 ⊆ (𝑓‘𝑤) → ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠))) |
10 | 9 | rexlimdv 3012 |
. . . . . . . 8
⊢ (𝑓:𝐵⟶𝐴 → (∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤) → ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) |
11 | 10 | ralimdv 2946 |
. . . . . . 7
⊢ (𝑓:𝐵⟶𝐴 → (∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤) → ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) |
12 | 11 | imp 444 |
. . . . . 6
⊢ ((𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠) |
13 | 2, 12 | jca 553 |
. . . . 5
⊢ ((𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) |
14 | | fvex 6113 |
. . . . . 6
⊢
(card‘ran 𝑓)
∈ V |
15 | | cfval 8952 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ On →
(cf‘𝐴) = ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))}) |
16 | 15 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
(cf‘𝐴) = ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))}) |
17 | 16 | 3ad2ant2 1076 |
. . . . . . . . 9
⊢ ((𝑥 = (card‘ran 𝑓) ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) → (cf‘𝐴) = ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))}) |
18 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑓 ∈ V |
19 | 18 | rnex 6992 |
. . . . . . . . . . . . 13
⊢ ran 𝑓 ∈ V |
20 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = ran 𝑓 → (card‘𝑦) = (card‘ran 𝑓)) |
21 | 20 | eqeq2d 2620 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ran 𝑓 → (𝑥 = (card‘𝑦) ↔ 𝑥 = (card‘ran 𝑓))) |
22 | | sseq1 3589 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = ran 𝑓 → (𝑦 ⊆ 𝐴 ↔ ran 𝑓 ⊆ 𝐴)) |
23 | | rexeq 3116 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = ran 𝑓 → (∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ↔ ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) |
24 | 23 | ralbidv 2969 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = ran 𝑓 → (∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ↔ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) |
25 | 22, 24 | anbi12d 743 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ran 𝑓 → ((𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠) ↔ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠))) |
26 | 21, 25 | anbi12d 743 |
. . . . . . . . . . . . 13
⊢ (𝑦 = ran 𝑓 → ((𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠)) ↔ (𝑥 = (card‘ran 𝑓) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)))) |
27 | 19, 26 | spcev 3273 |
. . . . . . . . . . . 12
⊢ ((𝑥 = (card‘ran 𝑓) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) → ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))) |
28 | | abid 2598 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))} ↔ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))) |
29 | 27, 28 | sylibr 223 |
. . . . . . . . . . 11
⊢ ((𝑥 = (card‘ran 𝑓) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) → 𝑥 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))}) |
30 | | intss1 4427 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))} → ∩
{𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))} ⊆ 𝑥) |
31 | 29, 30 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑥 = (card‘ran 𝑓) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) → ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))} ⊆ 𝑥) |
32 | 31 | 3adant2 1073 |
. . . . . . . . 9
⊢ ((𝑥 = (card‘ran 𝑓) ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) → ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))} ⊆ 𝑥) |
33 | 17, 32 | eqsstrd 3602 |
. . . . . . . 8
⊢ ((𝑥 = (card‘ran 𝑓) ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) → (cf‘𝐴) ⊆ 𝑥) |
34 | 33 | 3expib 1260 |
. . . . . . 7
⊢ (𝑥 = (card‘ran 𝑓) → (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) → (cf‘𝐴) ⊆ 𝑥)) |
35 | | sseq2 3590 |
. . . . . . 7
⊢ (𝑥 = (card‘ran 𝑓) → ((cf‘𝐴) ⊆ 𝑥 ↔ (cf‘𝐴) ⊆ (card‘ran 𝑓))) |
36 | 34, 35 | sylibd 228 |
. . . . . 6
⊢ (𝑥 = (card‘ran 𝑓) → (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) → (cf‘𝐴) ⊆ (card‘ran 𝑓))) |
37 | 14, 36 | vtocle 3255 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) → (cf‘𝐴) ⊆ (card‘ran 𝑓)) |
38 | 13, 37 | sylan2 490 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → (cf‘𝐴) ⊆ (card‘ran 𝑓)) |
39 | | cardidm 8668 |
. . . . . . 7
⊢
(card‘(card‘ran 𝑓)) = (card‘ran 𝑓) |
40 | | onss 6882 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ On → 𝐴 ⊆ On) |
41 | 1, 40 | sylan9ssr 3582 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ 𝑓:𝐵⟶𝐴) → ran 𝑓 ⊆ On) |
42 | 41 | 3adant2 1073 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → ran 𝑓 ⊆ On) |
43 | | onssnum 8746 |
. . . . . . . . . . . 12
⊢ ((ran
𝑓 ∈ V ∧ ran 𝑓 ⊆ On) → ran 𝑓 ∈ dom
card) |
44 | 19, 42, 43 | sylancr 694 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → ran 𝑓 ∈ dom card) |
45 | | cardid2 8662 |
. . . . . . . . . . 11
⊢ (ran
𝑓 ∈ dom card →
(card‘ran 𝑓) ≈
ran 𝑓) |
46 | 44, 45 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → (card‘ran 𝑓) ≈ ran 𝑓) |
47 | | onenon 8658 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ On → 𝐵 ∈ dom
card) |
48 | | dffn4 6034 |
. . . . . . . . . . . . . 14
⊢ (𝑓 Fn 𝐵 ↔ 𝑓:𝐵–onto→ran 𝑓) |
49 | 3, 48 | sylib 207 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐵⟶𝐴 → 𝑓:𝐵–onto→ran 𝑓) |
50 | | fodomnum 8763 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ dom card → (𝑓:𝐵–onto→ran 𝑓 → ran 𝑓 ≼ 𝐵)) |
51 | 47, 49, 50 | syl2im 39 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ On → (𝑓:𝐵⟶𝐴 → ran 𝑓 ≼ 𝐵)) |
52 | 51 | imp 444 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → ran 𝑓 ≼ 𝐵) |
53 | 52 | 3adant1 1072 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → ran 𝑓 ≼ 𝐵) |
54 | | endomtr 7900 |
. . . . . . . . . 10
⊢
(((card‘ran 𝑓)
≈ ran 𝑓 ∧ ran
𝑓 ≼ 𝐵) → (card‘ran 𝑓) ≼ 𝐵) |
55 | 46, 53, 54 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → (card‘ran 𝑓) ≼ 𝐵) |
56 | | cardon 8653 |
. . . . . . . . . . . 12
⊢
(card‘ran 𝑓)
∈ On |
57 | | onenon 8658 |
. . . . . . . . . . . 12
⊢
((card‘ran 𝑓)
∈ On → (card‘ran 𝑓) ∈ dom card) |
58 | 56, 57 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(card‘ran 𝑓)
∈ dom card |
59 | | carddom2 8686 |
. . . . . . . . . . 11
⊢
(((card‘ran 𝑓)
∈ dom card ∧ 𝐵
∈ dom card) → ((card‘(card‘ran 𝑓)) ⊆ (card‘𝐵) ↔ (card‘ran 𝑓) ≼ 𝐵)) |
60 | 58, 47, 59 | sylancr 694 |
. . . . . . . . . 10
⊢ (𝐵 ∈ On →
((card‘(card‘ran 𝑓)) ⊆ (card‘𝐵) ↔ (card‘ran 𝑓) ≼ 𝐵)) |
61 | 60 | 3ad2ant2 1076 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → ((card‘(card‘ran 𝑓)) ⊆ (card‘𝐵) ↔ (card‘ran 𝑓) ≼ 𝐵)) |
62 | 55, 61 | mpbird 246 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → (card‘(card‘ran 𝑓)) ⊆ (card‘𝐵)) |
63 | | cardonle 8666 |
. . . . . . . . 9
⊢ (𝐵 ∈ On →
(card‘𝐵) ⊆
𝐵) |
64 | 63 | 3ad2ant2 1076 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → (card‘𝐵) ⊆ 𝐵) |
65 | 62, 64 | sstrd 3578 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → (card‘(card‘ran 𝑓)) ⊆ 𝐵) |
66 | 39, 65 | syl5eqssr 3613 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → (card‘ran 𝑓) ⊆ 𝐵) |
67 | 66 | 3expa 1257 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → (card‘ran 𝑓) ⊆ 𝐵) |
68 | 67 | adantrr 749 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → (card‘ran 𝑓) ⊆ 𝐵) |
69 | 38, 68 | sstrd 3578 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → (cf‘𝐴) ⊆ 𝐵) |
70 | 69 | ex 449 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → (cf‘𝐴) ⊆ 𝐵)) |
71 | 70 | exlimdv 1848 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∃𝑓(𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → (cf‘𝐴) ⊆ 𝐵)) |