Step | Hyp | Ref
| Expression |
1 | | simplr 769 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) → 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) |
2 | | vex 3402 |
. . . . . . 7
⊢ 𝑦 ∈ V |
3 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑗 ∈ 𝐴 ↦ 𝐵) = (𝑗 ∈ 𝐴 ↦ 𝐵) |
4 | 3 | elrnmpt 5799 |
. . . . . . 7
⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑗 ∈ 𝐴 𝑦 = 𝐵)) |
5 | 2, 4 | ax-mp 5 |
. . . . . 6
⊢ (𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑗 ∈ 𝐴 𝑦 = 𝐵) |
6 | 1, 5 | sylib 221 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) → ∃𝑗 ∈ 𝐴 𝑦 = 𝐵) |
7 | | nfv 1921 |
. . . . . . . 8
⊢
Ⅎ𝑗(𝜑 ∧ 𝑥 ∈ 𝐶) |
8 | | nfcv 2899 |
. . . . . . . . 9
⊢
Ⅎ𝑗𝑦 |
9 | | nfmpt1 5128 |
. . . . . . . . . 10
⊢
Ⅎ𝑗(𝑗 ∈ 𝐴 ↦ 𝐵) |
10 | 9 | nfrn 5795 |
. . . . . . . . 9
⊢
Ⅎ𝑗ran
(𝑗 ∈ 𝐴 ↦ 𝐵) |
11 | 8, 10 | nfel 2913 |
. . . . . . . 8
⊢
Ⅎ𝑗 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵) |
12 | 7, 11 | nfan 1906 |
. . . . . . 7
⊢
Ⅎ𝑗((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) |
13 | | nfv 1921 |
. . . . . . 7
⊢
Ⅎ𝑗 𝑥 ∈ 𝑦 |
14 | 12, 13 | nfan 1906 |
. . . . . 6
⊢
Ⅎ𝑗(((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) |
15 | | simpllr 776 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) ∧ 𝑗 ∈ 𝐴) ∧ 𝑦 = 𝐵) → 𝑥 ∈ 𝑦) |
16 | | simpr 488 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) ∧ 𝑗 ∈ 𝐴) ∧ 𝑦 = 𝐵) → 𝑦 = 𝐵) |
17 | 15, 16 | eleqtrd 2835 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) ∧ 𝑗 ∈ 𝐴) ∧ 𝑦 = 𝐵) → 𝑥 ∈ 𝐵) |
18 | 17 | ex 416 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) ∧ 𝑗 ∈ 𝐴) → (𝑦 = 𝐵 → 𝑥 ∈ 𝐵)) |
19 | 18 | ex 416 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) → (𝑗 ∈ 𝐴 → (𝑦 = 𝐵 → 𝑥 ∈ 𝐵))) |
20 | 14, 19 | reximdai 3221 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) → (∃𝑗 ∈ 𝐴 𝑦 = 𝐵 → ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵)) |
21 | 6, 20 | mpd 15 |
. . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) → ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵) |
22 | | acunirnmpt2.2 |
. . . . . . . 8
⊢ 𝐶 = ∪
ran (𝑗 ∈ 𝐴 ↦ 𝐵) |
23 | 22 | eleq2i 2824 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐶 ↔ 𝑥 ∈ ∪ ran
(𝑗 ∈ 𝐴 ↦ 𝐵)) |
24 | 23 | biimpi 219 |
. . . . . 6
⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ ∪ ran
(𝑗 ∈ 𝐴 ↦ 𝐵)) |
25 | | eluni2 4800 |
. . . . . 6
⊢ (𝑥 ∈ ∪ ran (𝑗 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)𝑥 ∈ 𝑦) |
26 | 24, 25 | sylib 221 |
. . . . 5
⊢ (𝑥 ∈ 𝐶 → ∃𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)𝑥 ∈ 𝑦) |
27 | 26 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∃𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)𝑥 ∈ 𝑦) |
28 | 21, 27 | r19.29a 3199 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵) |
29 | 28 | ralrimiva 3096 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵) |
30 | | acunirnmpt.0 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
31 | | mptexg 6994 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (𝑗 ∈ 𝐴 ↦ 𝐵) ∈ V) |
32 | | rnexg 7635 |
. . . . 5
⊢ ((𝑗 ∈ 𝐴 ↦ 𝐵) ∈ V → ran (𝑗 ∈ 𝐴 ↦ 𝐵) ∈ V) |
33 | | uniexg 7484 |
. . . . 5
⊢ (ran
(𝑗 ∈ 𝐴 ↦ 𝐵) ∈ V → ∪ ran (𝑗 ∈ 𝐴 ↦ 𝐵) ∈ V) |
34 | 30, 31, 32, 33 | 4syl 19 |
. . . 4
⊢ (𝜑 → ∪ ran (𝑗 ∈ 𝐴 ↦ 𝐵) ∈ V) |
35 | 22, 34 | eqeltrid 2837 |
. . 3
⊢ (𝜑 → 𝐶 ∈ V) |
36 | | id 22 |
. . . . . 6
⊢ (𝑐 = 𝐶 → 𝑐 = 𝐶) |
37 | 36 | raleqdv 3316 |
. . . . 5
⊢ (𝑐 = 𝐶 → (∀𝑥 ∈ 𝑐 ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∀𝑥 ∈ 𝐶 ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵)) |
38 | 36 | feq2d 6490 |
. . . . . . 7
⊢ (𝑐 = 𝐶 → (𝑓:𝑐⟶𝐴 ↔ 𝑓:𝐶⟶𝐴)) |
39 | 36 | raleqdv 3316 |
. . . . . . 7
⊢ (𝑐 = 𝐶 → (∀𝑥 ∈ 𝑐 𝑥 ∈ 𝐷 ↔ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷)) |
40 | 38, 39 | anbi12d 634 |
. . . . . 6
⊢ (𝑐 = 𝐶 → ((𝑓:𝑐⟶𝐴 ∧ ∀𝑥 ∈ 𝑐 𝑥 ∈ 𝐷) ↔ (𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷))) |
41 | 40 | exbidv 1928 |
. . . . 5
⊢ (𝑐 = 𝐶 → (∃𝑓(𝑓:𝑐⟶𝐴 ∧ ∀𝑥 ∈ 𝑐 𝑥 ∈ 𝐷) ↔ ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷))) |
42 | 37, 41 | imbi12d 348 |
. . . 4
⊢ (𝑐 = 𝐶 → ((∀𝑥 ∈ 𝑐 ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃𝑓(𝑓:𝑐⟶𝐴 ∧ ∀𝑥 ∈ 𝑐 𝑥 ∈ 𝐷)) ↔ (∀𝑥 ∈ 𝐶 ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷)))) |
43 | | vex 3402 |
. . . . 5
⊢ 𝑐 ∈ V |
44 | | acunirnmpt2.3 |
. . . . . 6
⊢ (𝑗 = (𝑓‘𝑥) → 𝐵 = 𝐷) |
45 | 44 | eleq2d 2818 |
. . . . 5
⊢ (𝑗 = (𝑓‘𝑥) → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐷)) |
46 | 43, 45 | ac6s 9984 |
. . . 4
⊢
(∀𝑥 ∈
𝑐 ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃𝑓(𝑓:𝑐⟶𝐴 ∧ ∀𝑥 ∈ 𝑐 𝑥 ∈ 𝐷)) |
47 | 42, 46 | vtoclg 3470 |
. . 3
⊢ (𝐶 ∈ V → (∀𝑥 ∈ 𝐶 ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷))) |
48 | 35, 47 | syl 17 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ 𝐶 ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷))) |
49 | 29, 48 | mpd 15 |
1
⊢ (𝜑 → ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷)) |