Step | Hyp | Ref
| Expression |
1 | | djulcl 7028 |
. 2
⊢ (𝐶 ∈ 𝐴 → (inl‘𝐶) ∈ (𝐴 ⊔ 𝐵)) |
2 | | 1n0 6411 |
. . . . . . . . . 10
⊢
1o ≠ ∅ |
3 | 2 | necomi 2425 |
. . . . . . . . 9
⊢ ∅
≠ 1o |
4 | | 0ex 4116 |
. . . . . . . . . 10
⊢ ∅
∈ V |
5 | 4 | elsn 3599 |
. . . . . . . . 9
⊢ (∅
∈ {1o} ↔ ∅ = 1o) |
6 | 3, 5 | nemtbir 2429 |
. . . . . . . 8
⊢ ¬
∅ ∈ {1o} |
7 | 6 | intnanr 925 |
. . . . . . 7
⊢ ¬
(∅ ∈ {1o} ∧ 𝐶 ∈ 𝐵) |
8 | | opelxp 4641 |
. . . . . . 7
⊢
(〈∅, 𝐶〉 ∈ ({1o} × 𝐵) ↔ (∅ ∈
{1o} ∧ 𝐶
∈ 𝐵)) |
9 | 7, 8 | mtbir 666 |
. . . . . 6
⊢ ¬
〈∅, 𝐶〉
∈ ({1o} × 𝐵) |
10 | | elex 2741 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ 𝑉 → 𝐶 ∈ V) |
11 | | opexg 4213 |
. . . . . . . . . . . . 13
⊢ ((∅
∈ V ∧ 𝐶 ∈
𝑉) → 〈∅,
𝐶〉 ∈
V) |
12 | 4, 11 | mpan 422 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ 𝑉 → 〈∅, 𝐶〉 ∈ V) |
13 | | opeq2 3766 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐶 → 〈∅, 𝑥〉 = 〈∅, 𝐶〉) |
14 | | df-inl 7024 |
. . . . . . . . . . . . 13
⊢ inl =
(𝑥 ∈ V ↦
〈∅, 𝑥〉) |
15 | 13, 14 | fvmptg 5572 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ V ∧ 〈∅,
𝐶〉 ∈ V) →
(inl‘𝐶) =
〈∅, 𝐶〉) |
16 | 10, 12, 15 | syl2anc 409 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ 𝑉 → (inl‘𝐶) = 〈∅, 𝐶〉) |
17 | 16 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ 𝑉 ∧ (inl‘𝐶) ∈ (𝐴 ⊔ 𝐵)) → (inl‘𝐶) = 〈∅, 𝐶〉) |
18 | | df-dju 7015 |
. . . . . . . . . . . . 13
⊢ (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵)) |
19 | 18 | eleq2i 2237 |
. . . . . . . . . . . 12
⊢
((inl‘𝐶)
∈ (𝐴 ⊔ 𝐵) ↔ (inl‘𝐶) ∈ (({∅} ×
𝐴) ∪ ({1o}
× 𝐵))) |
20 | 19 | biimpi 119 |
. . . . . . . . . . 11
⊢
((inl‘𝐶)
∈ (𝐴 ⊔ 𝐵) → (inl‘𝐶) ∈ (({∅} ×
𝐴) ∪ ({1o}
× 𝐵))) |
21 | 20 | adantl 275 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ 𝑉 ∧ (inl‘𝐶) ∈ (𝐴 ⊔ 𝐵)) → (inl‘𝐶) ∈ (({∅} × 𝐴) ∪ ({1o} ×
𝐵))) |
22 | 17, 21 | eqeltrrd 2248 |
. . . . . . . . 9
⊢ ((𝐶 ∈ 𝑉 ∧ (inl‘𝐶) ∈ (𝐴 ⊔ 𝐵)) → 〈∅, 𝐶〉 ∈ (({∅} × 𝐴) ∪ ({1o} ×
𝐵))) |
23 | | elun 3268 |
. . . . . . . . 9
⊢
(〈∅, 𝐶〉 ∈ (({∅} × 𝐴) ∪ ({1o} ×
𝐵)) ↔ (〈∅,
𝐶〉 ∈ ({∅}
× 𝐴) ∨
〈∅, 𝐶〉
∈ ({1o} × 𝐵))) |
24 | 22, 23 | sylib 121 |
. . . . . . . 8
⊢ ((𝐶 ∈ 𝑉 ∧ (inl‘𝐶) ∈ (𝐴 ⊔ 𝐵)) → (〈∅, 𝐶〉 ∈ ({∅} × 𝐴) ∨ 〈∅, 𝐶〉 ∈ ({1o}
× 𝐵))) |
25 | 24 | orcomd 724 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑉 ∧ (inl‘𝐶) ∈ (𝐴 ⊔ 𝐵)) → (〈∅, 𝐶〉 ∈ ({1o} × 𝐵) ∨ 〈∅, 𝐶〉 ∈ ({∅} ×
𝐴))) |
26 | 25 | ord 719 |
. . . . . 6
⊢ ((𝐶 ∈ 𝑉 ∧ (inl‘𝐶) ∈ (𝐴 ⊔ 𝐵)) → (¬ 〈∅, 𝐶〉 ∈ ({1o}
× 𝐵) →
〈∅, 𝐶〉
∈ ({∅} × 𝐴))) |
27 | 9, 26 | mpi 15 |
. . . . 5
⊢ ((𝐶 ∈ 𝑉 ∧ (inl‘𝐶) ∈ (𝐴 ⊔ 𝐵)) → 〈∅, 𝐶〉 ∈ ({∅} × 𝐴)) |
28 | | opelxp 4641 |
. . . . 5
⊢
(〈∅, 𝐶〉 ∈ ({∅} × 𝐴) ↔ (∅ ∈
{∅} ∧ 𝐶 ∈
𝐴)) |
29 | 27, 28 | sylib 121 |
. . . 4
⊢ ((𝐶 ∈ 𝑉 ∧ (inl‘𝐶) ∈ (𝐴 ⊔ 𝐵)) → (∅ ∈ {∅} ∧
𝐶 ∈ 𝐴)) |
30 | 29 | simprd 113 |
. . 3
⊢ ((𝐶 ∈ 𝑉 ∧ (inl‘𝐶) ∈ (𝐴 ⊔ 𝐵)) → 𝐶 ∈ 𝐴) |
31 | 30 | ex 114 |
. 2
⊢ (𝐶 ∈ 𝑉 → ((inl‘𝐶) ∈ (𝐴 ⊔ 𝐵) → 𝐶 ∈ 𝐴)) |
32 | 1, 31 | impbid2 142 |
1
⊢ (𝐶 ∈ 𝑉 → (𝐶 ∈ 𝐴 ↔ (inl‘𝐶) ∈ (𝐴 ⊔ 𝐵))) |