Step |
Hyp |
Ref |
Expression |
1 |
|
domss2.1 |
⊢ 𝐺 = ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) |
2 |
|
f1f1orn |
⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 ) |
3 |
2
|
3ad2ant1 |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 ) |
4 |
|
simp2 |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐴 ∈ 𝑉 ) |
5 |
|
rnexg |
⊢ ( 𝐴 ∈ 𝑉 → ran 𝐴 ∈ V ) |
6 |
4 5
|
syl |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ran 𝐴 ∈ V ) |
7 |
|
uniexg |
⊢ ( ran 𝐴 ∈ V → ∪ ran 𝐴 ∈ V ) |
8 |
|
pwexg |
⊢ ( ∪ ran 𝐴 ∈ V → 𝒫 ∪ ran 𝐴 ∈ V ) |
9 |
6 7 8
|
3syl |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝒫 ∪ ran 𝐴 ∈ V ) |
10 |
|
1stconst |
⊢ ( 𝒫 ∪ ran 𝐴 ∈ V → ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) : ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) –1-1-onto→ ( 𝐵 ∖ ran 𝐹 ) ) |
11 |
9 10
|
syl |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) : ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) –1-1-onto→ ( 𝐵 ∖ ran 𝐹 ) ) |
12 |
|
difexg |
⊢ ( 𝐵 ∈ 𝑊 → ( 𝐵 ∖ ran 𝐹 ) ∈ V ) |
13 |
12
|
3ad2ant3 |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐵 ∖ ran 𝐹 ) ∈ V ) |
14 |
|
disjen |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 ∖ ran 𝐹 ) ∈ V ) → ( ( 𝐴 ∩ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) = ∅ ∧ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ≈ ( 𝐵 ∖ ran 𝐹 ) ) ) |
15 |
4 13 14
|
syl2anc |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 ∩ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) = ∅ ∧ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ≈ ( 𝐵 ∖ ran 𝐹 ) ) ) |
16 |
15
|
simpld |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ∩ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) = ∅ ) |
17 |
|
disjdif |
⊢ ( ran 𝐹 ∩ ( 𝐵 ∖ ran 𝐹 ) ) = ∅ |
18 |
17
|
a1i |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ran 𝐹 ∩ ( 𝐵 ∖ ran 𝐹 ) ) = ∅ ) |
19 |
|
f1oun |
⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ ran 𝐹 ∧ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) : ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) –1-1-onto→ ( 𝐵 ∖ ran 𝐹 ) ) ∧ ( ( 𝐴 ∩ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) = ∅ ∧ ( ran 𝐹 ∩ ( 𝐵 ∖ ran 𝐹 ) ) = ∅ ) ) → ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : ( 𝐴 ∪ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) –1-1-onto→ ( ran 𝐹 ∪ ( 𝐵 ∖ ran 𝐹 ) ) ) |
20 |
3 11 16 18 19
|
syl22anc |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : ( 𝐴 ∪ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) –1-1-onto→ ( ran 𝐹 ∪ ( 𝐵 ∖ ran 𝐹 ) ) ) |
21 |
|
undif2 |
⊢ ( ran 𝐹 ∪ ( 𝐵 ∖ ran 𝐹 ) ) = ( ran 𝐹 ∪ 𝐵 ) |
22 |
|
f1f |
⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 ) |
23 |
22
|
3ad2ant1 |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐹 : 𝐴 ⟶ 𝐵 ) |
24 |
23
|
frnd |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ran 𝐹 ⊆ 𝐵 ) |
25 |
|
ssequn1 |
⊢ ( ran 𝐹 ⊆ 𝐵 ↔ ( ran 𝐹 ∪ 𝐵 ) = 𝐵 ) |
26 |
24 25
|
sylib |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ran 𝐹 ∪ 𝐵 ) = 𝐵 ) |
27 |
21 26
|
syl5eq |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ran 𝐹 ∪ ( 𝐵 ∖ ran 𝐹 ) ) = 𝐵 ) |
28 |
27
|
f1oeq3d |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : ( 𝐴 ∪ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) –1-1-onto→ ( ran 𝐹 ∪ ( 𝐵 ∖ ran 𝐹 ) ) ↔ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : ( 𝐴 ∪ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) –1-1-onto→ 𝐵 ) ) |
29 |
20 28
|
mpbid |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : ( 𝐴 ∪ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) –1-1-onto→ 𝐵 ) |
30 |
|
f1ocnv |
⊢ ( ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : ( 𝐴 ∪ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) –1-1-onto→ 𝐵 → ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1-onto→ ( 𝐴 ∪ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) |
31 |
29 30
|
syl |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1-onto→ ( 𝐴 ∪ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) |
32 |
|
f1oeq1 |
⊢ ( 𝐺 = ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) → ( 𝐺 : 𝐵 –1-1-onto→ ( 𝐴 ∪ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ↔ ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1-onto→ ( 𝐴 ∪ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ) |
33 |
1 32
|
ax-mp |
⊢ ( 𝐺 : 𝐵 –1-1-onto→ ( 𝐴 ∪ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ↔ ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) : 𝐵 –1-1-onto→ ( 𝐴 ∪ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) |
34 |
31 33
|
sylibr |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐺 : 𝐵 –1-1-onto→ ( 𝐴 ∪ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) |
35 |
|
f1ofo |
⊢ ( 𝐺 : 𝐵 –1-1-onto→ ( 𝐴 ∪ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) → 𝐺 : 𝐵 –onto→ ( 𝐴 ∪ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) |
36 |
|
forn |
⊢ ( 𝐺 : 𝐵 –onto→ ( 𝐴 ∪ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) → ran 𝐺 = ( 𝐴 ∪ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) |
37 |
34 35 36
|
3syl |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ran 𝐺 = ( 𝐴 ∪ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) |
38 |
37
|
f1oeq3d |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐺 : 𝐵 –1-1-onto→ ran 𝐺 ↔ 𝐺 : 𝐵 –1-1-onto→ ( 𝐴 ∪ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ) |
39 |
34 38
|
mpbird |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐺 : 𝐵 –1-1-onto→ ran 𝐺 ) |
40 |
|
ssun1 |
⊢ 𝐴 ⊆ ( 𝐴 ∪ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) |
41 |
40 37
|
sseqtrrid |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐴 ⊆ ran 𝐺 ) |
42 |
|
ssid |
⊢ ran 𝐹 ⊆ ran 𝐹 |
43 |
|
cores |
⊢ ( ran 𝐹 ⊆ ran 𝐹 → ( ( 𝐺 ↾ ran 𝐹 ) ∘ 𝐹 ) = ( 𝐺 ∘ 𝐹 ) ) |
44 |
42 43
|
ax-mp |
⊢ ( ( 𝐺 ↾ ran 𝐹 ) ∘ 𝐹 ) = ( 𝐺 ∘ 𝐹 ) |
45 |
|
dmres |
⊢ dom ( ◡ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ↾ ran 𝐹 ) = ( ran 𝐹 ∩ dom ◡ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) |
46 |
|
f1ocnv |
⊢ ( ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) : ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) –1-1-onto→ ( 𝐵 ∖ ran 𝐹 ) → ◡ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) : ( 𝐵 ∖ ran 𝐹 ) –1-1-onto→ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) |
47 |
|
f1odm |
⊢ ( ◡ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) : ( 𝐵 ∖ ran 𝐹 ) –1-1-onto→ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) → dom ◡ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) = ( 𝐵 ∖ ran 𝐹 ) ) |
48 |
11 46 47
|
3syl |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → dom ◡ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) = ( 𝐵 ∖ ran 𝐹 ) ) |
49 |
48
|
ineq2d |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ran 𝐹 ∩ dom ◡ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) = ( ran 𝐹 ∩ ( 𝐵 ∖ ran 𝐹 ) ) ) |
50 |
49 17
|
eqtrdi |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ran 𝐹 ∩ dom ◡ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) = ∅ ) |
51 |
45 50
|
syl5eq |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → dom ( ◡ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ↾ ran 𝐹 ) = ∅ ) |
52 |
|
relres |
⊢ Rel ( ◡ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ↾ ran 𝐹 ) |
53 |
|
reldm0 |
⊢ ( Rel ( ◡ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ↾ ran 𝐹 ) → ( ( ◡ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ↾ ran 𝐹 ) = ∅ ↔ dom ( ◡ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ↾ ran 𝐹 ) = ∅ ) ) |
54 |
52 53
|
ax-mp |
⊢ ( ( ◡ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ↾ ran 𝐹 ) = ∅ ↔ dom ( ◡ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ↾ ran 𝐹 ) = ∅ ) |
55 |
51 54
|
sylibr |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ◡ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ↾ ran 𝐹 ) = ∅ ) |
56 |
55
|
uneq2d |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ◡ 𝐹 ∪ ( ◡ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ↾ ran 𝐹 ) ) = ( ◡ 𝐹 ∪ ∅ ) ) |
57 |
|
cnvun |
⊢ ◡ ( 𝐹 ∪ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) = ( ◡ 𝐹 ∪ ◡ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) |
58 |
1 57
|
eqtri |
⊢ 𝐺 = ( ◡ 𝐹 ∪ ◡ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) |
59 |
58
|
reseq1i |
⊢ ( 𝐺 ↾ ran 𝐹 ) = ( ( ◡ 𝐹 ∪ ◡ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ↾ ran 𝐹 ) |
60 |
|
resundir |
⊢ ( ( ◡ 𝐹 ∪ ◡ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ) ↾ ran 𝐹 ) = ( ( ◡ 𝐹 ↾ ran 𝐹 ) ∪ ( ◡ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ↾ ran 𝐹 ) ) |
61 |
|
df-rn |
⊢ ran 𝐹 = dom ◡ 𝐹 |
62 |
61
|
reseq2i |
⊢ ( ◡ 𝐹 ↾ ran 𝐹 ) = ( ◡ 𝐹 ↾ dom ◡ 𝐹 ) |
63 |
|
relcnv |
⊢ Rel ◡ 𝐹 |
64 |
|
resdm |
⊢ ( Rel ◡ 𝐹 → ( ◡ 𝐹 ↾ dom ◡ 𝐹 ) = ◡ 𝐹 ) |
65 |
63 64
|
ax-mp |
⊢ ( ◡ 𝐹 ↾ dom ◡ 𝐹 ) = ◡ 𝐹 |
66 |
62 65
|
eqtri |
⊢ ( ◡ 𝐹 ↾ ran 𝐹 ) = ◡ 𝐹 |
67 |
66
|
uneq1i |
⊢ ( ( ◡ 𝐹 ↾ ran 𝐹 ) ∪ ( ◡ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ↾ ran 𝐹 ) ) = ( ◡ 𝐹 ∪ ( ◡ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ↾ ran 𝐹 ) ) |
68 |
59 60 67
|
3eqtrri |
⊢ ( ◡ 𝐹 ∪ ( ◡ ( 1st ↾ ( ( 𝐵 ∖ ran 𝐹 ) × { 𝒫 ∪ ran 𝐴 } ) ) ↾ ran 𝐹 ) ) = ( 𝐺 ↾ ran 𝐹 ) |
69 |
|
un0 |
⊢ ( ◡ 𝐹 ∪ ∅ ) = ◡ 𝐹 |
70 |
56 68 69
|
3eqtr3g |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐺 ↾ ran 𝐹 ) = ◡ 𝐹 ) |
71 |
70
|
coeq1d |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐺 ↾ ran 𝐹 ) ∘ 𝐹 ) = ( ◡ 𝐹 ∘ 𝐹 ) ) |
72 |
|
f1cocnv1 |
⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) |
73 |
72
|
3ad2ant1 |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) |
74 |
71 73
|
eqtrd |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐺 ↾ ran 𝐹 ) ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) |
75 |
44 74
|
syl5eqr |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) |
76 |
39 41 75
|
3jca |
⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐺 : 𝐵 –1-1-onto→ ran 𝐺 ∧ 𝐴 ⊆ ran 𝐺 ∧ ( 𝐺 ∘ 𝐹 ) = ( I ↾ 𝐴 ) ) ) |