Step | Hyp | Ref
| Expression |
1 | | df-dju 9396 |
. . . 4
⊢ (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵)) |
2 | 1 | eleq2i 2824 |
. . 3
⊢ (𝐶 ∈ (𝐴 ⊔ 𝐵) ↔ 𝐶 ∈ (({∅} × 𝐴) ∪ ({1o} ×
𝐵))) |
3 | | elun 4037 |
. . 3
⊢ (𝐶 ∈ (({∅} ×
𝐴) ∪ ({1o}
× 𝐵)) ↔ (𝐶 ∈ ({∅} × 𝐴) ∨ 𝐶 ∈ ({1o} × 𝐵))) |
4 | 2, 3 | sylbb 222 |
. 2
⊢ (𝐶 ∈ (𝐴 ⊔ 𝐵) → (𝐶 ∈ ({∅} × 𝐴) ∨ 𝐶 ∈ ({1o} × 𝐵))) |
5 | | xp2nd 7740 |
. . . 4
⊢ (𝐶 ∈ ({∅} × 𝐴) → (2nd
‘𝐶) ∈ 𝐴) |
6 | | 1st2nd2 7746 |
. . . . . 6
⊢ (𝐶 ∈ ({∅} × 𝐴) → 𝐶 = 〈(1st ‘𝐶), (2nd ‘𝐶)〉) |
7 | | xp1st 7739 |
. . . . . . 7
⊢ (𝐶 ∈ ({∅} × 𝐴) → (1st
‘𝐶) ∈
{∅}) |
8 | | elsni 4530 |
. . . . . . 7
⊢
((1st ‘𝐶) ∈ {∅} → (1st
‘𝐶) =
∅) |
9 | | opeq1 4756 |
. . . . . . . 8
⊢
((1st ‘𝐶) = ∅ → 〈(1st
‘𝐶), (2nd
‘𝐶)〉 =
〈∅, (2nd ‘𝐶)〉) |
10 | 9 | eqeq2d 2749 |
. . . . . . 7
⊢
((1st ‘𝐶) = ∅ → (𝐶 = 〈(1st ‘𝐶), (2nd ‘𝐶)〉 ↔ 𝐶 = 〈∅, (2nd
‘𝐶)〉)) |
11 | 7, 8, 10 | 3syl 18 |
. . . . . 6
⊢ (𝐶 ∈ ({∅} × 𝐴) → (𝐶 = 〈(1st ‘𝐶), (2nd ‘𝐶)〉 ↔ 𝐶 = 〈∅, (2nd
‘𝐶)〉)) |
12 | 6, 11 | mpbid 235 |
. . . . 5
⊢ (𝐶 ∈ ({∅} × 𝐴) → 𝐶 = 〈∅, (2nd
‘𝐶)〉) |
13 | | fvexd 6683 |
. . . . . 6
⊢ (𝐶 ∈ ({∅} × 𝐴) → (2nd
‘𝐶) ∈
V) |
14 | | opex 5319 |
. . . . . 6
⊢
〈∅, (2nd ‘𝐶)〉 ∈ V |
15 | | opeq2 4758 |
. . . . . . 7
⊢ (𝑦 = (2nd ‘𝐶) → 〈∅, 𝑦〉 = 〈∅,
(2nd ‘𝐶)〉) |
16 | | df-inl 9397 |
. . . . . . 7
⊢ inl =
(𝑦 ∈ V ↦
〈∅, 𝑦〉) |
17 | 15, 16 | fvmptg 6767 |
. . . . . 6
⊢
(((2nd ‘𝐶) ∈ V ∧ 〈∅,
(2nd ‘𝐶)〉 ∈ V) →
(inl‘(2nd ‘𝐶)) = 〈∅, (2nd
‘𝐶)〉) |
18 | 13, 14, 17 | sylancl 589 |
. . . . 5
⊢ (𝐶 ∈ ({∅} × 𝐴) →
(inl‘(2nd ‘𝐶)) = 〈∅, (2nd
‘𝐶)〉) |
19 | 12, 18 | eqtr4d 2776 |
. . . 4
⊢ (𝐶 ∈ ({∅} × 𝐴) → 𝐶 = (inl‘(2nd ‘𝐶))) |
20 | | fveq2 6668 |
. . . . 5
⊢ (𝑥 = (2nd ‘𝐶) → (inl‘𝑥) = (inl‘(2nd
‘𝐶))) |
21 | 20 | rspceeqv 3539 |
. . . 4
⊢
(((2nd ‘𝐶) ∈ 𝐴 ∧ 𝐶 = (inl‘(2nd ‘𝐶))) → ∃𝑥 ∈ 𝐴 𝐶 = (inl‘𝑥)) |
22 | 5, 19, 21 | syl2anc 587 |
. . 3
⊢ (𝐶 ∈ ({∅} × 𝐴) → ∃𝑥 ∈ 𝐴 𝐶 = (inl‘𝑥)) |
23 | | xp2nd 7740 |
. . . 4
⊢ (𝐶 ∈ ({1o} ×
𝐵) → (2nd
‘𝐶) ∈ 𝐵) |
24 | | 1st2nd2 7746 |
. . . . . 6
⊢ (𝐶 ∈ ({1o} ×
𝐵) → 𝐶 = 〈(1st ‘𝐶), (2nd ‘𝐶)〉) |
25 | | xp1st 7739 |
. . . . . . 7
⊢ (𝐶 ∈ ({1o} ×
𝐵) → (1st
‘𝐶) ∈
{1o}) |
26 | | elsni 4530 |
. . . . . . 7
⊢
((1st ‘𝐶) ∈ {1o} →
(1st ‘𝐶) =
1o) |
27 | | opeq1 4756 |
. . . . . . . 8
⊢
((1st ‘𝐶) = 1o →
〈(1st ‘𝐶), (2nd ‘𝐶)〉 = 〈1o,
(2nd ‘𝐶)〉) |
28 | 27 | eqeq2d 2749 |
. . . . . . 7
⊢
((1st ‘𝐶) = 1o → (𝐶 = 〈(1st ‘𝐶), (2nd ‘𝐶)〉 ↔ 𝐶 = 〈1o, (2nd
‘𝐶)〉)) |
29 | 25, 26, 28 | 3syl 18 |
. . . . . 6
⊢ (𝐶 ∈ ({1o} ×
𝐵) → (𝐶 = 〈(1st
‘𝐶), (2nd
‘𝐶)〉 ↔
𝐶 = 〈1o,
(2nd ‘𝐶)〉)) |
30 | 24, 29 | mpbid 235 |
. . . . 5
⊢ (𝐶 ∈ ({1o} ×
𝐵) → 𝐶 = 〈1o, (2nd
‘𝐶)〉) |
31 | | fvexd 6683 |
. . . . . 6
⊢ (𝐶 ∈ ({1o} ×
𝐵) → (2nd
‘𝐶) ∈
V) |
32 | | opex 5319 |
. . . . . 6
⊢
〈1o, (2nd ‘𝐶)〉 ∈ V |
33 | | opeq2 4758 |
. . . . . . 7
⊢ (𝑧 = (2nd ‘𝐶) → 〈1o,
𝑧〉 =
〈1o, (2nd ‘𝐶)〉) |
34 | | df-inr 9398 |
. . . . . . 7
⊢ inr =
(𝑧 ∈ V ↦
〈1o, 𝑧〉) |
35 | 33, 34 | fvmptg 6767 |
. . . . . 6
⊢
(((2nd ‘𝐶) ∈ V ∧ 〈1o,
(2nd ‘𝐶)〉 ∈ V) →
(inr‘(2nd ‘𝐶)) = 〈1o, (2nd
‘𝐶)〉) |
36 | 31, 32, 35 | sylancl 589 |
. . . . 5
⊢ (𝐶 ∈ ({1o} ×
𝐵) →
(inr‘(2nd ‘𝐶)) = 〈1o, (2nd
‘𝐶)〉) |
37 | 30, 36 | eqtr4d 2776 |
. . . 4
⊢ (𝐶 ∈ ({1o} ×
𝐵) → 𝐶 = (inr‘(2nd ‘𝐶))) |
38 | | fveq2 6668 |
. . . . 5
⊢ (𝑥 = (2nd ‘𝐶) → (inr‘𝑥) = (inr‘(2nd
‘𝐶))) |
39 | 38 | rspceeqv 3539 |
. . . 4
⊢
(((2nd ‘𝐶) ∈ 𝐵 ∧ 𝐶 = (inr‘(2nd ‘𝐶))) → ∃𝑥 ∈ 𝐵 𝐶 = (inr‘𝑥)) |
40 | 23, 37, 39 | syl2anc 587 |
. . 3
⊢ (𝐶 ∈ ({1o} ×
𝐵) → ∃𝑥 ∈ 𝐵 𝐶 = (inr‘𝑥)) |
41 | 22, 40 | orim12i 908 |
. 2
⊢ ((𝐶 ∈ ({∅} × 𝐴) ∨ 𝐶 ∈ ({1o} × 𝐵)) → (∃𝑥 ∈ 𝐴 𝐶 = (inl‘𝑥) ∨ ∃𝑥 ∈ 𝐵 𝐶 = (inr‘𝑥))) |
42 | 4, 41 | syl 17 |
1
⊢ (𝐶 ∈ (𝐴 ⊔ 𝐵) → (∃𝑥 ∈ 𝐴 𝐶 = (inl‘𝑥) ∨ ∃𝑥 ∈ 𝐵 𝐶 = (inr‘𝑥))) |