| Step | Hyp | Ref
| Expression |
| 1 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑓 ∈ V |
| 2 | 1 | elixp 8944 |
. . . . . . . . 9
⊢ (𝑓 ∈ X𝑥 ∈
𝐴 𝐵 ↔ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)) |
| 3 | 2 | simprbi 496 |
. . . . . . . 8
⊢ (𝑓 ∈ X𝑥 ∈
𝐴 𝐵 → ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵) |
| 4 | | ssiun2 5047 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪
𝑥 ∈ 𝐴 𝐵) |
| 5 | 4 | sseld 3982 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → ((𝑓‘𝑥) ∈ 𝐵 → (𝑓‘𝑥) ∈ ∪
𝑥 ∈ 𝐴 𝐵)) |
| 6 | 5 | ralimia 3080 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐴 (𝑓‘𝑥) ∈ 𝐵 → ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
| 7 | 3, 6 | syl 17 |
. . . . . . 7
⊢ (𝑓 ∈ X𝑥 ∈
𝐴 𝐵 → ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
| 8 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑦(𝑓‘𝑥) ∈ ∪
𝑥 ∈ 𝐴 𝐵 |
| 9 | | nfiu1 5027 |
. . . . . . . . 9
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵 |
| 10 | 9 | nfel2 2924 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑓‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 𝐵 |
| 11 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑓‘𝑥) = (𝑓‘𝑦)) |
| 12 | 11 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝑓‘𝑥) ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↔ (𝑓‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 𝐵)) |
| 13 | 8, 10, 12 | cbvralw 3306 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 (𝑓‘𝑥) ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
| 14 | 7, 13 | sylib 218 |
. . . . . 6
⊢ (𝑓 ∈ X𝑥 ∈
𝐴 𝐵 → ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
| 15 | 14 | adantl 481 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) ∧ 𝑓 ∈ X𝑥 ∈ 𝐴 𝐵) → ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
| 16 | 15 | ralrimiva 3146 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → ∀𝑓 ∈ X
𝑥 ∈ 𝐴 𝐵∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
| 17 | | eqid 2737 |
. . . . 5
⊢ (𝑓 ∈ X𝑥 ∈
𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)) = (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)) |
| 18 | 17 | fmpo 8093 |
. . . 4
⊢
(∀𝑓 ∈
X 𝑥
∈ 𝐴 𝐵∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↔ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)):(X𝑥 ∈ 𝐴 𝐵 × 𝐴)⟶∪
𝑥 ∈ 𝐴 𝐵) |
| 19 | 16, 18 | sylib 218 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)):(X𝑥 ∈ 𝐴 𝐵 × 𝐴)⟶∪
𝑥 ∈ 𝐴 𝐵) |
| 20 | | ixpssmap2g 8967 |
. . . . . 6
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 → X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴)) |
| 21 | 20 | 3ad2ant2 1135 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → X𝑥 ∈
𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴)) |
| 22 | | ovex 7464 |
. . . . . 6
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴) ∈ V |
| 23 | 22 | ssex 5321 |
. . . . 5
⊢ (X𝑥 ∈
𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴) → X𝑥 ∈ 𝐴 𝐵 ∈ V) |
| 24 | 21, 23 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → X𝑥 ∈
𝐴 𝐵 ∈ V) |
| 25 | | simp1 1137 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → 𝐴 ∈ 𝑉) |
| 26 | 24, 25 | xpexd 7771 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → (X𝑥 ∈
𝐴 𝐵 × 𝐴) ∈ V) |
| 27 | 19, 26 | fexd 7247 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)) ∈ V) |
| 28 | 19 | ffnd 6737 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)) Fn (X𝑥 ∈ 𝐴 𝐵 × 𝐴)) |
| 29 | | dffn4 6826 |
. . . 4
⊢ ((𝑓 ∈ X𝑥 ∈
𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)) Fn (X𝑥 ∈ 𝐴 𝐵 × 𝐴) ↔ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)):(X𝑥 ∈ 𝐴 𝐵 × 𝐴)–onto→ran (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦))) |
| 30 | 28, 29 | sylib 218 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)):(X𝑥 ∈ 𝐴 𝐵 × 𝐴)–onto→ran (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦))) |
| 31 | | n0 4353 |
. . . . . . . . . 10
⊢ (X𝑥 ∈
𝐴 𝐵 ≠ ∅ ↔ ∃𝑔 𝑔 ∈ X𝑥 ∈ 𝐴 𝐵) |
| 32 | | eliun 4995 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵) |
| 33 | | nfixp1 8958 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥X𝑥 ∈
𝐴 𝐵 |
| 34 | 33 | nfel2 2924 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥 𝑔 ∈ X𝑥 ∈
𝐴 𝐵 |
| 35 | | nfv 1914 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦) |
| 36 | 33, 35 | nfrexw 3313 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥∃𝑓 ∈ X
𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦) |
| 37 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑘 ∈ 𝐴) → 𝑧 ∈ 𝐵) |
| 38 | | iftrue 4531 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑥 → if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)) = 𝑧) |
| 39 | | csbeq1a 3913 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑘 → 𝐵 = ⦋𝑘 / 𝑥⦌𝐵) |
| 40 | 39 | equcoms 2019 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 𝑥 → 𝐵 = ⦋𝑘 / 𝑥⦌𝐵) |
| 41 | 40 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑥 → ⦋𝑘 / 𝑥⦌𝐵 = 𝐵) |
| 42 | 38, 41 | eleq12d 2835 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑥 → (if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)) ∈ ⦋𝑘 / 𝑥⦌𝐵 ↔ 𝑧 ∈ 𝐵)) |
| 43 | 37, 42 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑘 ∈ 𝐴) → (𝑘 = 𝑥 → if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)) ∈ ⦋𝑘 / 𝑥⦌𝐵)) |
| 44 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑔 ∈ V |
| 45 | 44 | elixp 8944 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ↔ (𝑔 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ 𝐵)) |
| 46 | 45 | simprbi 496 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑔 ∈ X𝑥 ∈
𝐴 𝐵 → ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ 𝐵) |
| 47 | 46 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ 𝐵) |
| 48 | | nfv 1914 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑘(𝑔‘𝑥) ∈ 𝐵 |
| 49 | | nfcsb1v 3923 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑥⦋𝑘 / 𝑥⦌𝐵 |
| 50 | 49 | nfel2 2924 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑥(𝑔‘𝑘) ∈ ⦋𝑘 / 𝑥⦌𝐵 |
| 51 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑘 → (𝑔‘𝑥) = (𝑔‘𝑘)) |
| 52 | 51, 39 | eleq12d 2835 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑘 → ((𝑔‘𝑥) ∈ 𝐵 ↔ (𝑔‘𝑘) ∈ ⦋𝑘 / 𝑥⦌𝐵)) |
| 53 | 48, 50, 52 | cbvralw 3306 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑥 ∈
𝐴 (𝑔‘𝑥) ∈ 𝐵 ↔ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ ⦋𝑘 / 𝑥⦌𝐵) |
| 54 | 47, 53 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ ⦋𝑘 / 𝑥⦌𝐵) |
| 55 | 54 | r19.21bi 3251 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑘 ∈ 𝐴) → (𝑔‘𝑘) ∈ ⦋𝑘 / 𝑥⦌𝐵) |
| 56 | | iffalse 4534 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
𝑘 = 𝑥 → if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)) = (𝑔‘𝑘)) |
| 57 | 56 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝑘 = 𝑥 → (if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)) ∈ ⦋𝑘 / 𝑥⦌𝐵 ↔ (𝑔‘𝑘) ∈ ⦋𝑘 / 𝑥⦌𝐵)) |
| 58 | 55, 57 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑘 ∈ 𝐴) → (¬ 𝑘 = 𝑥 → if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)) ∈ ⦋𝑘 / 𝑥⦌𝐵)) |
| 59 | 43, 58 | pm2.61d 179 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑘 ∈ 𝐴) → if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)) ∈ ⦋𝑘 / 𝑥⦌𝐵) |
| 60 | 59 | ralrimiva 3146 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → ∀𝑘 ∈ 𝐴 if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)) ∈ ⦋𝑘 / 𝑥⦌𝐵) |
| 61 | | ixpfn 8943 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 ∈ X𝑥 ∈
𝐴 𝐵 → 𝑔 Fn 𝐴) |
| 62 | 61 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → 𝑔 Fn 𝐴) |
| 63 | 62 | fndmd 6673 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → dom 𝑔 = 𝐴) |
| 64 | 44 | dmex 7931 |
. . . . . . . . . . . . . . . . . . 19
⊢ dom 𝑔 ∈ V |
| 65 | 63, 64 | eqeltrrdi 2850 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → 𝐴 ∈ V) |
| 66 | | mptelixpg 8975 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ V → ((𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘))) ∈ X𝑘 ∈ 𝐴 ⦋𝑘 / 𝑥⦌𝐵 ↔ ∀𝑘 ∈ 𝐴 if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)) ∈ ⦋𝑘 / 𝑥⦌𝐵)) |
| 67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → ((𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘))) ∈ X𝑘 ∈ 𝐴 ⦋𝑘 / 𝑥⦌𝐵 ↔ ∀𝑘 ∈ 𝐴 if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)) ∈ ⦋𝑘 / 𝑥⦌𝐵)) |
| 68 | 60, 67 | mpbird 257 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → (𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘))) ∈ X𝑘 ∈ 𝐴 ⦋𝑘 / 𝑥⦌𝐵) |
| 69 | | nfcv 2905 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘𝐵 |
| 70 | 69, 49, 39 | cbvixp 8954 |
. . . . . . . . . . . . . . . 16
⊢ X𝑥 ∈
𝐴 𝐵 = X𝑘 ∈ 𝐴 ⦋𝑘 / 𝑥⦌𝐵 |
| 71 | 68, 70 | eleqtrrdi 2852 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → (𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘))) ∈ X𝑥 ∈ 𝐴 𝐵) |
| 72 | | simprl 771 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → 𝑥 ∈ 𝐴) |
| 73 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘))) = (𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘))) |
| 74 | | vex 3484 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑧 ∈ V |
| 75 | 38, 73, 74 | fvmpt 7016 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝐴 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)))‘𝑥) = 𝑧) |
| 76 | 75 | ad2antrl 728 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → ((𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)))‘𝑥) = 𝑧) |
| 77 | 76 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → 𝑧 = ((𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)))‘𝑥)) |
| 78 | | fveq1 6905 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘))) → (𝑓‘𝑦) = ((𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)))‘𝑦)) |
| 79 | 78 | eqeq2d 2748 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘))) → (𝑧 = (𝑓‘𝑦) ↔ 𝑧 = ((𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)))‘𝑦))) |
| 80 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑥 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)))‘𝑦) = ((𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)))‘𝑥)) |
| 81 | 80 | eqeq2d 2748 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑥 → (𝑧 = ((𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)))‘𝑦) ↔ 𝑧 = ((𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)))‘𝑥))) |
| 82 | 79, 81 | rspc2ev 3635 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘))) ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = ((𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)))‘𝑥)) → ∃𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦)) |
| 83 | 71, 72, 77, 82 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ ((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → ∃𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦)) |
| 84 | 83 | exp32 420 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ X𝑥 ∈
𝐴 𝐵 → (𝑥 ∈ 𝐴 → (𝑧 ∈ 𝐵 → ∃𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦)))) |
| 85 | 34, 36, 84 | rexlimd 3266 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ X𝑥 ∈
𝐴 𝐵 → (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 → ∃𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦))) |
| 86 | 32, 85 | biimtrid 242 |
. . . . . . . . . . 11
⊢ (𝑔 ∈ X𝑥 ∈
𝐴 𝐵 → (𝑧 ∈ ∪
𝑥 ∈ 𝐴 𝐵 → ∃𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦))) |
| 87 | 86 | exlimiv 1930 |
. . . . . . . . . 10
⊢
(∃𝑔 𝑔 ∈ X𝑥 ∈
𝐴 𝐵 → (𝑧 ∈ ∪
𝑥 ∈ 𝐴 𝐵 → ∃𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦))) |
| 88 | 31, 87 | sylbi 217 |
. . . . . . . . 9
⊢ (X𝑥 ∈
𝐴 𝐵 ≠ ∅ → (𝑧 ∈ ∪
𝑥 ∈ 𝐴 𝐵 → ∃𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦))) |
| 89 | 88 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → (𝑧 ∈ ∪
𝑥 ∈ 𝐴 𝐵 → ∃𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦))) |
| 90 | 89 | alrimiv 1927 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → ∀𝑧(𝑧 ∈ ∪
𝑥 ∈ 𝐴 𝐵 → ∃𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦))) |
| 91 | | ssab 4064 |
. . . . . . 7
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ {𝑧 ∣ ∃𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦)} ↔ ∀𝑧(𝑧 ∈ ∪
𝑥 ∈ 𝐴 𝐵 → ∃𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦))) |
| 92 | 90, 91 | sylibr 234 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ {𝑧 ∣ ∃𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦)}) |
| 93 | 17 | rnmpo 7566 |
. . . . . 6
⊢ ran
(𝑓 ∈ X𝑥 ∈
𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)) = {𝑧 ∣ ∃𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦)} |
| 94 | 92, 93 | sseqtrrdi 4025 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ran (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦))) |
| 95 | 19 | frnd 6744 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → ran (𝑓 ∈ X𝑥 ∈
𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)) ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) |
| 96 | 94, 95 | eqssd 4001 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → ∪ 𝑥 ∈ 𝐴 𝐵 = ran (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦))) |
| 97 | | foeq3 6818 |
. . . 4
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 = ran (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)) → ((𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)):(X𝑥 ∈ 𝐴 𝐵 × 𝐴)–onto→∪ 𝑥 ∈ 𝐴 𝐵 ↔ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)):(X𝑥 ∈ 𝐴 𝐵 × 𝐴)–onto→ran (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)))) |
| 98 | 96, 97 | syl 17 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → ((𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)):(X𝑥 ∈ 𝐴 𝐵 × 𝐴)–onto→∪ 𝑥 ∈ 𝐴 𝐵 ↔ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)):(X𝑥 ∈ 𝐴 𝐵 × 𝐴)–onto→ran (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)))) |
| 99 | 30, 98 | mpbird 257 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)):(X𝑥 ∈ 𝐴 𝐵 × 𝐴)–onto→∪ 𝑥 ∈ 𝐴 𝐵) |
| 100 | | fowdom 9611 |
. 2
⊢ (((𝑓 ∈ X𝑥 ∈
𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)) ∈ V ∧ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)):(X𝑥 ∈ 𝐴 𝐵 × 𝐴)–onto→∪ 𝑥 ∈ 𝐴 𝐵) → ∪
𝑥 ∈ 𝐴 𝐵 ≼* (X𝑥 ∈
𝐴 𝐵 × 𝐴)) |
| 101 | 27, 99, 100 | syl2anc 584 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → ∪ 𝑥 ∈ 𝐴 𝐵 ≼* (X𝑥 ∈
𝐴 𝐵 × 𝐴)) |