Step |
Hyp |
Ref |
Expression |
1 |
|
funcnvmpt.0 |
⊢ Ⅎ 𝑥 𝜑 |
2 |
|
funcnvmpt.1 |
⊢ Ⅎ 𝑥 𝐴 |
3 |
|
funcnvmpt.2 |
⊢ Ⅎ 𝑥 𝐹 |
4 |
|
funcnvmpt.3 |
⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) |
5 |
|
funcnvmpt.4 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 ) |
6 |
|
relcnv |
⊢ Rel ◡ 𝐹 |
7 |
|
nfcv |
⊢ Ⅎ 𝑦 ◡ 𝐹 |
8 |
3
|
nfcnv |
⊢ Ⅎ 𝑥 ◡ 𝐹 |
9 |
7 8
|
dffun6f |
⊢ ( Fun ◡ 𝐹 ↔ ( Rel ◡ 𝐹 ∧ ∀ 𝑦 ∃* 𝑥 𝑦 ◡ 𝐹 𝑥 ) ) |
10 |
6 9
|
mpbiran |
⊢ ( Fun ◡ 𝐹 ↔ ∀ 𝑦 ∃* 𝑥 𝑦 ◡ 𝐹 𝑥 ) |
11 |
|
vex |
⊢ 𝑦 ∈ V |
12 |
|
vex |
⊢ 𝑥 ∈ V |
13 |
11 12
|
brcnv |
⊢ ( 𝑦 ◡ 𝐹 𝑥 ↔ 𝑥 𝐹 𝑦 ) |
14 |
13
|
mobii |
⊢ ( ∃* 𝑥 𝑦 ◡ 𝐹 𝑥 ↔ ∃* 𝑥 𝑥 𝐹 𝑦 ) |
15 |
14
|
albii |
⊢ ( ∀ 𝑦 ∃* 𝑥 𝑦 ◡ 𝐹 𝑥 ↔ ∀ 𝑦 ∃* 𝑥 𝑥 𝐹 𝑦 ) |
16 |
10 15
|
bitri |
⊢ ( Fun ◡ 𝐹 ↔ ∀ 𝑦 ∃* 𝑥 𝑥 𝐹 𝑦 ) |
17 |
4
|
funmpt2 |
⊢ Fun 𝐹 |
18 |
|
funbrfv2b |
⊢ ( Fun 𝐹 → ( 𝑥 𝐹 𝑦 ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) ) |
19 |
17 18
|
ax-mp |
⊢ ( 𝑥 𝐹 𝑦 ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) |
20 |
4
|
dmmpt |
⊢ dom 𝐹 = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V } |
21 |
5
|
elexd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ V ) |
22 |
21
|
ex |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝐵 ∈ V ) ) |
23 |
1 22
|
ralrimi |
⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ) |
24 |
2
|
rabid2f |
⊢ ( 𝐴 = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V } ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ) |
25 |
23 24
|
sylibr |
⊢ ( 𝜑 → 𝐴 = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V } ) |
26 |
20 25
|
eqtr4id |
⊢ ( 𝜑 → dom 𝐹 = 𝐴 ) |
27 |
26
|
eleq2d |
⊢ ( 𝜑 → ( 𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴 ) ) |
28 |
27
|
anbi1d |
⊢ ( 𝜑 → ( ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) ) |
29 |
19 28
|
syl5bb |
⊢ ( 𝜑 → ( 𝑥 𝐹 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) ) |
30 |
29
|
bian1d |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) ) ) |
31 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 ) |
32 |
4
|
fveq1i |
⊢ ( 𝐹 ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) |
33 |
2
|
fvmpt2f |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 ) |
34 |
32 33
|
syl5eq |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 ) |
35 |
31 5 34
|
syl2anc |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 ) |
36 |
35
|
eqeq2d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ 𝑦 = 𝐵 ) ) |
37 |
|
eqcom |
⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) |
38 |
27
|
biimpar |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ dom 𝐹 ) |
39 |
|
funbrfvb |
⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ 𝑥 𝐹 𝑦 ) ) |
40 |
17 38 39
|
sylancr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑦 ↔ 𝑥 𝐹 𝑦 ) ) |
41 |
37 40
|
bitr3id |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 = ( 𝐹 ‘ 𝑥 ) ↔ 𝑥 𝐹 𝑦 ) ) |
42 |
36 41
|
bitr3d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 = 𝐵 ↔ 𝑥 𝐹 𝑦 ) ) |
43 |
42
|
pm5.32da |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝐹 𝑦 ) ) ) |
44 |
30 43 29
|
3bitr4rd |
⊢ ( 𝜑 → ( 𝑥 𝐹 𝑦 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ) ) |
45 |
1 44
|
mobid |
⊢ ( 𝜑 → ( ∃* 𝑥 𝑥 𝐹 𝑦 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ) ) |
46 |
|
df-rmo |
⊢ ( ∃* 𝑥 ∈ 𝐴 𝑦 = 𝐵 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ) |
47 |
45 46
|
bitr4di |
⊢ ( 𝜑 → ( ∃* 𝑥 𝑥 𝐹 𝑦 ↔ ∃* 𝑥 ∈ 𝐴 𝑦 = 𝐵 ) ) |
48 |
47
|
albidv |
⊢ ( 𝜑 → ( ∀ 𝑦 ∃* 𝑥 𝑥 𝐹 𝑦 ↔ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 = 𝐵 ) ) |
49 |
16 48
|
syl5bb |
⊢ ( 𝜑 → ( Fun ◡ 𝐹 ↔ ∀ 𝑦 ∃* 𝑥 ∈ 𝐴 𝑦 = 𝐵 ) ) |