Step |
Hyp |
Ref |
Expression |
1 |
|
uniexr |
⊢ ( ∪ 𝐴 ∈ dom card → 𝐴 ∈ V ) |
2 |
|
dfac8b |
⊢ ( ∪ 𝐴 ∈ dom card → ∃ 𝑟 𝑟 We ∪ 𝐴 ) |
3 |
|
dfac8c |
⊢ ( 𝐴 ∈ V → ( ∃ 𝑟 𝑟 We ∪ 𝐴 → ∃ 𝑔 ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
4 |
1 2 3
|
sylc |
⊢ ( ∪ 𝐴 ∈ dom card → ∃ 𝑔 ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) |
5 |
4
|
adantr |
⊢ ( ( ∪ 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) → ∃ 𝑔 ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) |
6 |
1
|
ad2antrr |
⊢ ( ( ( ∪ 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) → 𝐴 ∈ V ) |
7 |
6
|
mptexd |
⊢ ( ( ( ∪ 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) → ( 𝑦 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) ∈ V ) |
8 |
|
nelne2 |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) → 𝑥 ≠ ∅ ) |
9 |
8
|
ancoms |
⊢ ( ( ¬ ∅ ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≠ ∅ ) |
10 |
9
|
adantll |
⊢ ( ( ( ∪ 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≠ ∅ ) |
11 |
|
pm2.27 |
⊢ ( 𝑥 ≠ ∅ → ( ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) |
12 |
10 11
|
syl |
⊢ ( ( ( ∪ 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) |
13 |
12
|
ralimdva |
⊢ ( ( ∪ 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) → ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) |
14 |
13
|
imp |
⊢ ( ( ( ∪ 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) |
15 |
|
fveq2 |
⊢ ( 𝑥 = 𝑦 → ( 𝑔 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑦 ) ) |
16 |
|
id |
⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 ) |
17 |
15 16
|
eleq12d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ↔ ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) ) |
18 |
17
|
rspccva |
⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) |
19 |
14 18
|
sylan |
⊢ ( ( ( ( ∪ 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ) |
20 |
|
elunii |
⊢ ( ( ( 𝑔 ‘ 𝑦 ) ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑦 ) ∈ ∪ 𝐴 ) |
21 |
19 20
|
sylancom |
⊢ ( ( ( ( ∪ 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑦 ) ∈ ∪ 𝐴 ) |
22 |
21
|
fmpttd |
⊢ ( ( ( ∪ 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) → ( 𝑦 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) : 𝐴 ⟶ ∪ 𝐴 ) |
23 |
|
fveq2 |
⊢ ( 𝑦 = 𝑥 → ( 𝑔 ‘ 𝑦 ) = ( 𝑔 ‘ 𝑥 ) ) |
24 |
|
eqid |
⊢ ( 𝑦 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) = ( 𝑦 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) |
25 |
|
fvex |
⊢ ( 𝑔 ‘ 𝑥 ) ∈ V |
26 |
23 24 25
|
fvmpt |
⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑦 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) ‘ 𝑥 ) = ( 𝑔 ‘ 𝑥 ) ) |
27 |
26
|
eleq1d |
⊢ ( 𝑥 ∈ 𝐴 → ( ( ( 𝑦 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) ‘ 𝑥 ) ∈ 𝑥 ↔ ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) |
28 |
27
|
ralbiia |
⊢ ( ∀ 𝑥 ∈ 𝐴 ( ( 𝑦 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) ‘ 𝑥 ) ∈ 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) |
29 |
14 28
|
sylibr |
⊢ ( ( ( ∪ 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) → ∀ 𝑥 ∈ 𝐴 ( ( 𝑦 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) ‘ 𝑥 ) ∈ 𝑥 ) |
30 |
22 29
|
jca |
⊢ ( ( ( ∪ 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) → ( ( 𝑦 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) : 𝐴 ⟶ ∪ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( ( 𝑦 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) ‘ 𝑥 ) ∈ 𝑥 ) ) |
31 |
|
feq1 |
⊢ ( 𝑓 = ( 𝑦 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) → ( 𝑓 : 𝐴 ⟶ ∪ 𝐴 ↔ ( 𝑦 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) : 𝐴 ⟶ ∪ 𝐴 ) ) |
32 |
|
fveq1 |
⊢ ( 𝑓 = ( 𝑦 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) → ( 𝑓 ‘ 𝑥 ) = ( ( 𝑦 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) ‘ 𝑥 ) ) |
33 |
32
|
eleq1d |
⊢ ( 𝑓 = ( 𝑦 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) → ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ↔ ( ( 𝑦 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) ‘ 𝑥 ) ∈ 𝑥 ) ) |
34 |
33
|
ralbidv |
⊢ ( 𝑓 = ( 𝑦 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝑦 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) ‘ 𝑥 ) ∈ 𝑥 ) ) |
35 |
31 34
|
anbi12d |
⊢ ( 𝑓 = ( 𝑦 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) → ( ( 𝑓 : 𝐴 ⟶ ∪ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ↔ ( ( 𝑦 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) : 𝐴 ⟶ ∪ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( ( 𝑦 ∈ 𝐴 ↦ ( 𝑔 ‘ 𝑦 ) ) ‘ 𝑥 ) ∈ 𝑥 ) ) ) |
36 |
7 30 35
|
spcedv |
⊢ ( ( ( ∪ 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ≠ ∅ → ( 𝑔 ‘ 𝑥 ) ∈ 𝑥 ) ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ ∪ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) |
37 |
5 36
|
exlimddv |
⊢ ( ( ∪ 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴 ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ ∪ 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝑥 ) ) |