| Step | Hyp | Ref
| Expression |
| 1 | | djur 9959 |
. . 3
⊢ (𝑥 ∈ (𝐴 ⊔ 𝐵) → (∃𝑦 ∈ 𝐴 𝑥 = (inl‘𝑦) ∨ ∃𝑦 ∈ 𝐵 𝑥 = (inr‘𝑦))) |
| 2 | | simpr 484 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑥 = (inl‘𝑦)) → 𝑥 = (inl‘𝑦)) |
| 3 | | df-inl 9942 |
. . . . . . . . 9
⊢ inl =
(𝑥 ∈ V ↦
〈∅, 𝑥〉) |
| 4 | | opeq2 4874 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → 〈∅, 𝑥〉 = 〈∅, 𝑦〉) |
| 5 | | elex 3501 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐴 → 𝑦 ∈ V) |
| 6 | | opex 5469 |
. . . . . . . . . 10
⊢
〈∅, 𝑦〉 ∈ V |
| 7 | 6 | a1i 11 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐴 → 〈∅, 𝑦〉 ∈ V) |
| 8 | 3, 4, 5, 7 | fvmptd3 7039 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐴 → (inl‘𝑦) = 〈∅, 𝑦〉) |
| 9 | 8 | adantr 480 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑥 = (inl‘𝑦)) → (inl‘𝑦) = 〈∅, 𝑦〉) |
| 10 | 2, 9 | eqtrd 2777 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑥 = (inl‘𝑦)) → 𝑥 = 〈∅, 𝑦〉) |
| 11 | | elun1 4182 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐴 → 𝑦 ∈ (𝐴 ∪ 𝐵)) |
| 12 | | 0ex 5307 |
. . . . . . . . . 10
⊢ ∅
∈ V |
| 13 | 12 | prid1 4762 |
. . . . . . . . 9
⊢ ∅
∈ {∅, 1o} |
| 14 | 11, 13 | jctil 519 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐴 → (∅ ∈ {∅,
1o} ∧ 𝑦
∈ (𝐴 ∪ 𝐵))) |
| 15 | 14 | adantr 480 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑥 = (inl‘𝑦)) → (∅ ∈ {∅,
1o} ∧ 𝑦
∈ (𝐴 ∪ 𝐵))) |
| 16 | | opelxp 5721 |
. . . . . . 7
⊢
(〈∅, 𝑦〉 ∈ ({∅, 1o}
× (𝐴 ∪ 𝐵)) ↔ (∅ ∈
{∅, 1o} ∧ 𝑦 ∈ (𝐴 ∪ 𝐵))) |
| 17 | 15, 16 | sylibr 234 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑥 = (inl‘𝑦)) → 〈∅, 𝑦〉 ∈ ({∅, 1o}
× (𝐴 ∪ 𝐵))) |
| 18 | 10, 17 | eqeltrd 2841 |
. . . . 5
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑥 = (inl‘𝑦)) → 𝑥 ∈ ({∅, 1o} ×
(𝐴 ∪ 𝐵))) |
| 19 | 18 | rexlimiva 3147 |
. . . 4
⊢
(∃𝑦 ∈
𝐴 𝑥 = (inl‘𝑦) → 𝑥 ∈ ({∅, 1o} ×
(𝐴 ∪ 𝐵))) |
| 20 | | simpr 484 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑥 = (inr‘𝑦)) → 𝑥 = (inr‘𝑦)) |
| 21 | | df-inr 9943 |
. . . . . . . . 9
⊢ inr =
(𝑥 ∈ V ↦
〈1o, 𝑥〉) |
| 22 | | opeq2 4874 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → 〈1o, 𝑥〉 = 〈1o,
𝑦〉) |
| 23 | | elex 3501 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ V) |
| 24 | | opex 5469 |
. . . . . . . . . 10
⊢
〈1o, 𝑦〉 ∈ V |
| 25 | 24 | a1i 11 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐵 → 〈1o, 𝑦〉 ∈
V) |
| 26 | 21, 22, 23, 25 | fvmptd3 7039 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 → (inr‘𝑦) = 〈1o, 𝑦〉) |
| 27 | 26 | adantr 480 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑥 = (inr‘𝑦)) → (inr‘𝑦) = 〈1o, 𝑦〉) |
| 28 | 20, 27 | eqtrd 2777 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑥 = (inr‘𝑦)) → 𝑥 = 〈1o, 𝑦〉) |
| 29 | | elun2 4183 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ (𝐴 ∪ 𝐵)) |
| 30 | 29 | adantr 480 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑥 = (inr‘𝑦)) → 𝑦 ∈ (𝐴 ∪ 𝐵)) |
| 31 | | 1oex 8516 |
. . . . . . . . 9
⊢
1o ∈ V |
| 32 | 31 | prid2 4763 |
. . . . . . . 8
⊢
1o ∈ {∅, 1o} |
| 33 | 30, 32 | jctil 519 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑥 = (inr‘𝑦)) → (1o ∈ {∅,
1o} ∧ 𝑦
∈ (𝐴 ∪ 𝐵))) |
| 34 | | opelxp 5721 |
. . . . . . 7
⊢
(〈1o, 𝑦〉 ∈ ({∅, 1o}
× (𝐴 ∪ 𝐵)) ↔ (1o ∈
{∅, 1o} ∧ 𝑦 ∈ (𝐴 ∪ 𝐵))) |
| 35 | 33, 34 | sylibr 234 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑥 = (inr‘𝑦)) → 〈1o, 𝑦〉 ∈ ({∅,
1o} × (𝐴
∪ 𝐵))) |
| 36 | 28, 35 | eqeltrd 2841 |
. . . . 5
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑥 = (inr‘𝑦)) → 𝑥 ∈ ({∅, 1o} ×
(𝐴 ∪ 𝐵))) |
| 37 | 36 | rexlimiva 3147 |
. . . 4
⊢
(∃𝑦 ∈
𝐵 𝑥 = (inr‘𝑦) → 𝑥 ∈ ({∅, 1o} ×
(𝐴 ∪ 𝐵))) |
| 38 | 19, 37 | jaoi 858 |
. . 3
⊢
((∃𝑦 ∈
𝐴 𝑥 = (inl‘𝑦) ∨ ∃𝑦 ∈ 𝐵 𝑥 = (inr‘𝑦)) → 𝑥 ∈ ({∅, 1o} ×
(𝐴 ∪ 𝐵))) |
| 39 | 1, 38 | syl 17 |
. 2
⊢ (𝑥 ∈ (𝐴 ⊔ 𝐵) → 𝑥 ∈ ({∅, 1o} ×
(𝐴 ∪ 𝐵))) |
| 40 | 39 | ssriv 3987 |
1
⊢ (𝐴 ⊔ 𝐵) ⊆ ({∅, 1o} ×
(𝐴 ∪ 𝐵)) |