Step | Hyp | Ref
| Expression |
1 | | snex 4111 |
. . . . 5
⊢ {B} ∈
V |
2 | | eqpw1relk.1 |
. . . . . 6
⊢ A ∈
V |
3 | 2, 1 | opkelxpk 4248 |
. . . . 5
⊢ (⟪A, {B}⟫
∈ (℘1c ×k
V) ↔ (A ∈ ℘1c ∧ {B} ∈ V)) |
4 | 1, 3 | mpbiran2 885 |
. . . 4
⊢ (⟪A, {B}⟫
∈ (℘1c ×k
V) ↔ A ∈ ℘1c) |
5 | 2 | elpw 3728 |
. . . 4
⊢ (A ∈ ℘1c ↔ A ⊆
1c) |
6 | 4, 5 | bitri 240 |
. . 3
⊢ (⟪A, {B}⟫
∈ (℘1c ×k
V) ↔ A ⊆ 1c) |
7 | | opkex 4113 |
. . . . . . 7
⊢ ⟪A, {B}⟫
∈ V |
8 | 7 | elimak 4259 |
. . . . . 6
⊢ (⟪A, {B}⟫
∈ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c) ↔ ∃t ∈ ℘1
℘1℘11c⟪t, ⟪A,
{B}⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k SIk Sk )) |
9 | | elpw131c 4149 |
. . . . . . . . . 10
⊢ (t ∈ ℘1℘1℘11c ↔ ∃x t = {{{{x}}}}) |
10 | 9 | anbi1i 676 |
. . . . . . . . 9
⊢ ((t ∈ ℘1℘1℘11c ∧ ⟪t,
⟪A, {B}⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k SIk Sk )) ↔ (∃x t = {{{{x}}}}
∧ ⟪t, ⟪A,
{B}⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k SIk Sk ))) |
11 | | 19.41v 1901 |
. . . . . . . . 9
⊢ (∃x(t = {{{{x}}}}
∧ ⟪t, ⟪A,
{B}⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k SIk Sk )) ↔ (∃x t = {{{{x}}}}
∧ ⟪t, ⟪A,
{B}⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k SIk Sk ))) |
12 | 10, 11 | bitr4i 243 |
. . . . . . . 8
⊢ ((t ∈ ℘1℘1℘11c ∧ ⟪t,
⟪A, {B}⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k SIk Sk )) ↔ ∃x(t = {{{{x}}}}
∧ ⟪t, ⟪A,
{B}⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k SIk Sk ))) |
13 | 12 | exbii 1582 |
. . . . . . 7
⊢ (∃t(t ∈ ℘1℘1℘11c ∧ ⟪t,
⟪A, {B}⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k SIk Sk )) ↔ ∃t∃x(t = {{{{x}}}}
∧ ⟪t, ⟪A,
{B}⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k SIk Sk ))) |
14 | | df-rex 2620 |
. . . . . . 7
⊢ (∃t ∈ ℘1
℘1℘11c⟪t, ⟪A,
{B}⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k SIk Sk ) ↔ ∃t(t ∈ ℘1℘1℘11c ∧ ⟪t,
⟪A, {B}⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k SIk Sk ))) |
15 | | excom 1741 |
. . . . . . 7
⊢ (∃x∃t(t = {{{{x}}}}
∧ ⟪t, ⟪A,
{B}⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k SIk Sk )) ↔ ∃t∃x(t = {{{{x}}}}
∧ ⟪t, ⟪A,
{B}⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k SIk Sk ))) |
16 | 13, 14, 15 | 3bitr4i 268 |
. . . . . 6
⊢ (∃t ∈ ℘1
℘1℘11c⟪t, ⟪A,
{B}⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k SIk Sk ) ↔ ∃x∃t(t = {{{{x}}}}
∧ ⟪t, ⟪A,
{B}⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k SIk Sk ))) |
17 | 8, 16 | bitri 240 |
. . . . 5
⊢ (⟪A, {B}⟫
∈ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c) ↔ ∃x∃t(t = {{{{x}}}}
∧ ⟪t, ⟪A,
{B}⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k SIk Sk ))) |
18 | | snex 4111 |
. . . . . . . 8
⊢ {{{{x}}}} ∈
V |
19 | | opkeq1 4059 |
. . . . . . . . 9
⊢ (t = {{{{x}}}}
→ ⟪t, ⟪A, {B}⟫⟫ = ⟪{{{{x}}}}, ⟪A, {B}⟫⟫) |
20 | 19 | eleq1d 2419 |
. . . . . . . 8
⊢ (t = {{{{x}}}}
→ (⟪t, ⟪A, {B}⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k SIk Sk ) ↔ ⟪{{{{x}}}}, ⟪A, {B}⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k SIk Sk ))) |
21 | 18, 20 | ceqsexv 2894 |
. . . . . . 7
⊢ (∃t(t = {{{{x}}}}
∧ ⟪t, ⟪A,
{B}⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k SIk Sk )) ↔ ⟪{{{{x}}}}, ⟪A, {B}⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k SIk Sk )) |
22 | | elsymdif 3223 |
. . . . . . . 8
⊢
(⟪{{{{x}}}}, ⟪A, {B}⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k SIk Sk ) ↔ ¬
(⟪{{{{x}}}}, ⟪A, {B}⟫⟫ ∈ Ins3k Sk ↔ ⟪{{{{x}}}}, ⟪A, {B}⟫⟫ ∈ Ins2k SIk Sk )) |
23 | | snex 4111 |
. . . . . . . . . . 11
⊢ {{x}} ∈
V |
24 | 23, 2, 1 | otkelins3k 4256 |
. . . . . . . . . 10
⊢
(⟪{{{{x}}}}, ⟪A, {B}⟫⟫ ∈ Ins3k Sk ↔ ⟪{{x}}, A⟫
∈ Sk ) |
25 | | snex 4111 |
. . . . . . . . . . 11
⊢ {x} ∈
V |
26 | 25, 2 | elssetk 4270 |
. . . . . . . . . 10
⊢ (⟪{{x}}, A⟫
∈ Sk ↔ {x} ∈ A) |
27 | 24, 26 | bitri 240 |
. . . . . . . . 9
⊢
(⟪{{{{x}}}}, ⟪A, {B}⟫⟫ ∈ Ins3k Sk ↔ {x} ∈ A) |
28 | 23, 2, 1 | otkelins2k 4255 |
. . . . . . . . . 10
⊢
(⟪{{{{x}}}}, ⟪A, {B}⟫⟫ ∈ Ins2k SIk Sk ↔ ⟪{{x}}, {B}⟫
∈ SIk Sk ) |
29 | | eqpw1relk.2 |
. . . . . . . . . . . 12
⊢ B ∈
V |
30 | 25, 29 | opksnelsik 4265 |
. . . . . . . . . . 11
⊢ (⟪{{x}}, {B}⟫
∈ SIk Sk ↔ ⟪{x}, B⟫
∈ Sk ) |
31 | | vex 2862 |
. . . . . . . . . . . 12
⊢ x ∈
V |
32 | 31, 29 | elssetk 4270 |
. . . . . . . . . . 11
⊢ (⟪{x}, B⟫
∈ Sk ↔ x ∈ B) |
33 | 30, 32 | bitri 240 |
. . . . . . . . . 10
⊢ (⟪{{x}}, {B}⟫
∈ SIk Sk ↔ x ∈ B) |
34 | 28, 33 | bitri 240 |
. . . . . . . . 9
⊢
(⟪{{{{x}}}}, ⟪A, {B}⟫⟫ ∈ Ins2k SIk Sk ↔ x ∈ B) |
35 | 27, 34 | bibi12i 306 |
. . . . . . . 8
⊢
((⟪{{{{x}}}},
⟪A, {B}⟫⟫ ∈ Ins3k Sk ↔ ⟪{{{{x}}}}, ⟪A, {B}⟫⟫ ∈ Ins2k SIk Sk ) ↔ ({x} ∈ A ↔ x ∈ B)) |
36 | 22, 35 | xchbinx 301 |
. . . . . . 7
⊢
(⟪{{{{x}}}}, ⟪A, {B}⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k SIk Sk ) ↔ ¬ ({x} ∈ A ↔ x ∈ B)) |
37 | 21, 36 | bitri 240 |
. . . . . 6
⊢ (∃t(t = {{{{x}}}}
∧ ⟪t, ⟪A,
{B}⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k SIk Sk )) ↔ ¬ ({x} ∈ A ↔ x ∈ B)) |
38 | 37 | exbii 1582 |
. . . . 5
⊢ (∃x∃t(t = {{{{x}}}}
∧ ⟪t, ⟪A,
{B}⟫⟫ ∈ ( Ins3k Sk ⊕ Ins2k SIk Sk )) ↔ ∃x ¬
({x} ∈
A ↔ x ∈ B)) |
39 | | exnal 1574 |
. . . . 5
⊢ (∃x ¬
({x} ∈
A ↔ x ∈ B) ↔ ¬ ∀x({x} ∈ A ↔ x ∈ B)) |
40 | 17, 38, 39 | 3bitrri 263 |
. . . 4
⊢ (¬ ∀x({x} ∈ A ↔ x ∈ B) ↔
⟪A, {B}⟫ ∈ ((
Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) |
41 | 40 | con1bii 321 |
. . 3
⊢ (¬
⟪A, {B}⟫ ∈ ((
Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c) ↔ ∀x({x} ∈ A ↔ x ∈ B)) |
42 | 6, 41 | anbi12i 678 |
. 2
⊢ ((⟪A, {B}⟫
∈ (℘1c ×k
V) ∧ ¬ ⟪A, {B}⟫
∈ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ↔
(A ⊆
1c ∧ ∀x({x} ∈ A ↔ x ∈ B))) |
43 | | eldif 3221 |
. 2
⊢ (⟪A, {B}⟫
∈ ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ↔
(⟪A, {B}⟫ ∈
(℘1c
×k V) ∧ ¬
⟪A, {B}⟫ ∈ ((
Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c))) |
44 | | eqpw1 4162 |
. 2
⊢ (A = ℘1B ↔ (A
⊆ 1c ∧ ∀x({x} ∈ A ↔
x ∈
B))) |
45 | 42, 43, 44 | 3bitr4i 268 |
1
⊢ (⟪A, {B}⟫
∈ ((℘1c ×k
V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ↔
A = ℘1B) |