Step | Hyp | Ref
| Expression |
1 | | djur 7008 |
. . 3
⊢ (𝑥 ∈ (𝐴 ⊔ 𝐵) ↔ (∃𝑦 ∈ 𝐴 𝑥 = (inl‘𝑦) ∨ ∃𝑦 ∈ 𝐵 𝑥 = (inr‘𝑦))) |
2 | | simpr 109 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑥 = (inl‘𝑦)) → 𝑥 = (inl‘𝑦)) |
3 | | df-inl 6986 |
. . . . . . . . 9
⊢ inl =
(𝑥 ∈ V ↦
〈∅, 𝑥〉) |
4 | | opeq2 3742 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → 〈∅, 𝑥〉 = 〈∅, 𝑦〉) |
5 | | elex 2723 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐴 → 𝑦 ∈ V) |
6 | | 0ex 4091 |
. . . . . . . . . . 11
⊢ ∅
∈ V |
7 | | vex 2715 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
8 | 6, 7 | opex 4189 |
. . . . . . . . . 10
⊢
〈∅, 𝑦〉 ∈ V |
9 | 8 | a1i 9 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐴 → 〈∅, 𝑦〉 ∈ V) |
10 | 3, 4, 5, 9 | fvmptd3 5560 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐴 → (inl‘𝑦) = 〈∅, 𝑦〉) |
11 | 10 | adantr 274 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑥 = (inl‘𝑦)) → (inl‘𝑦) = 〈∅, 𝑦〉) |
12 | 2, 11 | eqtrd 2190 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑥 = (inl‘𝑦)) → 𝑥 = 〈∅, 𝑦〉) |
13 | | elun1 3274 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐴 → 𝑦 ∈ (𝐴 ∪ 𝐵)) |
14 | 6 | prid1 3665 |
. . . . . . . . 9
⊢ ∅
∈ {∅, 1o} |
15 | 13, 14 | jctil 310 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐴 → (∅ ∈ {∅,
1o} ∧ 𝑦
∈ (𝐴 ∪ 𝐵))) |
16 | 15 | adantr 274 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑥 = (inl‘𝑦)) → (∅ ∈ {∅,
1o} ∧ 𝑦
∈ (𝐴 ∪ 𝐵))) |
17 | | opelxp 4615 |
. . . . . . 7
⊢
(〈∅, 𝑦〉 ∈ ({∅, 1o}
× (𝐴 ∪ 𝐵)) ↔ (∅ ∈
{∅, 1o} ∧ 𝑦 ∈ (𝐴 ∪ 𝐵))) |
18 | 16, 17 | sylibr 133 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑥 = (inl‘𝑦)) → 〈∅, 𝑦〉 ∈ ({∅, 1o}
× (𝐴 ∪ 𝐵))) |
19 | 12, 18 | eqeltrd 2234 |
. . . . 5
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑥 = (inl‘𝑦)) → 𝑥 ∈ ({∅, 1o} ×
(𝐴 ∪ 𝐵))) |
20 | 19 | rexlimiva 2569 |
. . . 4
⊢
(∃𝑦 ∈
𝐴 𝑥 = (inl‘𝑦) → 𝑥 ∈ ({∅, 1o} ×
(𝐴 ∪ 𝐵))) |
21 | | simpr 109 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑥 = (inr‘𝑦)) → 𝑥 = (inr‘𝑦)) |
22 | | df-inr 6987 |
. . . . . . . . 9
⊢ inr =
(𝑥 ∈ V ↦
〈1o, 𝑥〉) |
23 | | opeq2 3742 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → 〈1o, 𝑥〉 = 〈1o,
𝑦〉) |
24 | | elex 2723 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ V) |
25 | | 1oex 6368 |
. . . . . . . . . . 11
⊢
1o ∈ V |
26 | 25, 7 | opex 4189 |
. . . . . . . . . 10
⊢
〈1o, 𝑦〉 ∈ V |
27 | 26 | a1i 9 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐵 → 〈1o, 𝑦〉 ∈
V) |
28 | 22, 23, 24, 27 | fvmptd3 5560 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 → (inr‘𝑦) = 〈1o, 𝑦〉) |
29 | 28 | adantr 274 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑥 = (inr‘𝑦)) → (inr‘𝑦) = 〈1o, 𝑦〉) |
30 | 21, 29 | eqtrd 2190 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑥 = (inr‘𝑦)) → 𝑥 = 〈1o, 𝑦〉) |
31 | | elun2 3275 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ (𝐴 ∪ 𝐵)) |
32 | 31 | adantr 274 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑥 = (inr‘𝑦)) → 𝑦 ∈ (𝐴 ∪ 𝐵)) |
33 | 25 | prid2 3666 |
. . . . . . . 8
⊢
1o ∈ {∅, 1o} |
34 | 32, 33 | jctil 310 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑥 = (inr‘𝑦)) → (1o ∈ {∅,
1o} ∧ 𝑦
∈ (𝐴 ∪ 𝐵))) |
35 | | opelxp 4615 |
. . . . . . 7
⊢
(〈1o, 𝑦〉 ∈ ({∅, 1o}
× (𝐴 ∪ 𝐵)) ↔ (1o ∈
{∅, 1o} ∧ 𝑦 ∈ (𝐴 ∪ 𝐵))) |
36 | 34, 35 | sylibr 133 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑥 = (inr‘𝑦)) → 〈1o, 𝑦〉 ∈ ({∅,
1o} × (𝐴
∪ 𝐵))) |
37 | 30, 36 | eqeltrd 2234 |
. . . . 5
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑥 = (inr‘𝑦)) → 𝑥 ∈ ({∅, 1o} ×
(𝐴 ∪ 𝐵))) |
38 | 37 | rexlimiva 2569 |
. . . 4
⊢
(∃𝑦 ∈
𝐵 𝑥 = (inr‘𝑦) → 𝑥 ∈ ({∅, 1o} ×
(𝐴 ∪ 𝐵))) |
39 | 20, 38 | jaoi 706 |
. . 3
⊢
((∃𝑦 ∈
𝐴 𝑥 = (inl‘𝑦) ∨ ∃𝑦 ∈ 𝐵 𝑥 = (inr‘𝑦)) → 𝑥 ∈ ({∅, 1o} ×
(𝐴 ∪ 𝐵))) |
40 | 1, 39 | sylbi 120 |
. 2
⊢ (𝑥 ∈ (𝐴 ⊔ 𝐵) → 𝑥 ∈ ({∅, 1o} ×
(𝐴 ∪ 𝐵))) |
41 | 40 | ssriv 3132 |
1
⊢ (𝐴 ⊔ 𝐵) ⊆ ({∅, 1o} ×
(𝐴 ∪ 𝐵)) |