Step | Hyp | Ref
| Expression |
1 | | simplr 766 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) → 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) |
2 | | vex 3436 |
. . . . . . 7
⊢ 𝑦 ∈ V |
3 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑗 ∈ 𝐴 ↦ 𝐵) = (𝑗 ∈ 𝐴 ↦ 𝐵) |
4 | 3 | elrnmpt 5865 |
. . . . . . 7
⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑗 ∈ 𝐴 𝑦 = 𝐵)) |
5 | 2, 4 | ax-mp 5 |
. . . . . 6
⊢ (𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑗 ∈ 𝐴 𝑦 = 𝐵) |
6 | 1, 5 | sylib 217 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) → ∃𝑗 ∈ 𝐴 𝑦 = 𝐵) |
7 | | nfv 1917 |
. . . . . . . 8
⊢
Ⅎ𝑗(𝜑 ∧ 𝑥 ∈ 𝐶) |
8 | | nfcv 2907 |
. . . . . . . . 9
⊢
Ⅎ𝑗𝑦 |
9 | | nfmpt1 5182 |
. . . . . . . . . 10
⊢
Ⅎ𝑗(𝑗 ∈ 𝐴 ↦ 𝐵) |
10 | 9 | nfrn 5861 |
. . . . . . . . 9
⊢
Ⅎ𝑗ran
(𝑗 ∈ 𝐴 ↦ 𝐵) |
11 | 8, 10 | nfel 2921 |
. . . . . . . 8
⊢
Ⅎ𝑗 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵) |
12 | 7, 11 | nfan 1902 |
. . . . . . 7
⊢
Ⅎ𝑗((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) |
13 | | nfv 1917 |
. . . . . . 7
⊢
Ⅎ𝑗 𝑥 ∈ 𝑦 |
14 | 12, 13 | nfan 1902 |
. . . . . 6
⊢
Ⅎ𝑗(((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) |
15 | | simpllr 773 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) ∧ 𝑗 ∈ 𝐴) ∧ 𝑦 = 𝐵) → 𝑥 ∈ 𝑦) |
16 | | simpr 485 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) ∧ 𝑗 ∈ 𝐴) ∧ 𝑦 = 𝐵) → 𝑦 = 𝐵) |
17 | 15, 16 | eleqtrd 2841 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) ∧ 𝑗 ∈ 𝐴) ∧ 𝑦 = 𝐵) → 𝑥 ∈ 𝐵) |
18 | 17 | ex 413 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) ∧ 𝑗 ∈ 𝐴) → (𝑦 = 𝐵 → 𝑥 ∈ 𝐵)) |
19 | 18 | ex 413 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) → (𝑗 ∈ 𝐴 → (𝑦 = 𝐵 → 𝑥 ∈ 𝐵))) |
20 | 14, 19 | reximdai 3244 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) → (∃𝑗 ∈ 𝐴 𝑦 = 𝐵 → ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵)) |
21 | 6, 20 | mpd 15 |
. . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐶) ∧ 𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)) ∧ 𝑥 ∈ 𝑦) → ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵) |
22 | | acunirnmpt2.2 |
. . . . . . . 8
⊢ 𝐶 = ∪
ran (𝑗 ∈ 𝐴 ↦ 𝐵) |
23 | 22 | eleq2i 2830 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐶 ↔ 𝑥 ∈ ∪ ran
(𝑗 ∈ 𝐴 ↦ 𝐵)) |
24 | 23 | biimpi 215 |
. . . . . 6
⊢ (𝑥 ∈ 𝐶 → 𝑥 ∈ ∪ ran
(𝑗 ∈ 𝐴 ↦ 𝐵)) |
25 | | eluni2 4843 |
. . . . . 6
⊢ (𝑥 ∈ ∪ ran (𝑗 ∈ 𝐴 ↦ 𝐵) ↔ ∃𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)𝑥 ∈ 𝑦) |
26 | 24, 25 | sylib 217 |
. . . . 5
⊢ (𝑥 ∈ 𝐶 → ∃𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)𝑥 ∈ 𝑦) |
27 | 26 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∃𝑦 ∈ ran (𝑗 ∈ 𝐴 ↦ 𝐵)𝑥 ∈ 𝑦) |
28 | 21, 27 | r19.29a 3218 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐶) → ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵) |
29 | 28 | ralrimiva 3103 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵) |
30 | | acunirnmpt.0 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
31 | | mptexg 7097 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (𝑗 ∈ 𝐴 ↦ 𝐵) ∈ V) |
32 | | rnexg 7751 |
. . . . 5
⊢ ((𝑗 ∈ 𝐴 ↦ 𝐵) ∈ V → ran (𝑗 ∈ 𝐴 ↦ 𝐵) ∈ V) |
33 | | uniexg 7593 |
. . . . 5
⊢ (ran
(𝑗 ∈ 𝐴 ↦ 𝐵) ∈ V → ∪ ran (𝑗 ∈ 𝐴 ↦ 𝐵) ∈ V) |
34 | 30, 31, 32, 33 | 4syl 19 |
. . . 4
⊢ (𝜑 → ∪ ran (𝑗 ∈ 𝐴 ↦ 𝐵) ∈ V) |
35 | 22, 34 | eqeltrid 2843 |
. . 3
⊢ (𝜑 → 𝐶 ∈ V) |
36 | | id 22 |
. . . . . 6
⊢ (𝑐 = 𝐶 → 𝑐 = 𝐶) |
37 | 36 | raleqdv 3348 |
. . . . 5
⊢ (𝑐 = 𝐶 → (∀𝑥 ∈ 𝑐 ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∀𝑥 ∈ 𝐶 ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵)) |
38 | 36 | feq2d 6586 |
. . . . . . 7
⊢ (𝑐 = 𝐶 → (𝑓:𝑐⟶𝐴 ↔ 𝑓:𝐶⟶𝐴)) |
39 | 36 | raleqdv 3348 |
. . . . . . 7
⊢ (𝑐 = 𝐶 → (∀𝑥 ∈ 𝑐 𝑥 ∈ 𝐷 ↔ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷)) |
40 | 38, 39 | anbi12d 631 |
. . . . . 6
⊢ (𝑐 = 𝐶 → ((𝑓:𝑐⟶𝐴 ∧ ∀𝑥 ∈ 𝑐 𝑥 ∈ 𝐷) ↔ (𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷))) |
41 | 40 | exbidv 1924 |
. . . . 5
⊢ (𝑐 = 𝐶 → (∃𝑓(𝑓:𝑐⟶𝐴 ∧ ∀𝑥 ∈ 𝑐 𝑥 ∈ 𝐷) ↔ ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷))) |
42 | 37, 41 | imbi12d 345 |
. . . 4
⊢ (𝑐 = 𝐶 → ((∀𝑥 ∈ 𝑐 ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃𝑓(𝑓:𝑐⟶𝐴 ∧ ∀𝑥 ∈ 𝑐 𝑥 ∈ 𝐷)) ↔ (∀𝑥 ∈ 𝐶 ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷)))) |
43 | | vex 3436 |
. . . . 5
⊢ 𝑐 ∈ V |
44 | | acunirnmpt2.3 |
. . . . . 6
⊢ (𝑗 = (𝑓‘𝑥) → 𝐵 = 𝐷) |
45 | 44 | eleq2d 2824 |
. . . . 5
⊢ (𝑗 = (𝑓‘𝑥) → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐷)) |
46 | 43, 45 | ac6s 10240 |
. . . 4
⊢
(∀𝑥 ∈
𝑐 ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃𝑓(𝑓:𝑐⟶𝐴 ∧ ∀𝑥 ∈ 𝑐 𝑥 ∈ 𝐷)) |
47 | 42, 46 | vtoclg 3505 |
. . 3
⊢ (𝐶 ∈ V → (∀𝑥 ∈ 𝐶 ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷))) |
48 | 35, 47 | syl 17 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ 𝐶 ∃𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 → ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷))) |
49 | 29, 48 | mpd 15 |
1
⊢ (𝜑 → ∃𝑓(𝑓:𝐶⟶𝐴 ∧ ∀𝑥 ∈ 𝐶 𝑥 ∈ 𝐷)) |