Step | Hyp | Ref
| Expression |
1 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑓 ∈ V |
2 | 1 | elixp 7915 |
. . . . . . . . 9
⊢ (𝑓 ∈ X𝑥 ∈
𝐴 𝐵 ↔ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)) |
3 | 2 | simprbi 480 |
. . . . . . . 8
⊢ (𝑓 ∈ X𝑥 ∈
𝐴 𝐵 → ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵) |
4 | | ssiun2 4563 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪
𝑥 ∈ 𝐴 𝐵) |
5 | 4 | sseld 3602 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴 → ((𝑓‘𝑥) ∈ 𝐵 → (𝑓‘𝑥) ∈ ∪
𝑥 ∈ 𝐴 𝐵)) |
6 | 5 | ralimia 2950 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐴 (𝑓‘𝑥) ∈ 𝐵 → ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
7 | 3, 6 | syl 17 |
. . . . . . 7
⊢ (𝑓 ∈ X𝑥 ∈
𝐴 𝐵 → ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
8 | | nfv 1843 |
. . . . . . . 8
⊢
Ⅎ𝑦(𝑓‘𝑥) ∈ ∪
𝑥 ∈ 𝐴 𝐵 |
9 | | nfiu1 4550 |
. . . . . . . . 9
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵 |
10 | 9 | nfel2 2781 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑓‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 𝐵 |
11 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑓‘𝑥) = (𝑓‘𝑦)) |
12 | 11 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝑓‘𝑥) ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↔ (𝑓‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 𝐵)) |
13 | 8, 10, 12 | cbvral 3167 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 (𝑓‘𝑥) ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
14 | 7, 13 | sylib 208 |
. . . . . 6
⊢ (𝑓 ∈ X𝑥 ∈
𝐴 𝐵 → ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
15 | 14 | adantl 482 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) ∧ 𝑓 ∈ X𝑥 ∈ 𝐴 𝐵) → ∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
16 | 15 | ralrimiva 2966 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → ∀𝑓 ∈ X
𝑥 ∈ 𝐴 𝐵∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
17 | | eqid 2622 |
. . . . 5
⊢ (𝑓 ∈ X𝑥 ∈
𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)) = (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)) |
18 | 17 | fmpt2 7237 |
. . . 4
⊢
(∀𝑓 ∈
X 𝑥
∈ 𝐴 𝐵∀𝑦 ∈ 𝐴 (𝑓‘𝑦) ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↔ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)):(X𝑥 ∈ 𝐴 𝐵 × 𝐴)⟶∪
𝑥 ∈ 𝐴 𝐵) |
19 | 16, 18 | sylib 208 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)):(X𝑥 ∈ 𝐴 𝐵 × 𝐴)⟶∪
𝑥 ∈ 𝐴 𝐵) |
20 | | ixpssmap2g 7937 |
. . . . . 6
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 → X𝑥 ∈ 𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑𝑚 𝐴)) |
21 | 20 | 3ad2ant2 1083 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → X𝑥 ∈
𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑𝑚 𝐴)) |
22 | | ovex 6678 |
. . . . . 6
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ↑𝑚 𝐴) ∈ V |
23 | 22 | ssex 4802 |
. . . . 5
⊢ (X𝑥 ∈
𝐴 𝐵 ⊆ (∪ 𝑥 ∈ 𝐴 𝐵 ↑𝑚 𝐴) → X𝑥 ∈
𝐴 𝐵 ∈ V) |
24 | 21, 23 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → X𝑥 ∈
𝐴 𝐵 ∈ V) |
25 | | simp1 1061 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → 𝐴 ∈ 𝑉) |
26 | | xpexg 6960 |
. . . 4
⊢ ((X𝑥 ∈
𝐴 𝐵 ∈ V ∧ 𝐴 ∈ 𝑉) → (X𝑥 ∈ 𝐴 𝐵 × 𝐴) ∈ V) |
27 | 24, 25, 26 | syl2anc 693 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → (X𝑥 ∈
𝐴 𝐵 × 𝐴) ∈ V) |
28 | | simp2 1062 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) |
29 | | fex2 7121 |
. . 3
⊢ (((𝑓 ∈ X𝑥 ∈
𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)):(X𝑥 ∈ 𝐴 𝐵 × 𝐴)⟶∪
𝑥 ∈ 𝐴 𝐵 ∧ (X𝑥 ∈ 𝐴 𝐵 × 𝐴) ∈ V ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊) → (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)) ∈ V) |
30 | 19, 27, 28, 29 | syl3anc 1326 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)) ∈ V) |
31 | | ffn 6045 |
. . . . 5
⊢ ((𝑓 ∈ X𝑥 ∈
𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)):(X𝑥 ∈ 𝐴 𝐵 × 𝐴)⟶∪
𝑥 ∈ 𝐴 𝐵 → (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)) Fn (X𝑥 ∈ 𝐴 𝐵 × 𝐴)) |
32 | 19, 31 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)) Fn (X𝑥 ∈ 𝐴 𝐵 × 𝐴)) |
33 | | dffn4 6121 |
. . . 4
⊢ ((𝑓 ∈ X𝑥 ∈
𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)) Fn (X𝑥 ∈ 𝐴 𝐵 × 𝐴) ↔ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)):(X𝑥 ∈ 𝐴 𝐵 × 𝐴)–onto→ran (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦))) |
34 | 32, 33 | sylib 208 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)):(X𝑥 ∈ 𝐴 𝐵 × 𝐴)–onto→ran (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦))) |
35 | | n0 3931 |
. . . . . . . . . 10
⊢ (X𝑥 ∈
𝐴 𝐵 ≠ ∅ ↔ ∃𝑔 𝑔 ∈ X𝑥 ∈ 𝐴 𝐵) |
36 | | eliun 4524 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵) |
37 | | nfixp1 7928 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥X𝑥 ∈
𝐴 𝐵 |
38 | 37 | nfel2 2781 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥 𝑔 ∈ X𝑥 ∈
𝐴 𝐵 |
39 | | nfv 1843 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦) |
40 | 37, 39 | nfrex 3007 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥∃𝑓 ∈ X
𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦) |
41 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑘 ∈ 𝐴) → 𝑧 ∈ 𝐵) |
42 | | iftrue 4092 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑥 → if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)) = 𝑧) |
43 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑘 → 𝐵 = ⦋𝑘 / 𝑥⦌𝐵) |
44 | 43 | equcoms 1947 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 𝑥 → 𝐵 = ⦋𝑘 / 𝑥⦌𝐵) |
45 | 44 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑥 → ⦋𝑘 / 𝑥⦌𝐵 = 𝐵) |
46 | 42, 45 | eleq12d 2695 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑥 → (if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)) ∈ ⦋𝑘 / 𝑥⦌𝐵 ↔ 𝑧 ∈ 𝐵)) |
47 | 41, 46 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑘 ∈ 𝐴) → (𝑘 = 𝑥 → if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)) ∈ ⦋𝑘 / 𝑥⦌𝐵)) |
48 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑔 ∈ V |
49 | 48 | elixp 7915 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ↔ (𝑔 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ 𝐵)) |
50 | 49 | simprbi 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑔 ∈ X𝑥 ∈
𝐴 𝐵 → ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ 𝐵) |
51 | 50 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ 𝐵) |
52 | | nfv 1843 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑘(𝑔‘𝑥) ∈ 𝐵 |
53 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑥⦋𝑘 / 𝑥⦌𝐵 |
54 | 53 | nfel2 2781 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑥(𝑔‘𝑘) ∈ ⦋𝑘 / 𝑥⦌𝐵 |
55 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑘 → (𝑔‘𝑥) = (𝑔‘𝑘)) |
56 | 55, 43 | eleq12d 2695 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 𝑘 → ((𝑔‘𝑥) ∈ 𝐵 ↔ (𝑔‘𝑘) ∈ ⦋𝑘 / 𝑥⦌𝐵)) |
57 | 52, 54, 56 | cbvral 3167 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑥 ∈
𝐴 (𝑔‘𝑥) ∈ 𝐵 ↔ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ ⦋𝑘 / 𝑥⦌𝐵) |
58 | 51, 57 | sylib 208 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ ⦋𝑘 / 𝑥⦌𝐵) |
59 | 58 | r19.21bi 2932 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑘 ∈ 𝐴) → (𝑔‘𝑘) ∈ ⦋𝑘 / 𝑥⦌𝐵) |
60 | | iffalse 4095 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
𝑘 = 𝑥 → if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)) = (𝑔‘𝑘)) |
61 | 60 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
𝑘 = 𝑥 → (if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)) ∈ ⦋𝑘 / 𝑥⦌𝐵 ↔ (𝑔‘𝑘) ∈ ⦋𝑘 / 𝑥⦌𝐵)) |
62 | 59, 61 | syl5ibrcom 237 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑘 ∈ 𝐴) → (¬ 𝑘 = 𝑥 → if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)) ∈ ⦋𝑘 / 𝑥⦌𝐵)) |
63 | 47, 62 | pm2.61d 170 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑘 ∈ 𝐴) → if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)) ∈ ⦋𝑘 / 𝑥⦌𝐵) |
64 | 63 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → ∀𝑘 ∈ 𝐴 if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)) ∈ ⦋𝑘 / 𝑥⦌𝐵) |
65 | | ixpfn 7914 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 ∈ X𝑥 ∈
𝐴 𝐵 → 𝑔 Fn 𝐴) |
66 | 65 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → 𝑔 Fn 𝐴) |
67 | | fndm 5990 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 Fn 𝐴 → dom 𝑔 = 𝐴) |
68 | 66, 67 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → dom 𝑔 = 𝐴) |
69 | 48 | dmex 7099 |
. . . . . . . . . . . . . . . . . . 19
⊢ dom 𝑔 ∈ V |
70 | 68, 69 | syl6eqelr 2710 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → 𝐴 ∈ V) |
71 | | mptelixpg 7945 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ V → ((𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘))) ∈ X𝑘 ∈ 𝐴 ⦋𝑘 / 𝑥⦌𝐵 ↔ ∀𝑘 ∈ 𝐴 if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)) ∈ ⦋𝑘 / 𝑥⦌𝐵)) |
72 | 70, 71 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → ((𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘))) ∈ X𝑘 ∈ 𝐴 ⦋𝑘 / 𝑥⦌𝐵 ↔ ∀𝑘 ∈ 𝐴 if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)) ∈ ⦋𝑘 / 𝑥⦌𝐵)) |
73 | 64, 72 | mpbird 247 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → (𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘))) ∈ X𝑘 ∈ 𝐴 ⦋𝑘 / 𝑥⦌𝐵) |
74 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘𝐵 |
75 | 74, 53, 43 | cbvixp 7925 |
. . . . . . . . . . . . . . . 16
⊢ X𝑥 ∈
𝐴 𝐵 = X𝑘 ∈ 𝐴 ⦋𝑘 / 𝑥⦌𝐵 |
76 | 73, 75 | syl6eleqr 2712 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → (𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘))) ∈ X𝑥 ∈ 𝐴 𝐵) |
77 | | simprl 794 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → 𝑥 ∈ 𝐴) |
78 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘))) = (𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘))) |
79 | | vex 3203 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑧 ∈ V |
80 | 42, 78, 79 | fvmpt 6282 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝐴 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)))‘𝑥) = 𝑧) |
81 | 80 | ad2antrl 764 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → ((𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)))‘𝑥) = 𝑧) |
82 | 81 | eqcomd 2628 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → 𝑧 = ((𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)))‘𝑥)) |
83 | | fveq1 6190 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘))) → (𝑓‘𝑦) = ((𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)))‘𝑦)) |
84 | 83 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘))) → (𝑧 = (𝑓‘𝑦) ↔ 𝑧 = ((𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)))‘𝑦))) |
85 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑥 → ((𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)))‘𝑦) = ((𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)))‘𝑥)) |
86 | 85 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑥 → (𝑧 = ((𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)))‘𝑦) ↔ 𝑧 = ((𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)))‘𝑥))) |
87 | 84, 86 | rspc2ev 3324 |
. . . . . . . . . . . . . . 15
⊢ (((𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘))) ∈ X𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = ((𝑘 ∈ 𝐴 ↦ if(𝑘 = 𝑥, 𝑧, (𝑔‘𝑘)))‘𝑥)) → ∃𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦)) |
88 | 76, 77, 82, 87 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ ((𝑔 ∈ X𝑥 ∈
𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵)) → ∃𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦)) |
89 | 88 | exp32 631 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ X𝑥 ∈
𝐴 𝐵 → (𝑥 ∈ 𝐴 → (𝑧 ∈ 𝐵 → ∃𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦)))) |
90 | 38, 40, 89 | rexlimd 3026 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ X𝑥 ∈
𝐴 𝐵 → (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 → ∃𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦))) |
91 | 36, 90 | syl5bi 232 |
. . . . . . . . . . 11
⊢ (𝑔 ∈ X𝑥 ∈
𝐴 𝐵 → (𝑧 ∈ ∪
𝑥 ∈ 𝐴 𝐵 → ∃𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦))) |
92 | 91 | exlimiv 1858 |
. . . . . . . . . 10
⊢
(∃𝑔 𝑔 ∈ X𝑥 ∈
𝐴 𝐵 → (𝑧 ∈ ∪
𝑥 ∈ 𝐴 𝐵 → ∃𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦))) |
93 | 35, 92 | sylbi 207 |
. . . . . . . . 9
⊢ (X𝑥 ∈
𝐴 𝐵 ≠ ∅ → (𝑧 ∈ ∪
𝑥 ∈ 𝐴 𝐵 → ∃𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦))) |
94 | 93 | 3ad2ant3 1084 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → (𝑧 ∈ ∪
𝑥 ∈ 𝐴 𝐵 → ∃𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦))) |
95 | 94 | alrimiv 1855 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → ∀𝑧(𝑧 ∈ ∪
𝑥 ∈ 𝐴 𝐵 → ∃𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦))) |
96 | | ssab 3672 |
. . . . . . 7
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 ⊆ {𝑧 ∣ ∃𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦)} ↔ ∀𝑧(𝑧 ∈ ∪
𝑥 ∈ 𝐴 𝐵 → ∃𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦))) |
97 | 95, 96 | sylibr 224 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ {𝑧 ∣ ∃𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦)}) |
98 | 17 | rnmpt2 6770 |
. . . . . 6
⊢ ran
(𝑓 ∈ X𝑥 ∈
𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)) = {𝑧 ∣ ∃𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵∃𝑦 ∈ 𝐴 𝑧 = (𝑓‘𝑦)} |
99 | 97, 98 | syl6sseqr 3652 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ran (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦))) |
100 | | frn 6053 |
. . . . . 6
⊢ ((𝑓 ∈ X𝑥 ∈
𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)):(X𝑥 ∈ 𝐴 𝐵 × 𝐴)⟶∪
𝑥 ∈ 𝐴 𝐵 → ran (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)) ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) |
101 | 19, 100 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → ran (𝑓 ∈ X𝑥 ∈
𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)) ⊆ ∪ 𝑥 ∈ 𝐴 𝐵) |
102 | 99, 101 | eqssd 3620 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → ∪ 𝑥 ∈ 𝐴 𝐵 = ran (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦))) |
103 | | foeq3 6113 |
. . . 4
⊢ (∪ 𝑥 ∈ 𝐴 𝐵 = ran (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)) → ((𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)):(X𝑥 ∈ 𝐴 𝐵 × 𝐴)–onto→∪ 𝑥 ∈ 𝐴 𝐵 ↔ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)):(X𝑥 ∈ 𝐴 𝐵 × 𝐴)–onto→ran (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)))) |
104 | 102, 103 | syl 17 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → ((𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)):(X𝑥 ∈ 𝐴 𝐵 × 𝐴)–onto→∪ 𝑥 ∈ 𝐴 𝐵 ↔ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)):(X𝑥 ∈ 𝐴 𝐵 × 𝐴)–onto→ran (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)))) |
105 | 34, 104 | mpbird 247 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)):(X𝑥 ∈ 𝐴 𝐵 × 𝐴)–onto→∪ 𝑥 ∈ 𝐴 𝐵) |
106 | | fowdom 8476 |
. 2
⊢ (((𝑓 ∈ X𝑥 ∈
𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)) ∈ V ∧ (𝑓 ∈ X𝑥 ∈ 𝐴 𝐵, 𝑦 ∈ 𝐴 ↦ (𝑓‘𝑦)):(X𝑥 ∈ 𝐴 𝐵 × 𝐴)–onto→∪ 𝑥 ∈ 𝐴 𝐵) → ∪
𝑥 ∈ 𝐴 𝐵 ≼* (X𝑥 ∈
𝐴 𝐵 × 𝐴)) |
107 | 30, 105, 106 | syl2anc 693 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ ∪
𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X𝑥 ∈ 𝐴 𝐵 ≠ ∅) → ∪ 𝑥 ∈ 𝐴 𝐵 ≼* (X𝑥 ∈
𝐴 𝐵 × 𝐴)) |