| Step | Hyp | Ref
| Expression |
| 1 | | simplr 769 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) → 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) |
| 2 | | vex 3484 |
. . . . . . 7
⊢ 𝑦 ∈ V |
| 3 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑗 ∈ 𝐴 ↦ 𝐵) = (𝑗 ∈ 𝐴 ↦ 𝐵) |
| 4 | 3 | elrnmpt 5969 |
. . . . . . 7
⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑗 ∈ 𝐴 𝑦 = 𝐵)) |
| 5 | 2, 4 | ax-mp 5 |
. . . . . 6
⊢ (𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑗 ∈ 𝐴 𝑦 = 𝐵) |
| 6 | 1, 5 | sylib 218 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) → ∃𝑗 ∈ 𝐴 𝑦 = 𝐵) |
| 7 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑗(𝜑 ∧ 𝑥 ∈ 𝐶) |
| 8 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑗𝑦 |
| 9 | | nfmpt1 5250 |
. . . . . . . . . 10
⊢
Ⅎ𝑗(𝑗 ∈ 𝐴 ↦ 𝐵) |
| 10 | 9 | nfrn 5963 |
. . . . . . . . 9
⊢
Ⅎ𝑗ran
(𝑗 ∈ 𝐴 ↦ 𝐵) |
| 11 | 8, 10 | nfel 2920 |
. . . . . . . 8
⊢
Ⅎ𝑗 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵) |
| 12 | 7, 11 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑗((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) |
| 13 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑗 𝑥 ∈ 𝑦 |
| 14 | 12, 13 | nfan 1899 |
. . . . . 6
⊢
Ⅎ𝑗(((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) |
| 15 | | simpllr 776 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) ∧ 𝑗 ∈ 𝐴) ∧ 𝑦 = 𝐵) → 𝑥 ∈ 𝑦) |
| 16 | | simpr 484 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) ∧ 𝑗 ∈ 𝐴) ∧ 𝑦 = 𝐵) → 𝑦 = 𝐵) |
| 17 | 15, 16 | eleqtrd 2843 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) ∧ 𝑗 ∈ 𝐴) ∧ 𝑦 = 𝐵) → 𝑥 ∈ 𝐵) |
| 18 | 17 | ex 412 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) ∧ 𝑗 ∈ 𝐴) → (𝑦 = 𝐵 → 𝑥 ∈ 𝐵)) |
| 19 | 18 | ex 412 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) → (𝑗 ∈ 𝐴 → (𝑦 = 𝐵 → 𝑥 ∈ 𝐵))) |
| 20 | 14, 19 | reximdai 3261 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) → (∃𝑗 ∈ 𝐴 𝑦 = 𝐵 → ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵)) |
| 21 | 6, 20 | mpd 15 |
. . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) → ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵) |
| 22 | | acunirnmpt2.2 |
. . . . . . . 8
⊢ 𝐶 = ∪
ran (𝑗 ∈ 𝐴 ↦ 𝐵) |
| 23 | 22 | eleq2i 2833 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐶 ↔ 𝑥 ∈ ∪ ran
(𝑗 ∈ 𝐴 ↦ 𝐵)) |
| 24 | 23 | biimpi 216 |
. . . . . 6
⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ ∪ ran
(𝑗 ∈ 𝐴 ↦ 𝐵)) |
| 25 | | eluni2 4911 |
. . . . . 6
⊢ (𝑥 ∈ ∪ ran (𝑗 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)𝑥 ∈ 𝑦) |
| 26 | 24, 25 | sylib 218 |
. . . . 5
⊢ (𝑥 ∈ 𝐶 → ∃𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)𝑥 ∈ 𝑦) |
| 27 | 26 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∃𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)𝑥 ∈ 𝑦) |
| 28 | 21, 27 | r19.29a 3162 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵) |
| 29 | 28 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵) |
| 30 | | acunirnmpt.0 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 31 | | mptexg 7241 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (𝑗 ∈ 𝐴 ↦ 𝐵) ∈ V) |
| 32 | | rnexg 7924 |
. . . . 5
⊢ ((𝑗 ∈ 𝐴 ↦ 𝐵) ∈ V → ran (𝑗 ∈ 𝐴 ↦ 𝐵) ∈ V) |
| 33 | | uniexg 7760 |
. . . . 5
⊢ (ran
(𝑗 ∈ 𝐴 ↦ 𝐵) ∈ V → ∪ ran (𝑗 ∈ 𝐴 ↦ 𝐵) ∈ V) |
| 34 | 30, 31, 32, 33 | 4syl 19 |
. . . 4
⊢ (𝜑 → ∪ ran (𝑗 ∈ 𝐴 ↦ 𝐵) ∈ V) |
| 35 | 22, 34 | eqeltrid 2845 |
. . 3
⊢ (𝜑 → 𝐶 ∈ V) |
| 36 | | id 22 |
. . . . . 6
⊢ (𝑐 = 𝐶 → 𝑐 = 𝐶) |
| 37 | 36 | raleqdv 3326 |
. . . . 5
⊢ (𝑐 = 𝐶 → (∀𝑥 ∈ 𝑐 ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∀𝑥 ∈ 𝐶 ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵)) |
| 38 | 36 | feq2d 6722 |
. . . . . . 7
⊢ (𝑐 = 𝐶 → (𝑓:𝑐⟶𝐴 ↔ 𝑓:𝐶⟶𝐴)) |
| 39 | 36 | raleqdv 3326 |
. . . . . . 7
⊢ (𝑐 = 𝐶 → (∀𝑥 ∈ 𝑐 𝑥 ∈ 𝐷 ↔ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷)) |
| 40 | 38, 39 | anbi12d 632 |
. . . . . 6
⊢ (𝑐 = 𝐶 → ((𝑓:𝑐⟶𝐴 ∧ ∀𝑥 ∈ 𝑐 𝑥 ∈ 𝐷) ↔ (𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷))) |
| 41 | 40 | exbidv 1921 |
. . . . 5
⊢ (𝑐 = 𝐶 → (∃𝑓(𝑓:𝑐⟶𝐴 ∧ ∀𝑥 ∈ 𝑐 𝑥 ∈ 𝐷) ↔ ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷))) |
| 42 | 37, 41 | imbi12d 344 |
. . . 4
⊢ (𝑐 = 𝐶 → ((∀𝑥 ∈ 𝑐 ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃𝑓(𝑓:𝑐⟶𝐴 ∧ ∀𝑥 ∈ 𝑐 𝑥 ∈ 𝐷)) ↔ (∀𝑥 ∈ 𝐶 ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷)))) |
| 43 | | vex 3484 |
. . . . 5
⊢ 𝑐 ∈ V |
| 44 | | acunirnmpt2.3 |
. . . . . 6
⊢ (𝑗 = (𝑓‘𝑥) → 𝐵 = 𝐷) |
| 45 | 44 | eleq2d 2827 |
. . . . 5
⊢ (𝑗 = (𝑓‘𝑥) → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐷)) |
| 46 | 43, 45 | ac6s 10524 |
. . . 4
⊢
(∀𝑥 ∈
𝑐 ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃𝑓(𝑓:𝑐⟶𝐴 ∧ ∀𝑥 ∈ 𝑐 𝑥 ∈ 𝐷)) |
| 47 | 42, 46 | vtoclg 3554 |
. . 3
⊢ (𝐶 ∈ V → (∀𝑥 ∈ 𝐶 ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷))) |
| 48 | 35, 47 | syl 17 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ 𝐶 ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷))) |
| 49 | 29, 48 | mpd 15 |
1
⊢ (𝜑 → ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷)) |