| Step | Hyp | Ref
| Expression |
| 1 | | nfv 1914 |
. . . 4
⊢
Ⅎ𝑧 𝐵 ≠ ∅ |
| 2 | | nfcsb1v 3923 |
. . . . 5
⊢
Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵 |
| 3 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑥∅ |
| 4 | 2, 3 | nfne 3043 |
. . . 4
⊢
Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵 ≠ ∅ |
| 5 | | csbeq1a 3913 |
. . . . 5
⊢ (𝑥 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
| 6 | 5 | neeq1d 3000 |
. . . 4
⊢ (𝑥 = 𝑧 → (𝐵 ≠ ∅ ↔ ⦋𝑧 / 𝑥⦌𝐵 ≠ ∅)) |
| 7 | 1, 4, 6 | cbvralw 3306 |
. . 3
⊢
(∀𝑥 ∈
𝐴 𝐵 ≠ ∅ ↔ ∀𝑧 ∈ 𝐴 ⦋𝑧 / 𝑥⦌𝐵 ≠ ∅) |
| 8 | | n0 4353 |
. . . . 5
⊢
(⦋𝑧 /
𝑥⦌𝐵 ≠ ∅ ↔
∃𝑦 𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵) |
| 9 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑦 𝑧 ∈ 𝐴 |
| 10 | | nfre1 3285 |
. . . . . 6
⊢
Ⅎ𝑦∃𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵 |
| 11 | 2 | nfel2 2924 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵 |
| 12 | 5 | eleq2d 2827 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵)) |
| 13 | 11, 12 | rspce 3611 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
| 14 | | eliun 4995 |
. . . . . . . . 9
⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
| 15 | 13, 14 | sylibr 234 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵) → 𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
| 16 | | rspe 3249 |
. . . . . . . 8
⊢ ((𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵) → ∃𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵) |
| 17 | 15, 16 | sylancom 588 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵) → ∃𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵) |
| 18 | 17 | ex 412 |
. . . . . 6
⊢ (𝑧 ∈ 𝐴 → (𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵 → ∃𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵)) |
| 19 | 9, 10, 18 | exlimd 2218 |
. . . . 5
⊢ (𝑧 ∈ 𝐴 → (∃𝑦 𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵 → ∃𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵)) |
| 20 | 8, 19 | biimtrid 242 |
. . . 4
⊢ (𝑧 ∈ 𝐴 → (⦋𝑧 / 𝑥⦌𝐵 ≠ ∅ → ∃𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵)) |
| 21 | 20 | ralimia 3080 |
. . 3
⊢
(∀𝑧 ∈
𝐴 ⦋𝑧 / 𝑥⦌𝐵 ≠ ∅ → ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵) |
| 22 | 7, 21 | sylbi 217 |
. 2
⊢
(∀𝑥 ∈
𝐴 𝐵 ≠ ∅ → ∀𝑧 ∈ 𝐴 ∃𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵) |
| 23 | | ac6c4.1 |
. . 3
⊢ 𝐴 ∈ V |
| 24 | | ac6c4.2 |
. . . 4
⊢ 𝐵 ∈ V |
| 25 | 23, 24 | iunex 7993 |
. . 3
⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V |
| 26 | | eleq1 2829 |
. . 3
⊢ (𝑦 = (𝑓‘𝑧) → (𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵 ↔ (𝑓‘𝑧) ∈ ⦋𝑧 / 𝑥⦌𝐵)) |
| 27 | 23, 25, 26 | ac6 10520 |
. 2
⊢
(∀𝑧 ∈
𝐴 ∃𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵 → ∃𝑓(𝑓:𝐴⟶∪
𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) ∈ ⦋𝑧 / 𝑥⦌𝐵)) |
| 28 | | ffn 6736 |
. . . 4
⊢ (𝑓:𝐴⟶∪
𝑥 ∈ 𝐴 𝐵 → 𝑓 Fn 𝐴) |
| 29 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑧(𝑓‘𝑥) ∈ 𝐵 |
| 30 | 2 | nfel2 2924 |
. . . . . 6
⊢
Ⅎ𝑥(𝑓‘𝑧) ∈ ⦋𝑧 / 𝑥⦌𝐵 |
| 31 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝑓‘𝑥) = (𝑓‘𝑧)) |
| 32 | 31, 5 | eleq12d 2835 |
. . . . . 6
⊢ (𝑥 = 𝑧 → ((𝑓‘𝑥) ∈ 𝐵 ↔ (𝑓‘𝑧) ∈ ⦋𝑧 / 𝑥⦌𝐵)) |
| 33 | 29, 30, 32 | cbvralw 3306 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 (𝑓‘𝑥) ∈ 𝐵 ↔ ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) ∈ ⦋𝑧 / 𝑥⦌𝐵) |
| 34 | 33 | biimpri 228 |
. . . 4
⊢
(∀𝑧 ∈
𝐴 (𝑓‘𝑧) ∈ ⦋𝑧 / 𝑥⦌𝐵 → ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵) |
| 35 | 28, 34 | anim12i 613 |
. . 3
⊢ ((𝑓:𝐴⟶∪
𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) ∈ ⦋𝑧 / 𝑥⦌𝐵) → (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)) |
| 36 | 35 | eximi 1835 |
. 2
⊢
(∃𝑓(𝑓:𝐴⟶∪
𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) ∈ ⦋𝑧 / 𝑥⦌𝐵) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)) |
| 37 | 22, 27, 36 | 3syl 18 |
1
⊢
(∀𝑥 ∈
𝐴 𝐵 ≠ ∅ → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)) |