| Step | Hyp | Ref
| Expression |
| 1 | | df-dju 9941 |
. . . 4
⊢ (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵)) |
| 2 | 1 | eleq2i 2833 |
. . 3
⊢ (𝐶 ∈ (𝐴 ⊔ 𝐵) ↔ 𝐶 ∈ (({∅} × 𝐴) ∪ ({1o} ×
𝐵))) |
| 3 | | elun 4153 |
. . 3
⊢ (𝐶 ∈ (({∅} ×
𝐴) ∪ ({1o}
× 𝐵)) ↔ (𝐶 ∈ ({∅} × 𝐴) ∨ 𝐶 ∈ ({1o} × 𝐵))) |
| 4 | 2, 3 | sylbb 219 |
. 2
⊢ (𝐶 ∈ (𝐴 ⊔ 𝐵) → (𝐶 ∈ ({∅} × 𝐴) ∨ 𝐶 ∈ ({1o} × 𝐵))) |
| 5 | | xp2nd 8047 |
. . . 4
⊢ (𝐶 ∈ ({∅} × 𝐴) → (2nd
‘𝐶) ∈ 𝐴) |
| 6 | | 1st2nd2 8053 |
. . . . . 6
⊢ (𝐶 ∈ ({∅} × 𝐴) → 𝐶 = 〈(1st ‘𝐶), (2nd ‘𝐶)〉) |
| 7 | | xp1st 8046 |
. . . . . . 7
⊢ (𝐶 ∈ ({∅} × 𝐴) → (1st
‘𝐶) ∈
{∅}) |
| 8 | | elsni 4643 |
. . . . . . 7
⊢
((1st ‘𝐶) ∈ {∅} → (1st
‘𝐶) =
∅) |
| 9 | | opeq1 4873 |
. . . . . . . 8
⊢
((1st ‘𝐶) = ∅ → 〈(1st
‘𝐶), (2nd
‘𝐶)〉 =
〈∅, (2nd ‘𝐶)〉) |
| 10 | 9 | eqeq2d 2748 |
. . . . . . 7
⊢
((1st ‘𝐶) = ∅ → (𝐶 = 〈(1st ‘𝐶), (2nd ‘𝐶)〉 ↔ 𝐶 = 〈∅, (2nd
‘𝐶)〉)) |
| 11 | 7, 8, 10 | 3syl 18 |
. . . . . 6
⊢ (𝐶 ∈ ({∅} × 𝐴) → (𝐶 = 〈(1st ‘𝐶), (2nd ‘𝐶)〉 ↔ 𝐶 = 〈∅, (2nd
‘𝐶)〉)) |
| 12 | 6, 11 | mpbid 232 |
. . . . 5
⊢ (𝐶 ∈ ({∅} × 𝐴) → 𝐶 = 〈∅, (2nd
‘𝐶)〉) |
| 13 | | fvexd 6921 |
. . . . . 6
⊢ (𝐶 ∈ ({∅} × 𝐴) → (2nd
‘𝐶) ∈
V) |
| 14 | | opex 5469 |
. . . . . 6
⊢
〈∅, (2nd ‘𝐶)〉 ∈ V |
| 15 | | opeq2 4874 |
. . . . . . 7
⊢ (𝑦 = (2nd ‘𝐶) → 〈∅, 𝑦〉 = 〈∅,
(2nd ‘𝐶)〉) |
| 16 | | df-inl 9942 |
. . . . . . 7
⊢ inl =
(𝑦 ∈ V ↦
〈∅, 𝑦〉) |
| 17 | 15, 16 | fvmptg 7014 |
. . . . . 6
⊢
(((2nd ‘𝐶) ∈ V ∧ 〈∅,
(2nd ‘𝐶)〉 ∈ V) →
(inl‘(2nd ‘𝐶)) = 〈∅, (2nd
‘𝐶)〉) |
| 18 | 13, 14, 17 | sylancl 586 |
. . . . 5
⊢ (𝐶 ∈ ({∅} × 𝐴) →
(inl‘(2nd ‘𝐶)) = 〈∅, (2nd
‘𝐶)〉) |
| 19 | 12, 18 | eqtr4d 2780 |
. . . 4
⊢ (𝐶 ∈ ({∅} × 𝐴) → 𝐶 = (inl‘(2nd ‘𝐶))) |
| 20 | | fveq2 6906 |
. . . . 5
⊢ (𝑥 = (2nd ‘𝐶) → (inl‘𝑥) = (inl‘(2nd
‘𝐶))) |
| 21 | 20 | rspceeqv 3645 |
. . . 4
⊢
(((2nd ‘𝐶) ∈ 𝐴 ∧ 𝐶 = (inl‘(2nd ‘𝐶))) → ∃𝑥 ∈ 𝐴 𝐶 = (inl‘𝑥)) |
| 22 | 5, 19, 21 | syl2anc 584 |
. . 3
⊢ (𝐶 ∈ ({∅} × 𝐴) → ∃𝑥 ∈ 𝐴 𝐶 = (inl‘𝑥)) |
| 23 | | xp2nd 8047 |
. . . 4
⊢ (𝐶 ∈ ({1o} ×
𝐵) → (2nd
‘𝐶) ∈ 𝐵) |
| 24 | | 1st2nd2 8053 |
. . . . . 6
⊢ (𝐶 ∈ ({1o} ×
𝐵) → 𝐶 = 〈(1st ‘𝐶), (2nd ‘𝐶)〉) |
| 25 | | xp1st 8046 |
. . . . . . 7
⊢ (𝐶 ∈ ({1o} ×
𝐵) → (1st
‘𝐶) ∈
{1o}) |
| 26 | | elsni 4643 |
. . . . . . 7
⊢
((1st ‘𝐶) ∈ {1o} →
(1st ‘𝐶) =
1o) |
| 27 | | opeq1 4873 |
. . . . . . . 8
⊢
((1st ‘𝐶) = 1o →
〈(1st ‘𝐶), (2nd ‘𝐶)〉 = 〈1o,
(2nd ‘𝐶)〉) |
| 28 | 27 | eqeq2d 2748 |
. . . . . . 7
⊢
((1st ‘𝐶) = 1o → (𝐶 = 〈(1st ‘𝐶), (2nd ‘𝐶)〉 ↔ 𝐶 = 〈1o, (2nd
‘𝐶)〉)) |
| 29 | 25, 26, 28 | 3syl 18 |
. . . . . 6
⊢ (𝐶 ∈ ({1o} ×
𝐵) → (𝐶 = 〈(1st
‘𝐶), (2nd
‘𝐶)〉 ↔
𝐶 = 〈1o,
(2nd ‘𝐶)〉)) |
| 30 | 24, 29 | mpbid 232 |
. . . . 5
⊢ (𝐶 ∈ ({1o} ×
𝐵) → 𝐶 = 〈1o, (2nd
‘𝐶)〉) |
| 31 | | fvexd 6921 |
. . . . . 6
⊢ (𝐶 ∈ ({1o} ×
𝐵) → (2nd
‘𝐶) ∈
V) |
| 32 | | opex 5469 |
. . . . . 6
⊢
〈1o, (2nd ‘𝐶)〉 ∈ V |
| 33 | | opeq2 4874 |
. . . . . . 7
⊢ (𝑧 = (2nd ‘𝐶) → 〈1o,
𝑧〉 =
〈1o, (2nd ‘𝐶)〉) |
| 34 | | df-inr 9943 |
. . . . . . 7
⊢ inr =
(𝑧 ∈ V ↦
〈1o, 𝑧〉) |
| 35 | 33, 34 | fvmptg 7014 |
. . . . . 6
⊢
(((2nd ‘𝐶) ∈ V ∧ 〈1o,
(2nd ‘𝐶)〉 ∈ V) →
(inr‘(2nd ‘𝐶)) = 〈1o, (2nd
‘𝐶)〉) |
| 36 | 31, 32, 35 | sylancl 586 |
. . . . 5
⊢ (𝐶 ∈ ({1o} ×
𝐵) →
(inr‘(2nd ‘𝐶)) = 〈1o, (2nd
‘𝐶)〉) |
| 37 | 30, 36 | eqtr4d 2780 |
. . . 4
⊢ (𝐶 ∈ ({1o} ×
𝐵) → 𝐶 = (inr‘(2nd ‘𝐶))) |
| 38 | | fveq2 6906 |
. . . . 5
⊢ (𝑥 = (2nd ‘𝐶) → (inr‘𝑥) = (inr‘(2nd
‘𝐶))) |
| 39 | 38 | rspceeqv 3645 |
. . . 4
⊢
(((2nd ‘𝐶) ∈ 𝐵 ∧ 𝐶 = (inr‘(2nd ‘𝐶))) → ∃𝑥 ∈ 𝐵 𝐶 = (inr‘𝑥)) |
| 40 | 23, 37, 39 | syl2anc 584 |
. . 3
⊢ (𝐶 ∈ ({1o} ×
𝐵) → ∃𝑥 ∈ 𝐵 𝐶 = (inr‘𝑥)) |
| 41 | 22, 40 | orim12i 909 |
. 2
⊢ ((𝐶 ∈ ({∅} × 𝐴) ∨ 𝐶 ∈ ({1o} × 𝐵)) → (∃𝑥 ∈ 𝐴 𝐶 = (inl‘𝑥) ∨ ∃𝑥 ∈ 𝐵 𝐶 = (inr‘𝑥))) |
| 42 | 4, 41 | syl 17 |
1
⊢ (𝐶 ∈ (𝐴 ⊔ 𝐵) → (∃𝑥 ∈ 𝐴 𝐶 = (inl‘𝑥) ∨ ∃𝑥 ∈ 𝐵 𝐶 = (inr‘𝑥))) |