| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | frn 6742 | . . . . . . 7
⊢ (𝑓:𝐵⟶𝐴 → ran 𝑓 ⊆ 𝐴) | 
| 2 | 1 | adantr 480 | . . . . . 6
⊢ ((𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → ran 𝑓 ⊆ 𝐴) | 
| 3 |  | ffn 6735 | . . . . . . . . . . 11
⊢ (𝑓:𝐵⟶𝐴 → 𝑓 Fn 𝐵) | 
| 4 |  | fnfvelrn 7099 | . . . . . . . . . . 11
⊢ ((𝑓 Fn 𝐵 ∧ 𝑤 ∈ 𝐵) → (𝑓‘𝑤) ∈ ran 𝑓) | 
| 5 | 3, 4 | sylan 580 | . . . . . . . . . 10
⊢ ((𝑓:𝐵⟶𝐴 ∧ 𝑤 ∈ 𝐵) → (𝑓‘𝑤) ∈ ran 𝑓) | 
| 6 |  | sseq2 4009 | . . . . . . . . . . 11
⊢ (𝑠 = (𝑓‘𝑤) → (𝑧 ⊆ 𝑠 ↔ 𝑧 ⊆ (𝑓‘𝑤))) | 
| 7 | 6 | rspcev 3621 | . . . . . . . . . 10
⊢ (((𝑓‘𝑤) ∈ ran 𝑓 ∧ 𝑧 ⊆ (𝑓‘𝑤)) → ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠) | 
| 8 | 5, 7 | sylan 580 | . . . . . . . . 9
⊢ (((𝑓:𝐵⟶𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑧 ⊆ (𝑓‘𝑤)) → ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠) | 
| 9 | 8 | rexlimdva2 3156 | . . . . . . . 8
⊢ (𝑓:𝐵⟶𝐴 → (∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤) → ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) | 
| 10 | 9 | ralimdv 3168 | . . . . . . 7
⊢ (𝑓:𝐵⟶𝐴 → (∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤) → ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) | 
| 11 | 10 | imp 406 | . . . . . 6
⊢ ((𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠) | 
| 12 | 2, 11 | jca 511 | . . . . 5
⊢ ((𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) | 
| 13 |  | fvex 6918 | . . . . . 6
⊢
(card‘ran 𝑓)
∈ V | 
| 14 |  | cfval 10288 | . . . . . . . . . . 11
⊢ (𝐴 ∈ On →
(cf‘𝐴) = ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))}) | 
| 15 | 14 | adantr 480 | . . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
(cf‘𝐴) = ∩ {𝑥
∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))}) | 
| 16 | 15 | 3ad2ant2 1134 | . . . . . . . . 9
⊢ ((𝑥 = (card‘ran 𝑓) ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) → (cf‘𝐴) = ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))}) | 
| 17 |  | vex 3483 | . . . . . . . . . . . . . 14
⊢ 𝑓 ∈ V | 
| 18 | 17 | rnex 7933 | . . . . . . . . . . . . 13
⊢ ran 𝑓 ∈ V | 
| 19 |  | fveq2 6905 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = ran 𝑓 → (card‘𝑦) = (card‘ran 𝑓)) | 
| 20 | 19 | eqeq2d 2747 | . . . . . . . . . . . . . 14
⊢ (𝑦 = ran 𝑓 → (𝑥 = (card‘𝑦) ↔ 𝑥 = (card‘ran 𝑓))) | 
| 21 |  | sseq1 4008 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = ran 𝑓 → (𝑦 ⊆ 𝐴 ↔ ran 𝑓 ⊆ 𝐴)) | 
| 22 |  | rexeq 3321 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = ran 𝑓 → (∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ↔ ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) | 
| 23 | 22 | ralbidv 3177 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = ran 𝑓 → (∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ↔ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) | 
| 24 | 21, 23 | anbi12d 632 | . . . . . . . . . . . . . 14
⊢ (𝑦 = ran 𝑓 → ((𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠) ↔ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠))) | 
| 25 | 20, 24 | anbi12d 632 | . . . . . . . . . . . . 13
⊢ (𝑦 = ran 𝑓 → ((𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠)) ↔ (𝑥 = (card‘ran 𝑓) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)))) | 
| 26 | 18, 25 | spcev 3605 | . . . . . . . . . . . 12
⊢ ((𝑥 = (card‘ran 𝑓) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) → ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))) | 
| 27 |  | abid 2717 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))} ↔ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))) | 
| 28 | 26, 27 | sylibr 234 | . . . . . . . . . . 11
⊢ ((𝑥 = (card‘ran 𝑓) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) → 𝑥 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))}) | 
| 29 |  | intss1 4962 | . . . . . . . . . . 11
⊢ (𝑥 ∈ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))} → ∩
{𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))} ⊆ 𝑥) | 
| 30 | 28, 29 | syl 17 | . . . . . . . . . 10
⊢ ((𝑥 = (card‘ran 𝑓) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) → ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))} ⊆ 𝑥) | 
| 31 | 30 | 3adant2 1131 | . . . . . . . . 9
⊢ ((𝑥 = (card‘ran 𝑓) ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) → ∩ {𝑥 ∣ ∃𝑦(𝑥 = (card‘𝑦) ∧ (𝑦 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠))} ⊆ 𝑥) | 
| 32 | 16, 31 | eqsstrd 4017 | . . . . . . . 8
⊢ ((𝑥 = (card‘ran 𝑓) ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) → (cf‘𝐴) ⊆ 𝑥) | 
| 33 | 32 | 3expib 1122 | . . . . . . 7
⊢ (𝑥 = (card‘ran 𝑓) → (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) → (cf‘𝐴) ⊆ 𝑥)) | 
| 34 |  | sseq2 4009 | . . . . . . 7
⊢ (𝑥 = (card‘ran 𝑓) → ((cf‘𝐴) ⊆ 𝑥 ↔ (cf‘𝐴) ⊆ (card‘ran 𝑓))) | 
| 35 | 33, 34 | sylibd 239 | . . . . . 6
⊢ (𝑥 = (card‘ran 𝑓) → (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) → (cf‘𝐴) ⊆ (card‘ran 𝑓))) | 
| 36 | 13, 35 | vtocle 3554 | . . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (ran 𝑓 ⊆ 𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠)) → (cf‘𝐴) ⊆ (card‘ran 𝑓)) | 
| 37 | 12, 36 | sylan2 593 | . . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → (cf‘𝐴) ⊆ (card‘ran 𝑓)) | 
| 38 |  | cardidm 10000 | . . . . . . 7
⊢
(card‘(card‘ran 𝑓)) = (card‘ran 𝑓) | 
| 39 |  | onss 7806 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ On → 𝐴 ⊆ On) | 
| 40 | 1, 39 | sylan9ssr 3997 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ 𝑓:𝐵⟶𝐴) → ran 𝑓 ⊆ On) | 
| 41 | 40 | 3adant2 1131 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → ran 𝑓 ⊆ On) | 
| 42 |  | onssnum 10081 | . . . . . . . . . . . 12
⊢ ((ran
𝑓 ∈ V ∧ ran 𝑓 ⊆ On) → ran 𝑓 ∈ dom
card) | 
| 43 | 18, 41, 42 | sylancr 587 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → ran 𝑓 ∈ dom card) | 
| 44 |  | cardid2 9994 | . . . . . . . . . . 11
⊢ (ran
𝑓 ∈ dom card →
(card‘ran 𝑓) ≈
ran 𝑓) | 
| 45 | 43, 44 | syl 17 | . . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → (card‘ran 𝑓) ≈ ran 𝑓) | 
| 46 |  | onenon 9990 | . . . . . . . . . . . . 13
⊢ (𝐵 ∈ On → 𝐵 ∈ dom
card) | 
| 47 |  | dffn4 6825 | . . . . . . . . . . . . . 14
⊢ (𝑓 Fn 𝐵 ↔ 𝑓:𝐵–onto→ran 𝑓) | 
| 48 | 3, 47 | sylib 218 | . . . . . . . . . . . . 13
⊢ (𝑓:𝐵⟶𝐴 → 𝑓:𝐵–onto→ran 𝑓) | 
| 49 |  | fodomnum 10098 | . . . . . . . . . . . . 13
⊢ (𝐵 ∈ dom card → (𝑓:𝐵–onto→ran 𝑓 → ran 𝑓 ≼ 𝐵)) | 
| 50 | 46, 48, 49 | syl2im 40 | . . . . . . . . . . . 12
⊢ (𝐵 ∈ On → (𝑓:𝐵⟶𝐴 → ran 𝑓 ≼ 𝐵)) | 
| 51 | 50 | imp 406 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → ran 𝑓 ≼ 𝐵) | 
| 52 | 51 | 3adant1 1130 | . . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → ran 𝑓 ≼ 𝐵) | 
| 53 |  | endomtr 9053 | . . . . . . . . . 10
⊢
(((card‘ran 𝑓)
≈ ran 𝑓 ∧ ran
𝑓 ≼ 𝐵) → (card‘ran 𝑓) ≼ 𝐵) | 
| 54 | 45, 52, 53 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → (card‘ran 𝑓) ≼ 𝐵) | 
| 55 |  | cardon 9985 | . . . . . . . . . . . 12
⊢
(card‘ran 𝑓)
∈ On | 
| 56 |  | onenon 9990 | . . . . . . . . . . . 12
⊢
((card‘ran 𝑓)
∈ On → (card‘ran 𝑓) ∈ dom card) | 
| 57 | 55, 56 | ax-mp 5 | . . . . . . . . . . 11
⊢
(card‘ran 𝑓)
∈ dom card | 
| 58 |  | carddom2 10018 | . . . . . . . . . . 11
⊢
(((card‘ran 𝑓)
∈ dom card ∧ 𝐵
∈ dom card) → ((card‘(card‘ran 𝑓)) ⊆ (card‘𝐵) ↔ (card‘ran 𝑓) ≼ 𝐵)) | 
| 59 | 57, 46, 58 | sylancr 587 | . . . . . . . . . 10
⊢ (𝐵 ∈ On →
((card‘(card‘ran 𝑓)) ⊆ (card‘𝐵) ↔ (card‘ran 𝑓) ≼ 𝐵)) | 
| 60 | 59 | 3ad2ant2 1134 | . . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → ((card‘(card‘ran 𝑓)) ⊆ (card‘𝐵) ↔ (card‘ran 𝑓) ≼ 𝐵)) | 
| 61 | 54, 60 | mpbird 257 | . . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → (card‘(card‘ran 𝑓)) ⊆ (card‘𝐵)) | 
| 62 |  | cardonle 9998 | . . . . . . . . 9
⊢ (𝐵 ∈ On →
(card‘𝐵) ⊆
𝐵) | 
| 63 | 62 | 3ad2ant2 1134 | . . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → (card‘𝐵) ⊆ 𝐵) | 
| 64 | 61, 63 | sstrd 3993 | . . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → (card‘(card‘ran 𝑓)) ⊆ 𝐵) | 
| 65 | 38, 64 | eqsstrrid 4022 | . . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓:𝐵⟶𝐴) → (card‘ran 𝑓) ⊆ 𝐵) | 
| 66 | 65 | 3expa 1118 | . . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑓:𝐵⟶𝐴) → (card‘ran 𝑓) ⊆ 𝐵) | 
| 67 | 66 | adantrr 717 | . . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → (card‘ran 𝑓) ⊆ 𝐵) | 
| 68 | 37, 67 | sstrd 3993 | . . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤))) → (cf‘𝐴) ⊆ 𝐵) | 
| 69 | 68 | ex 412 | . 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → (cf‘𝐴) ⊆ 𝐵)) | 
| 70 | 69 | exlimdv 1932 | 1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∃𝑓(𝑓:𝐵⟶𝐴 ∧ ∀𝑧 ∈ 𝐴 ∃𝑤 ∈ 𝐵 𝑧 ⊆ (𝑓‘𝑤)) → (cf‘𝐴) ⊆ 𝐵)) |