Description: A member of a disjoint union can be mapped from one of the classes which produced it. (Contributed by Jim Kingdon, 23-Jun-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | djur | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-dju | |
|
2 | 1 | eleq2i | |
3 | elun | |
|
4 | 2 3 | sylbb | |
5 | xp2nd | |
|
6 | 1st2nd2 | |
|
7 | xp1st | |
|
8 | elsni | |
|
9 | opeq1 | |
|
10 | 9 | eqeq2d | |
11 | 7 8 10 | 3syl | |
12 | 6 11 | mpbid | |
13 | fvexd | |
|
14 | opex | |
|
15 | opeq2 | |
|
16 | df-inl | |
|
17 | 15 16 | fvmptg | |
18 | 13 14 17 | sylancl | |
19 | 12 18 | eqtr4d | |
20 | fveq2 | |
|
21 | 20 | rspceeqv | |
22 | 5 19 21 | syl2anc | |
23 | xp2nd | |
|
24 | 1st2nd2 | |
|
25 | xp1st | |
|
26 | elsni | |
|
27 | opeq1 | |
|
28 | 27 | eqeq2d | |
29 | 25 26 28 | 3syl | |
30 | 24 29 | mpbid | |
31 | fvexd | |
|
32 | opex | |
|
33 | opeq2 | |
|
34 | df-inr | |
|
35 | 33 34 | fvmptg | |
36 | 31 32 35 | sylancl | |
37 | 30 36 | eqtr4d | |
38 | fveq2 | |
|
39 | 38 | rspceeqv | |
40 | 23 37 39 | syl2anc | |
41 | 22 40 | orim12i | |
42 | 4 41 | syl | |