Step | Hyp | Ref
| Expression |
1 | | df-qs 5951 |
. . 3
⊢ (A / R) =
{x ∣
∃y ∈ A x = [y]R} |
2 | | elimapw1 4944 |
. . . . 5
⊢ (x ∈ ( ∼ ((
Ins2 S ⊕
Ins3 SI ◡R)
“ 1c) “ ℘1A) ↔ ∃y ∈ A 〈{y}, x〉 ∈ ∼ (( Ins2 S ⊕ Ins3 SI ◡R) “ 1c)) |
3 | | elima1c 4947 |
. . . . . . . . . 10
⊢ (〈{y}, x〉 ∈ (( Ins2 S ⊕ Ins3 SI ◡R) “ 1c) ↔ ∃z〈{z}, 〈{y}, x〉〉 ∈ ( Ins2 S ⊕ Ins3 SI ◡R)) |
4 | | elsymdif 3223 |
. . . . . . . . . . . 12
⊢ (〈{z}, 〈{y}, x〉〉 ∈ ( Ins2 S ⊕ Ins3 SI ◡R)
↔ ¬ (〈{z}, 〈{y}, x〉〉 ∈ Ins2 S ↔ 〈{z}, 〈{y}, x〉〉 ∈ Ins3 SI ◡R)) |
5 | | snex 4111 |
. . . . . . . . . . . . . . . 16
⊢ {y} ∈
V |
6 | 5 | otelins2 5791 |
. . . . . . . . . . . . . . 15
⊢ (〈{z}, 〈{y}, x〉〉 ∈ Ins2 S ↔ 〈{z}, x〉 ∈ S
) |
7 | | vex 2862 |
. . . . . . . . . . . . . . . 16
⊢ z ∈
V |
8 | | vex 2862 |
. . . . . . . . . . . . . . . 16
⊢ x ∈
V |
9 | 7, 8 | opelssetsn 4760 |
. . . . . . . . . . . . . . 15
⊢ (〈{z}, x〉 ∈ S ↔ z ∈ x) |
10 | 6, 9 | bitri 240 |
. . . . . . . . . . . . . 14
⊢ (〈{z}, 〈{y}, x〉〉 ∈ Ins2 S ↔ z ∈ x) |
11 | 8 | otelins3 5792 |
. . . . . . . . . . . . . . 15
⊢ (〈{z}, 〈{y}, x〉〉 ∈ Ins3 SI ◡R ↔
〈{z},
{y}〉
∈ SI ◡R) |
12 | | df-br 4640 |
. . . . . . . . . . . . . . . . 17
⊢ (z◡Ry ↔ 〈z, y〉 ∈ ◡R) |
13 | | brcnv 4892 |
. . . . . . . . . . . . . . . . 17
⊢ (z◡Ry ↔
yRz) |
14 | 12, 13 | bitr3i 242 |
. . . . . . . . . . . . . . . 16
⊢ (〈z, y〉 ∈ ◡R ↔ yRz) |
15 | | vex 2862 |
. . . . . . . . . . . . . . . . 17
⊢ y ∈
V |
16 | 7, 15 | opsnelsi 5774 |
. . . . . . . . . . . . . . . 16
⊢ (〈{z}, {y}〉 ∈ SI ◡R ↔
〈z,
y〉 ∈ ◡R) |
17 | | elec 5964 |
. . . . . . . . . . . . . . . 16
⊢ (z ∈ [y]R ↔
yRz) |
18 | 14, 16, 17 | 3bitr4i 268 |
. . . . . . . . . . . . . . 15
⊢ (〈{z}, {y}〉 ∈ SI ◡R ↔
z ∈
[y]R) |
19 | 11, 18 | bitri 240 |
. . . . . . . . . . . . . 14
⊢ (〈{z}, 〈{y}, x〉〉 ∈ Ins3 SI ◡R ↔
z ∈
[y]R) |
20 | 10, 19 | bibi12i 306 |
. . . . . . . . . . . . 13
⊢ ((〈{z}, 〈{y}, x〉〉 ∈ Ins2 S ↔ 〈{z}, 〈{y}, x〉〉 ∈ Ins3 SI ◡R)
↔ (z ∈ x ↔
z ∈
[y]R)) |
21 | 20 | notbii 287 |
. . . . . . . . . . . 12
⊢ (¬ (〈{z}, 〈{y}, x〉〉 ∈ Ins2 S ↔ 〈{z}, 〈{y}, x〉〉 ∈ Ins3 SI ◡R)
↔ ¬ (z ∈ x ↔
z ∈
[y]R)) |
22 | 4, 21 | bitri 240 |
. . . . . . . . . . 11
⊢ (〈{z}, 〈{y}, x〉〉 ∈ ( Ins2 S ⊕ Ins3 SI ◡R)
↔ ¬ (z ∈ x ↔
z ∈
[y]R)) |
23 | 22 | exbii 1582 |
. . . . . . . . . 10
⊢ (∃z〈{z}, 〈{y}, x〉〉 ∈ ( Ins2 S ⊕ Ins3 SI ◡R)
↔ ∃z ¬ (z ∈ x ↔
z ∈
[y]R)) |
24 | 3, 23 | bitri 240 |
. . . . . . . . 9
⊢ (〈{y}, x〉 ∈ (( Ins2 S ⊕ Ins3 SI ◡R) “ 1c) ↔ ∃z ¬
(z ∈
x ↔ z ∈ [y]R)) |
25 | 24 | notbii 287 |
. . . . . . . 8
⊢ (¬ 〈{y}, x〉 ∈ (( Ins2 S ⊕ Ins3 SI ◡R) “ 1c) ↔ ¬ ∃z ¬
(z ∈
x ↔ z ∈ [y]R)) |
26 | 5, 8 | opex 4588 |
. . . . . . . . 9
⊢ 〈{y}, x〉 ∈ V |
27 | 26 | elcompl 3225 |
. . . . . . . 8
⊢ (〈{y}, x〉 ∈ ∼ (( Ins2 S ⊕ Ins3 SI ◡R) “ 1c) ↔ ¬ 〈{y}, x〉 ∈ (( Ins2 S ⊕ Ins3 SI ◡R) “ 1c)) |
28 | | alex 1572 |
. . . . . . . 8
⊢ (∀z(z ∈ x ↔ z ∈ [y]R) ↔ ¬ ∃z ¬
(z ∈
x ↔ z ∈ [y]R)) |
29 | 25, 27, 28 | 3bitr4i 268 |
. . . . . . 7
⊢ (〈{y}, x〉 ∈ ∼ (( Ins2 S ⊕ Ins3 SI ◡R) “ 1c) ↔ ∀z(z ∈ x ↔ z ∈ [y]R)) |
30 | | dfcleq 2347 |
. . . . . . 7
⊢ (x = [y]R ↔ ∀z(z ∈ x ↔ z ∈ [y]R)) |
31 | 29, 30 | bitr4i 243 |
. . . . . 6
⊢ (〈{y}, x〉 ∈ ∼ (( Ins2 S ⊕ Ins3 SI ◡R) “ 1c) ↔ x = [y]R) |
32 | 31 | rexbii 2639 |
. . . . 5
⊢ (∃y ∈ A 〈{y}, x〉 ∈ ∼ (( Ins2 S ⊕ Ins3 SI ◡R) “ 1c) ↔ ∃y ∈ A x = [y]R) |
33 | 2, 32 | bitri 240 |
. . . 4
⊢ (x ∈ ( ∼ ((
Ins2 S ⊕
Ins3 SI ◡R)
“ 1c) “ ℘1A) ↔ ∃y ∈ A x = [y]R) |
34 | 33 | abbi2i 2464 |
. . 3
⊢ ( ∼ (( Ins2 S ⊕ Ins3 SI ◡R)
“ 1c) “ ℘1A) = {x ∣ ∃y ∈ A x = [y]R} |
35 | 1, 34 | eqtr4i 2376 |
. 2
⊢ (A / R) =
( ∼ (( Ins2 S
⊕ Ins3 SI
◡R) “ 1c) “ ℘1A) |
36 | | ssetex 4744 |
. . . . . . 7
⊢ S ∈
V |
37 | 36 | ins2ex 5797 |
. . . . . 6
⊢ Ins2 S ∈ V |
38 | | cnvexg 5101 |
. . . . . . 7
⊢ (R ∈ V → ◡R ∈ V) |
39 | | siexg 4752 |
. . . . . . 7
⊢ (◡R ∈ V → SI ◡R ∈ V) |
40 | | ins3exg 5796 |
. . . . . . 7
⊢ ( SI ◡R ∈ V → Ins3 SI ◡R ∈ V) |
41 | 38, 39, 40 | 3syl 18 |
. . . . . 6
⊢ (R ∈ V → Ins3 SI ◡R ∈
V) |
42 | | symdifexg 4103 |
. . . . . 6
⊢ (( Ins2 S ∈ V ∧ Ins3 SI ◡R ∈ V) → ( Ins2
S ⊕ Ins3
SI ◡R) ∈ V) |
43 | 37, 41, 42 | sylancr 644 |
. . . . 5
⊢ (R ∈ V → ( Ins2 S ⊕ Ins3 SI ◡R) ∈
V) |
44 | | 1cex 4142 |
. . . . 5
⊢
1c ∈
V |
45 | | imaexg 4746 |
. . . . 5
⊢ ((( Ins2 S ⊕ Ins3 SI ◡R) ∈ V ∧
1c ∈ V) → (( Ins2 S ⊕ Ins3 SI ◡R)
“ 1c) ∈
V) |
46 | 43, 44, 45 | sylancl 643 |
. . . 4
⊢ (R ∈ V → (( Ins2 S ⊕ Ins3 SI ◡R) “ 1c) ∈ V) |
47 | | complexg 4099 |
. . . 4
⊢ ((( Ins2 S ⊕ Ins3 SI ◡R)
“ 1c) ∈ V →
∼ (( Ins2 S
⊕ Ins3 SI
◡R) “ 1c) ∈ V) |
48 | 46, 47 | syl 15 |
. . 3
⊢ (R ∈ V → ∼ (( Ins2
S ⊕ Ins3
SI ◡R)
“ 1c) ∈
V) |
49 | | pw1exg 4302 |
. . 3
⊢ (A ∈ W → ℘1A ∈
V) |
50 | | imaexg 4746 |
. . 3
⊢ (( ∼ (( Ins2 S ⊕ Ins3 SI ◡R)
“ 1c) ∈ V ∧ ℘1A ∈ V) → (
∼ (( Ins2 S
⊕ Ins3 SI
◡R) “ 1c) “ ℘1A) ∈
V) |
51 | 48, 49, 50 | syl2an 463 |
. 2
⊢ ((R ∈ V ∧ A ∈ W) → ( ∼ (( Ins2 S ⊕ Ins3 SI ◡R)
“ 1c) “ ℘1A) ∈
V) |
52 | 35, 51 | syl5eqel 2437 |
1
⊢ ((R ∈ V ∧ A ∈ W) → (A
/ R) ∈ V) |