| Step | Hyp | Ref
| Expression |
| 1 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑧𝜑 |
| 2 | | nfsbc1v 3808 |
. . . . . 6
⊢
Ⅎ𝑦[𝑧 / 𝑦]𝜑 |
| 3 | | sbceq1a 3799 |
. . . . . 6
⊢ (𝑦 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑦]𝜑)) |
| 4 | 1, 2, 3 | cbvrexw 3307 |
. . . . 5
⊢
(∃𝑦 ∈
𝐵 𝜑 ↔ ∃𝑧 ∈ 𝐵 [𝑧 / 𝑦]𝜑) |
| 5 | 4 | ralbii 3093 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐵 [𝑧 / 𝑦]𝜑) |
| 6 | | dfsbcq 3790 |
. . . . 5
⊢ (𝑧 = (𝑓‘𝑥) → ([𝑧 / 𝑦]𝜑 ↔ [(𝑓‘𝑥) / 𝑦]𝜑)) |
| 7 | 6 | ac6sfi 9320 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑧 ∈ 𝐵 [𝑧 / 𝑦]𝜑) → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑)) |
| 8 | 5, 7 | sylan2b 594 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑)) |
| 9 | | simpll 767 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑)) → 𝐴 ∈ Fin) |
| 10 | | ffn 6736 |
. . . . . . 7
⊢ (𝑓:𝐴⟶𝐵 → 𝑓 Fn 𝐴) |
| 11 | 10 | ad2antrl 728 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑)) → 𝑓 Fn 𝐴) |
| 12 | | dffn4 6826 |
. . . . . 6
⊢ (𝑓 Fn 𝐴 ↔ 𝑓:𝐴–onto→ran 𝑓) |
| 13 | 11, 12 | sylib 218 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑)) → 𝑓:𝐴–onto→ran 𝑓) |
| 14 | | fofi 9351 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝑓:𝐴–onto→ran 𝑓) → ran 𝑓 ∈ Fin) |
| 15 | 9, 13, 14 | syl2anc 584 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑)) → ran 𝑓 ∈ Fin) |
| 16 | | frn 6743 |
. . . . 5
⊢ (𝑓:𝐴⟶𝐵 → ran 𝑓 ⊆ 𝐵) |
| 17 | 16 | ad2antrl 728 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑)) → ran 𝑓 ⊆ 𝐵) |
| 18 | | fnfvelrn 7100 |
. . . . . . . . 9
⊢ ((𝑓 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ran 𝑓) |
| 19 | 10, 18 | sylan 580 |
. . . . . . . 8
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ran 𝑓) |
| 20 | | rspesbca 3881 |
. . . . . . . . 9
⊢ (((𝑓‘𝑥) ∈ ran 𝑓 ∧ [(𝑓‘𝑥) / 𝑦]𝜑) → ∃𝑦 ∈ ran 𝑓𝜑) |
| 21 | 20 | ex 412 |
. . . . . . . 8
⊢ ((𝑓‘𝑥) ∈ ran 𝑓 → ([(𝑓‘𝑥) / 𝑦]𝜑 → ∃𝑦 ∈ ran 𝑓𝜑)) |
| 22 | 19, 21 | syl 17 |
. . . . . . 7
⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → ([(𝑓‘𝑥) / 𝑦]𝜑 → ∃𝑦 ∈ ran 𝑓𝜑)) |
| 23 | 22 | ralimdva 3167 |
. . . . . 6
⊢ (𝑓:𝐴⟶𝐵 → (∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ran 𝑓𝜑)) |
| 24 | 23 | imp 406 |
. . . . 5
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ran 𝑓𝜑) |
| 25 | 24 | adantl 481 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑)) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ran 𝑓𝜑) |
| 26 | | simpr 484 |
. . . . . . . 8
⊢ ((((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑)) ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ 𝐴) |
| 27 | | simprr 773 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑)) → ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) |
| 28 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑤[(𝑓‘𝑥) / 𝑦]𝜑 |
| 29 | | nfsbc1v 3808 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥[𝑤 / 𝑥][(𝑓‘𝑤) / 𝑦]𝜑 |
| 30 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑤 → (𝑓‘𝑥) = (𝑓‘𝑤)) |
| 31 | 30 | sbceq1d 3793 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → ([(𝑓‘𝑥) / 𝑦]𝜑 ↔ [(𝑓‘𝑤) / 𝑦]𝜑)) |
| 32 | | sbceq1a 3799 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑤 → ([(𝑓‘𝑤) / 𝑦]𝜑 ↔ [𝑤 / 𝑥][(𝑓‘𝑤) / 𝑦]𝜑)) |
| 33 | 31, 32 | bitrd 279 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑤 → ([(𝑓‘𝑥) / 𝑦]𝜑 ↔ [𝑤 / 𝑥][(𝑓‘𝑤) / 𝑦]𝜑)) |
| 34 | 28, 29, 33 | cbvralw 3306 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝐴 [(𝑓‘𝑥) / 𝑦]𝜑 ↔ ∀𝑤 ∈ 𝐴 [𝑤 / 𝑥][(𝑓‘𝑤) / 𝑦]𝜑) |
| 35 | 27, 34 | sylib 218 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑)) → ∀𝑤 ∈ 𝐴 [𝑤 / 𝑥][(𝑓‘𝑤) / 𝑦]𝜑) |
| 36 | 35 | r19.21bi 3251 |
. . . . . . . 8
⊢ ((((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑)) ∧ 𝑤 ∈ 𝐴) → [𝑤 / 𝑥][(𝑓‘𝑤) / 𝑦]𝜑) |
| 37 | | rspesbca 3881 |
. . . . . . . 8
⊢ ((𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥][(𝑓‘𝑤) / 𝑦]𝜑) → ∃𝑥 ∈ 𝐴 [(𝑓‘𝑤) / 𝑦]𝜑) |
| 38 | 26, 36, 37 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑)) ∧ 𝑤 ∈ 𝐴) → ∃𝑥 ∈ 𝐴 [(𝑓‘𝑤) / 𝑦]𝜑) |
| 39 | 38 | ralrimiva 3146 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑)) → ∀𝑤 ∈ 𝐴 ∃𝑥 ∈ 𝐴 [(𝑓‘𝑤) / 𝑦]𝜑) |
| 40 | | dfsbcq 3790 |
. . . . . . . . 9
⊢ (𝑧 = (𝑓‘𝑤) → ([𝑧 / 𝑦]𝜑 ↔ [(𝑓‘𝑤) / 𝑦]𝜑)) |
| 41 | 40 | rexbidv 3179 |
. . . . . . . 8
⊢ (𝑧 = (𝑓‘𝑤) → (∃𝑥 ∈ 𝐴 [𝑧 / 𝑦]𝜑 ↔ ∃𝑥 ∈ 𝐴 [(𝑓‘𝑤) / 𝑦]𝜑)) |
| 42 | 41 | ralrn 7108 |
. . . . . . 7
⊢ (𝑓 Fn 𝐴 → (∀𝑧 ∈ ran 𝑓∃𝑥 ∈ 𝐴 [𝑧 / 𝑦]𝜑 ↔ ∀𝑤 ∈ 𝐴 ∃𝑥 ∈ 𝐴 [(𝑓‘𝑤) / 𝑦]𝜑)) |
| 43 | 11, 42 | syl 17 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑)) → (∀𝑧 ∈ ran 𝑓∃𝑥 ∈ 𝐴 [𝑧 / 𝑦]𝜑 ↔ ∀𝑤 ∈ 𝐴 ∃𝑥 ∈ 𝐴 [(𝑓‘𝑤) / 𝑦]𝜑)) |
| 44 | 39, 43 | mpbird 257 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑)) → ∀𝑧 ∈ ran 𝑓∃𝑥 ∈ 𝐴 [𝑧 / 𝑦]𝜑) |
| 45 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑧∃𝑥 ∈ 𝐴 𝜑 |
| 46 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑦𝐴 |
| 47 | 46, 2 | nfrexw 3313 |
. . . . . 6
⊢
Ⅎ𝑦∃𝑥 ∈ 𝐴 [𝑧 / 𝑦]𝜑 |
| 48 | 3 | rexbidv 3179 |
. . . . . 6
⊢ (𝑦 = 𝑧 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 [𝑧 / 𝑦]𝜑)) |
| 49 | 45, 47, 48 | cbvralw 3306 |
. . . . 5
⊢
(∀𝑦 ∈
ran 𝑓∃𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑧 ∈ ran 𝑓∃𝑥 ∈ 𝐴 [𝑧 / 𝑦]𝜑) |
| 50 | 44, 49 | sylibr 234 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑)) → ∀𝑦 ∈ ran 𝑓∃𝑥 ∈ 𝐴 𝜑) |
| 51 | | sseq1 4009 |
. . . . . 6
⊢ (𝑐 = ran 𝑓 → (𝑐 ⊆ 𝐵 ↔ ran 𝑓 ⊆ 𝐵)) |
| 52 | | rexeq 3322 |
. . . . . . 7
⊢ (𝑐 = ran 𝑓 → (∃𝑦 ∈ 𝑐 𝜑 ↔ ∃𝑦 ∈ ran 𝑓𝜑)) |
| 53 | 52 | ralbidv 3178 |
. . . . . 6
⊢ (𝑐 = ran 𝑓 → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ran 𝑓𝜑)) |
| 54 | | raleq 3323 |
. . . . . 6
⊢ (𝑐 = ran 𝑓 → (∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ ran 𝑓∃𝑥 ∈ 𝐴 𝜑)) |
| 55 | 51, 53, 54 | 3anbi123d 1438 |
. . . . 5
⊢ (𝑐 = ran 𝑓 → ((𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑) ↔ (ran 𝑓 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ran 𝑓𝜑 ∧ ∀𝑦 ∈ ran 𝑓∃𝑥 ∈ 𝐴 𝜑))) |
| 56 | 55 | rspcev 3622 |
. . . 4
⊢ ((ran
𝑓 ∈ Fin ∧ (ran
𝑓 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ran 𝑓𝜑 ∧ ∀𝑦 ∈ ran 𝑓∃𝑥 ∈ 𝐴 𝜑)) → ∃𝑐 ∈ Fin (𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑)) |
| 57 | 15, 17, 25, 50, 56 | syl13anc 1374 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) ∧ (𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑)) → ∃𝑐 ∈ Fin (𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑)) |
| 58 | 8, 57 | exlimddv 1935 |
. 2
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑐 ∈ Fin (𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑)) |
| 59 | 58 | 3adant2 1132 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑐 ∈ Fin (𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑)) |