Proof of Theorem opkth1g
Step | Hyp | Ref
| Expression |
1 | | eqid 2353 |
. . . . 5
⊢ {C} = {C} |
2 | 1 | orci 379 |
. . . 4
⊢ ({C} = {C} ∨ {C} =
{C, D}) |
3 | | elopk 4129 |
. . . 4
⊢ ({C} ∈
⟪C, D⟫ ↔ ({C} = {C} ∨ {C} =
{C, D})) |
4 | 2, 3 | mpbir 200 |
. . 3
⊢ {C} ∈
⟪C, D⟫ |
5 | | eleq2 2414 |
. . . . 5
⊢ (⟪A, B⟫ =
⟪C, D⟫ → ({C} ∈
⟪A, B⟫ ↔ {C} ∈
⟪C, D⟫)) |
6 | 5 | biimprd 214 |
. . . 4
⊢ (⟪A, B⟫ =
⟪C, D⟫ → ({C} ∈
⟪C, D⟫ → {C} ∈
⟪A, B⟫)) |
7 | | elopk 4129 |
. . . . 5
⊢ ({C} ∈
⟪A, B⟫ ↔ ({C} = {A} ∨ {C} =
{A, B})) |
8 | | snidg 3758 |
. . . . . . 7
⊢ (A ∈ V → A ∈ {A}) |
9 | | eleq2 2414 |
. . . . . . 7
⊢ ({C} = {A} →
(A ∈
{C} ↔ A ∈ {A})) |
10 | 8, 9 | syl5ibrcom 213 |
. . . . . 6
⊢ (A ∈ V → ({C} =
{A} → A ∈ {C})) |
11 | | prid1g 3825 |
. . . . . . 7
⊢ (A ∈ V → A ∈ {A, B}) |
12 | | eleq2 2414 |
. . . . . . 7
⊢ ({C} = {A,
B} → (A ∈ {C} ↔ A
∈ {A,
B})) |
13 | 11, 12 | syl5ibrcom 213 |
. . . . . 6
⊢ (A ∈ V → ({C} =
{A, B}
→ A ∈ {C})) |
14 | 10, 13 | jaod 369 |
. . . . 5
⊢ (A ∈ V → (({C} =
{A} ∨
{C} = {A, B}) →
A ∈
{C})) |
15 | 7, 14 | syl5bi 208 |
. . . 4
⊢ (A ∈ V → ({C}
∈ ⟪A, B⟫
→ A ∈ {C})) |
16 | 6, 15 | sylan9r 639 |
. . 3
⊢ ((A ∈ V ∧
⟪A, B⟫ = ⟪C, D⟫)
→ ({C} ∈ ⟪C,
D⟫ → A ∈ {C})) |
17 | 4, 16 | mpi 16 |
. 2
⊢ ((A ∈ V ∧
⟪A, B⟫ = ⟪C, D⟫)
→ A ∈ {C}) |
18 | | elsncg 3755 |
. . 3
⊢ (A ∈ V → (A
∈ {C}
↔ A = C)) |
19 | 18 | adantr 451 |
. 2
⊢ ((A ∈ V ∧
⟪A, B⟫ = ⟪C, D⟫)
→ (A ∈ {C} ↔
A = C)) |
20 | 17, 19 | mpbid 201 |
1
⊢ ((A ∈ V ∧
⟪A, B⟫ = ⟪C, D⟫)
→ A = C) |