Step |
Hyp |
Ref |
Expression |
1 |
|
ancom |
⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 𝑥 𝐹 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑥 𝐹 𝑦 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑥 𝐹 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 𝑥 𝐹 𝑦 ) ) |
2 |
|
vex |
⊢ 𝑦 ∈ V |
3 |
2
|
brresi |
⊢ ( 𝑥 ( 𝐹 ↾ 𝐴 ) 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ) |
4 |
3
|
mobii |
⊢ ( ∃* 𝑦 𝑥 ( 𝐹 ↾ 𝐴 ) 𝑦 ↔ ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ) |
5 |
|
moanimv |
⊢ ( ∃* 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 → ∃* 𝑦 𝑥 𝐹 𝑦 ) ) |
6 |
4 5
|
bitri |
⊢ ( ∃* 𝑦 𝑥 ( 𝐹 ↾ 𝐴 ) 𝑦 ↔ ( 𝑥 ∈ 𝐴 → ∃* 𝑦 𝑥 𝐹 𝑦 ) ) |
7 |
6
|
albii |
⊢ ( ∀ 𝑥 ∃* 𝑦 𝑥 ( 𝐹 ↾ 𝐴 ) 𝑦 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∃* 𝑦 𝑥 𝐹 𝑦 ) ) |
8 |
|
relres |
⊢ Rel ( 𝐹 ↾ 𝐴 ) |
9 |
|
dffun6 |
⊢ ( Fun ( 𝐹 ↾ 𝐴 ) ↔ ( Rel ( 𝐹 ↾ 𝐴 ) ∧ ∀ 𝑥 ∃* 𝑦 𝑥 ( 𝐹 ↾ 𝐴 ) 𝑦 ) ) |
10 |
8 9
|
mpbiran |
⊢ ( Fun ( 𝐹 ↾ 𝐴 ) ↔ ∀ 𝑥 ∃* 𝑦 𝑥 ( 𝐹 ↾ 𝐴 ) 𝑦 ) |
11 |
|
df-ral |
⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 𝑥 𝐹 𝑦 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∃* 𝑦 𝑥 𝐹 𝑦 ) ) |
12 |
7 10 11
|
3bitr4i |
⊢ ( Fun ( 𝐹 ↾ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 𝑥 𝐹 𝑦 ) |
13 |
|
dmres |
⊢ dom ( 𝐹 ↾ 𝐴 ) = ( 𝐴 ∩ dom 𝐹 ) |
14 |
|
inss1 |
⊢ ( 𝐴 ∩ dom 𝐹 ) ⊆ 𝐴 |
15 |
13 14
|
eqsstri |
⊢ dom ( 𝐹 ↾ 𝐴 ) ⊆ 𝐴 |
16 |
|
eqss |
⊢ ( dom ( 𝐹 ↾ 𝐴 ) = 𝐴 ↔ ( dom ( 𝐹 ↾ 𝐴 ) ⊆ 𝐴 ∧ 𝐴 ⊆ dom ( 𝐹 ↾ 𝐴 ) ) ) |
17 |
15 16
|
mpbiran |
⊢ ( dom ( 𝐹 ↾ 𝐴 ) = 𝐴 ↔ 𝐴 ⊆ dom ( 𝐹 ↾ 𝐴 ) ) |
18 |
|
dfss3 |
⊢ ( 𝐴 ⊆ dom ( 𝐹 ↾ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ) |
19 |
13
|
elin2 |
⊢ ( 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ dom 𝐹 ) ) |
20 |
19
|
baib |
⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ↔ 𝑥 ∈ dom 𝐹 ) ) |
21 |
|
vex |
⊢ 𝑥 ∈ V |
22 |
21
|
eldm |
⊢ ( 𝑥 ∈ dom 𝐹 ↔ ∃ 𝑦 𝑥 𝐹 𝑦 ) |
23 |
20 22
|
bitrdi |
⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ↔ ∃ 𝑦 𝑥 𝐹 𝑦 ) ) |
24 |
23
|
ralbiia |
⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑥 𝐹 𝑦 ) |
25 |
18 24
|
bitri |
⊢ ( 𝐴 ⊆ dom ( 𝐹 ↾ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑥 𝐹 𝑦 ) |
26 |
17 25
|
bitri |
⊢ ( dom ( 𝐹 ↾ 𝐴 ) = 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑥 𝐹 𝑦 ) |
27 |
12 26
|
anbi12i |
⊢ ( ( Fun ( 𝐹 ↾ 𝐴 ) ∧ dom ( 𝐹 ↾ 𝐴 ) = 𝐴 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 𝑥 𝐹 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑥 𝐹 𝑦 ) ) |
28 |
|
r19.26 |
⊢ ( ∀ 𝑥 ∈ 𝐴 ( ∃ 𝑦 𝑥 𝐹 𝑦 ∧ ∃* 𝑦 𝑥 𝐹 𝑦 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑥 𝐹 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 𝑥 𝐹 𝑦 ) ) |
29 |
1 27 28
|
3bitr4i |
⊢ ( ( Fun ( 𝐹 ↾ 𝐴 ) ∧ dom ( 𝐹 ↾ 𝐴 ) = 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ∃ 𝑦 𝑥 𝐹 𝑦 ∧ ∃* 𝑦 𝑥 𝐹 𝑦 ) ) |
30 |
|
df-fn |
⊢ ( ( 𝐹 ↾ 𝐴 ) Fn 𝐴 ↔ ( Fun ( 𝐹 ↾ 𝐴 ) ∧ dom ( 𝐹 ↾ 𝐴 ) = 𝐴 ) ) |
31 |
|
df-eu |
⊢ ( ∃! 𝑦 𝑥 𝐹 𝑦 ↔ ( ∃ 𝑦 𝑥 𝐹 𝑦 ∧ ∃* 𝑦 𝑥 𝐹 𝑦 ) ) |
32 |
31
|
ralbii |
⊢ ( ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 ( ∃ 𝑦 𝑥 𝐹 𝑦 ∧ ∃* 𝑦 𝑥 𝐹 𝑦 ) ) |
33 |
29 30 32
|
3bitr4i |
⊢ ( ( 𝐹 ↾ 𝐴 ) Fn 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∃! 𝑦 𝑥 𝐹 𝑦 ) |