| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐶) ∧ 𝑗 ∈ 𝐴) ∧ 𝑦 = 𝐵) → 𝑦 = 𝐵) |
| 2 | | simplll 775 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐶) ∧ 𝑗 ∈ 𝐴) ∧ 𝑦 = 𝐵) → 𝜑) |
| 3 | | simplr 769 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐶) ∧ 𝑗 ∈ 𝐴) ∧ 𝑦 = 𝐵) → 𝑗 ∈ 𝐴) |
| 4 | | acunirnmpt.1 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ≠ ∅) |
| 5 | 2, 3, 4 | syl2anc 584 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐶) ∧ 𝑗 ∈ 𝐴) ∧ 𝑦 = 𝐵) → 𝐵 ≠ ∅) |
| 6 | 1, 5 | eqnetrd 3008 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐶) ∧ 𝑗 ∈ 𝐴) ∧ 𝑦 = 𝐵) → 𝑦 ≠ ∅) |
| 7 | | acunirnmpt.2 |
. . . . . . . . 9
⊢ 𝐶 = ran (𝑗 ∈ 𝐴 ↦ 𝐵) |
| 8 | 7 | eleq2i 2833 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) |
| 9 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
| 10 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑗 ∈ 𝐴 ↦ 𝐵) = (𝑗 ∈ 𝐴 ↦ 𝐵) |
| 11 | 10 | elrnmpt 5969 |
. . . . . . . . 9
⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑗 ∈ 𝐴 𝑦 = 𝐵)) |
| 12 | 9, 11 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑗 ∈ 𝐴 𝑦 = 𝐵) |
| 13 | 8, 12 | bitri 275 |
. . . . . . 7
⊢ (𝑦 ∈ 𝐶 ↔ ∃𝑗 ∈ 𝐴 𝑦 = 𝐵) |
| 14 | 13 | biimpi 216 |
. . . . . 6
⊢ (𝑦 ∈ 𝐶 → ∃𝑗 ∈ 𝐴 𝑦 = 𝐵) |
| 15 | 14 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ∃𝑗 ∈ 𝐴 𝑦 = 𝐵) |
| 16 | 6, 15 | r19.29a 3162 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → 𝑦 ≠ ∅) |
| 17 | 16 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝐶 𝑦 ≠ ∅) |
| 18 | | acunirnmpt.0 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 19 | | mptexg 7241 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (𝑗 ∈ 𝐴 ↦ 𝐵) ∈ V) |
| 20 | | rnexg 7924 |
. . . . . 6
⊢ ((𝑗 ∈ 𝐴 ↦ 𝐵) ∈ V → ran (𝑗 ∈ 𝐴 ↦ 𝐵) ∈ V) |
| 21 | 18, 19, 20 | 3syl 18 |
. . . . 5
⊢ (𝜑 → ran (𝑗 ∈ 𝐴 ↦ 𝐵) ∈ V) |
| 22 | 7, 21 | eqeltrid 2845 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ V) |
| 23 | | raleq 3323 |
. . . . . 6
⊢ (𝑐 = 𝐶 → (∀𝑦 ∈ 𝑐 𝑦 ≠ ∅ ↔ ∀𝑦 ∈ 𝐶 𝑦 ≠ ∅)) |
| 24 | | id 22 |
. . . . . . . . 9
⊢ (𝑐 = 𝐶 → 𝑐 = 𝐶) |
| 25 | | unieq 4918 |
. . . . . . . . 9
⊢ (𝑐 = 𝐶 → ∪ 𝑐 = ∪
𝐶) |
| 26 | 24, 25 | feq23d 6731 |
. . . . . . . 8
⊢ (𝑐 = 𝐶 → (𝑓:𝑐⟶∪ 𝑐 ↔ 𝑓:𝐶⟶∪ 𝐶)) |
| 27 | | raleq 3323 |
. . . . . . . 8
⊢ (𝑐 = 𝐶 → (∀𝑦 ∈ 𝑐 (𝑓‘𝑦) ∈ 𝑦 ↔ ∀𝑦 ∈ 𝐶 (𝑓‘𝑦) ∈ 𝑦)) |
| 28 | 26, 27 | anbi12d 632 |
. . . . . . 7
⊢ (𝑐 = 𝐶 → ((𝑓:𝑐⟶∪ 𝑐 ∧ ∀𝑦 ∈ 𝑐 (𝑓‘𝑦) ∈ 𝑦) ↔ (𝑓:𝐶⟶∪ 𝐶 ∧ ∀𝑦 ∈ 𝐶 (𝑓‘𝑦) ∈ 𝑦))) |
| 29 | 28 | exbidv 1921 |
. . . . . 6
⊢ (𝑐 = 𝐶 → (∃𝑓(𝑓:𝑐⟶∪ 𝑐 ∧ ∀𝑦 ∈ 𝑐 (𝑓‘𝑦) ∈ 𝑦) ↔ ∃𝑓(𝑓:𝐶⟶∪ 𝐶 ∧ ∀𝑦 ∈ 𝐶 (𝑓‘𝑦) ∈ 𝑦))) |
| 30 | 23, 29 | imbi12d 344 |
. . . . 5
⊢ (𝑐 = 𝐶 → ((∀𝑦 ∈ 𝑐 𝑦 ≠ ∅ → ∃𝑓(𝑓:𝑐⟶∪ 𝑐 ∧ ∀𝑦 ∈ 𝑐 (𝑓‘𝑦) ∈ 𝑦)) ↔ (∀𝑦 ∈ 𝐶 𝑦 ≠ ∅ → ∃𝑓(𝑓:𝐶⟶∪ 𝐶 ∧ ∀𝑦 ∈ 𝐶 (𝑓‘𝑦) ∈ 𝑦)))) |
| 31 | | vex 3484 |
. . . . . 6
⊢ 𝑐 ∈ V |
| 32 | 31 | ac5b 10518 |
. . . . 5
⊢
(∀𝑦 ∈
𝑐 𝑦 ≠ ∅ → ∃𝑓(𝑓:𝑐⟶∪ 𝑐 ∧ ∀𝑦 ∈ 𝑐 (𝑓‘𝑦) ∈ 𝑦)) |
| 33 | 30, 32 | vtoclg 3554 |
. . . 4
⊢ (𝐶 ∈ V → (∀𝑦 ∈ 𝐶 𝑦 ≠ ∅ → ∃𝑓(𝑓:𝐶⟶∪ 𝐶 ∧ ∀𝑦 ∈ 𝐶 (𝑓‘𝑦) ∈ 𝑦))) |
| 34 | 22, 33 | syl 17 |
. . 3
⊢ (𝜑 → (∀𝑦 ∈ 𝐶 𝑦 ≠ ∅ → ∃𝑓(𝑓:𝐶⟶∪ 𝐶 ∧ ∀𝑦 ∈ 𝐶 (𝑓‘𝑦) ∈ 𝑦))) |
| 35 | 17, 34 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑓(𝑓:𝐶⟶∪ 𝐶 ∧ ∀𝑦 ∈ 𝐶 (𝑓‘𝑦) ∈ 𝑦)) |
| 36 | 15 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐶) ∧ (𝑓‘𝑦) ∈ 𝑦) → ∃𝑗 ∈ 𝐴 𝑦 = 𝐵) |
| 37 | | simpllr 776 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑦 ∈ 𝐶) ∧ (𝑓‘𝑦) ∈ 𝑦) ∧ 𝑗 ∈ 𝐴) ∧ 𝑦 = 𝐵) → (𝑓‘𝑦) ∈ 𝑦) |
| 38 | | simpr 484 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑦 ∈ 𝐶) ∧ (𝑓‘𝑦) ∈ 𝑦) ∧ 𝑗 ∈ 𝐴) ∧ 𝑦 = 𝐵) → 𝑦 = 𝐵) |
| 39 | 37, 38 | eleqtrd 2843 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑦 ∈ 𝐶) ∧ (𝑓‘𝑦) ∈ 𝑦) ∧ 𝑗 ∈ 𝐴) ∧ 𝑦 = 𝐵) → (𝑓‘𝑦) ∈ 𝐵) |
| 40 | 39 | ex 412 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐶) ∧ (𝑓‘𝑦) ∈ 𝑦) ∧ 𝑗 ∈ 𝐴) → (𝑦 = 𝐵 → (𝑓‘𝑦) ∈ 𝐵)) |
| 41 | 40 | reximdva 3168 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐶) ∧ (𝑓‘𝑦) ∈ 𝑦) → (∃𝑗 ∈ 𝐴 𝑦 = 𝐵 → ∃𝑗 ∈ 𝐴 (𝑓‘𝑦) ∈ 𝐵)) |
| 42 | 36, 41 | mpd 15 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐶) ∧ (𝑓‘𝑦) ∈ 𝑦) → ∃𝑗 ∈ 𝐴 (𝑓‘𝑦) ∈ 𝐵) |
| 43 | 42 | ex 412 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐶) → ((𝑓‘𝑦) ∈ 𝑦 → ∃𝑗 ∈ 𝐴 (𝑓‘𝑦) ∈ 𝐵)) |
| 44 | 43 | ralimdva 3167 |
. . . 4
⊢ (𝜑 → (∀𝑦 ∈ 𝐶 (𝑓‘𝑦) ∈ 𝑦 → ∀𝑦 ∈ 𝐶 ∃𝑗 ∈ 𝐴 (𝑓‘𝑦) ∈ 𝐵)) |
| 45 | 44 | anim2d 612 |
. . 3
⊢ (𝜑 → ((𝑓:𝐶⟶∪ 𝐶 ∧ ∀𝑦 ∈ 𝐶 (𝑓‘𝑦) ∈ 𝑦) → (𝑓:𝐶⟶∪ 𝐶 ∧ ∀𝑦 ∈ 𝐶 ∃𝑗 ∈ 𝐴 (𝑓‘𝑦) ∈ 𝐵))) |
| 46 | 45 | eximdv 1917 |
. 2
⊢ (𝜑 → (∃𝑓(𝑓:𝐶⟶∪ 𝐶 ∧ ∀𝑦 ∈ 𝐶 (𝑓‘𝑦) ∈ 𝑦) → ∃𝑓(𝑓:𝐶⟶∪ 𝐶 ∧ ∀𝑦 ∈ 𝐶 ∃𝑗 ∈ 𝐴 (𝑓‘𝑦) ∈ 𝐵))) |
| 47 | 35, 46 | mpd 15 |
1
⊢ (𝜑 → ∃𝑓(𝑓:𝐶⟶∪ 𝐶 ∧ ∀𝑦 ∈ 𝐶 ∃𝑗 ∈ 𝐴 (𝑓‘𝑦) ∈ 𝐵)) |