Step | Hyp | Ref
| Expression |
1 | | df-en 6030 |
. . 3
⊢ ≈ = {⟨x, y⟩ ∣ ∃f f:x–1-1-onto→y} |
2 | | elrn2 4898 |
. . . . 5
⊢ (⟨x, y⟩ ∈ ran ( Fns ⊗
ran (◡Image Swap
⊗ Fns )) ↔ ∃f⟨f, ⟨x, y⟩⟩ ∈ ( Fns ⊗ ran (◡Image Swap
⊗ Fns ))) |
3 | | df-br 4641 |
. . . . . . . . 9
⊢ (f Fns x ↔ ⟨f, x⟩ ∈ Fns ) |
4 | | vex 2863 |
. . . . . . . . . 10
⊢ f ∈
V |
5 | 4 | brfns 5834 |
. . . . . . . . 9
⊢ (f Fns x ↔ f Fn
x) |
6 | 3, 5 | bitr3i 242 |
. . . . . . . 8
⊢ (⟨f, x⟩ ∈ Fns ↔ f Fn x) |
7 | | elrn2 4898 |
. . . . . . . . 9
⊢ (⟨f, y⟩ ∈ ran (◡Image Swap
⊗ Fns ) ↔ ∃g⟨g, ⟨f, y⟩⟩ ∈ (◡Image Swap
⊗ Fns )) |
8 | | oteltxp 5783 |
. . . . . . . . . . . 12
⊢ (⟨g, ⟨f, y⟩⟩ ∈ (◡Image Swap
⊗ Fns ) ↔ (⟨g, f⟩ ∈ ◡Image Swap
∧ ⟨g, y⟩ ∈ Fns )) |
9 | | opelcnv 4894 |
. . . . . . . . . . . . . 14
⊢ (⟨g, f⟩ ∈ ◡Image Swap
↔ ⟨f, g⟩ ∈ Image Swap ) |
10 | | dfcnv2 5101 |
. . . . . . . . . . . . . . . 16
⊢ ◡f =
( Swap “ f) |
11 | 10 | eqeq2i 2363 |
. . . . . . . . . . . . . . 15
⊢ (g = ◡f ↔
g = ( Swap
“ f)) |
12 | | vex 2863 |
. . . . . . . . . . . . . . . 16
⊢ g ∈
V |
13 | 4, 12 | brimage 5794 |
. . . . . . . . . . . . . . 15
⊢ (fImage Swap g ↔ g =
( Swap “ f)) |
14 | | df-br 4641 |
. . . . . . . . . . . . . . 15
⊢ (fImage Swap g ↔ ⟨f, g⟩ ∈ Image Swap ) |
15 | 11, 13, 14 | 3bitr2ri 265 |
. . . . . . . . . . . . . 14
⊢ (⟨f, g⟩ ∈ Image Swap ↔
g = ◡f) |
16 | 9, 15 | bitri 240 |
. . . . . . . . . . . . 13
⊢ (⟨g, f⟩ ∈ ◡Image Swap
↔ g = ◡f) |
17 | | df-br 4641 |
. . . . . . . . . . . . . 14
⊢ (g Fns y ↔ ⟨g, y⟩ ∈ Fns ) |
18 | 12 | brfns 5834 |
. . . . . . . . . . . . . 14
⊢ (g Fns y ↔ g Fn
y) |
19 | 17, 18 | bitr3i 242 |
. . . . . . . . . . . . 13
⊢ (⟨g, y⟩ ∈ Fns ↔ g Fn y) |
20 | 16, 19 | anbi12i 678 |
. . . . . . . . . . . 12
⊢ ((⟨g, f⟩ ∈ ◡Image Swap
∧ ⟨g, y⟩ ∈ Fns ) ↔ (g =
◡f
∧ g Fn
y)) |
21 | 8, 20 | bitri 240 |
. . . . . . . . . . 11
⊢ (⟨g, ⟨f, y⟩⟩ ∈ (◡Image Swap
⊗ Fns ) ↔ (g = ◡f ∧ g Fn y)) |
22 | 21 | exbii 1582 |
. . . . . . . . . 10
⊢ (∃g⟨g, ⟨f, y⟩⟩ ∈ (◡Image Swap
⊗ Fns ) ↔ ∃g(g = ◡f ∧ g Fn y)) |
23 | 4 | cnvex 5103 |
. . . . . . . . . . 11
⊢ ◡f ∈ V |
24 | | fneq1 5174 |
. . . . . . . . . . 11
⊢ (g = ◡f →
(g Fn y
↔ ◡f Fn y)) |
25 | 23, 24 | ceqsexv 2895 |
. . . . . . . . . 10
⊢ (∃g(g = ◡f ∧ g Fn y) ↔ ◡f Fn
y) |
26 | 22, 25 | bitri 240 |
. . . . . . . . 9
⊢ (∃g⟨g, ⟨f, y⟩⟩ ∈ (◡Image Swap
⊗ Fns ) ↔ ◡f Fn
y) |
27 | 7, 26 | bitri 240 |
. . . . . . . 8
⊢ (⟨f, y⟩ ∈ ran (◡Image Swap
⊗ Fns ) ↔ ◡f Fn
y) |
28 | 6, 27 | anbi12i 678 |
. . . . . . 7
⊢ ((⟨f, x⟩ ∈ Fns ∧ ⟨f, y⟩ ∈ ran (◡Image Swap
⊗ Fns )) ↔ (f Fn x ∧ ◡f Fn y)) |
29 | | oteltxp 5783 |
. . . . . . 7
⊢ (⟨f, ⟨x, y⟩⟩ ∈ ( Fns ⊗ ran (◡Image Swap
⊗ Fns )) ↔ (⟨f, x⟩ ∈ Fns ∧ ⟨f, y⟩ ∈ ran (◡Image Swap
⊗ Fns ))) |
30 | | dff1o4 5295 |
. . . . . . 7
⊢ (f:x–1-1-onto→y ↔
(f Fn x
∧ ◡f Fn
y)) |
31 | 28, 29, 30 | 3bitr4i 268 |
. . . . . 6
⊢ (⟨f, ⟨x, y⟩⟩ ∈ ( Fns ⊗ ran (◡Image Swap
⊗ Fns )) ↔ f:x–1-1-onto→y) |
32 | 31 | exbii 1582 |
. . . . 5
⊢ (∃f⟨f, ⟨x, y⟩⟩ ∈ ( Fns ⊗ ran (◡Image Swap
⊗ Fns )) ↔ ∃f f:x–1-1-onto→y) |
33 | 2, 32 | bitri 240 |
. . . 4
⊢ (⟨x, y⟩ ∈ ran ( Fns ⊗
ran (◡Image Swap
⊗ Fns )) ↔ ∃f f:x–1-1-onto→y) |
34 | 33 | opabbi2i 4867 |
. . 3
⊢ ran ( Fns ⊗ ran (◡Image Swap
⊗ Fns )) = {⟨x, y⟩ ∣ ∃f f:x–1-1-onto→y} |
35 | 1, 34 | eqtr4i 2376 |
. 2
⊢ ≈ = ran (
Fns ⊗ ran (◡Image Swap
⊗ Fns )) |
36 | | fnsex 5833 |
. . . 4
⊢ Fns ∈
V |
37 | | swapex 4743 |
. . . . . . . 8
⊢ Swap ∈
V |
38 | 37 | imageex 5802 |
. . . . . . 7
⊢ Image Swap ∈
V |
39 | 38 | cnvex 5103 |
. . . . . 6
⊢ ◡Image Swap
∈ V |
40 | 39, 36 | txpex 5786 |
. . . . 5
⊢ (◡Image Swap
⊗ Fns ) ∈
V |
41 | 40 | rnex 5108 |
. . . 4
⊢ ran (◡Image Swap
⊗ Fns ) ∈
V |
42 | 36, 41 | txpex 5786 |
. . 3
⊢ ( Fns ⊗ ran (◡Image Swap
⊗ Fns )) ∈ V |
43 | 42 | rnex 5108 |
. 2
⊢ ran ( Fns ⊗ ran (◡Image Swap
⊗ Fns )) ∈ V |
44 | 35, 43 | eqeltri 2423 |
1
⊢ ≈ ∈ V |