Step | Hyp | Ref
| Expression |
1 | | df-connex 5904 |
. . 3
⊢ Connex = {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a (xry ∨ yrx)} |
2 | | vex 2863 |
. . . . . . 7
⊢ r ∈
V |
3 | | vex 2863 |
. . . . . . 7
⊢ a ∈
V |
4 | 2, 3 | opex 4589 |
. . . . . 6
⊢ ⟨r, a⟩ ∈ V |
5 | 4 | elcompl 3226 |
. . . . 5
⊢ (⟨r, a⟩ ∈ ∼ (( Ins2 S ∩ (( Ins2 Ins2 S ∖ Ins4 ((( Ins4 SI3
Swap ∩ Ins2
Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c) ↔ ¬ ⟨r, a⟩ ∈ (( Ins2 S ∩ (( Ins2 Ins2 S ∖ Ins4 ((( Ins4 SI3
Swap ∩ Ins2
Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c)) |
6 | | elima1c 4948 |
. . . . . . . 8
⊢ (⟨r, a⟩ ∈ (( Ins2 S ∩ (( Ins2 Ins2 S ∖ Ins4 ((( Ins4 SI3
Swap ∩ Ins2
Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c) ↔ ∃x⟨{x}, ⟨r, a⟩⟩ ∈ ( Ins2 S ∩ (( Ins2 Ins2 S ∖ Ins4 ((( Ins4 SI3 Swap
∩ Ins2 Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) “
1c))) |
7 | | elin 3220 |
. . . . . . . . . 10
⊢ (⟨{x}, ⟨r, a⟩⟩ ∈ ( Ins2 S ∩ (( Ins2 Ins2 S ∖ Ins4 ((( Ins4 SI3 Swap
∩ Ins2 Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) ↔ (⟨{x}, ⟨r, a⟩⟩ ∈ Ins2 S ∧ ⟨{x}, ⟨r, a⟩⟩ ∈ (( Ins2 Ins2 S ∖ Ins4 ((( Ins4 SI3 Swap
∩ Ins2 Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) “
1c))) |
8 | 2 | otelins2 5792 |
. . . . . . . . . . . 12
⊢ (⟨{x}, ⟨r, a⟩⟩ ∈ Ins2 S ↔ ⟨{x}, a⟩ ∈ S
) |
9 | | vex 2863 |
. . . . . . . . . . . . 13
⊢ x ∈
V |
10 | 9, 3 | opelssetsn 4761 |
. . . . . . . . . . . 12
⊢ (⟨{x}, a⟩ ∈ S ↔ x ∈ a) |
11 | 8, 10 | bitri 240 |
. . . . . . . . . . 11
⊢ (⟨{x}, ⟨r, a⟩⟩ ∈ Ins2 S ↔ x ∈ a) |
12 | | elima1c 4948 |
. . . . . . . . . . . . 13
⊢ (⟨{x}, ⟨r, a⟩⟩ ∈ (( Ins2 Ins2 S ∖ Ins4 ((( Ins4 SI3 Swap
∩ Ins2 Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) “
1c) ↔ ∃y⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩ ∈ ( Ins2 Ins2 S ∖ Ins4 ((( Ins4 SI3 Swap
∩ Ins2 Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c)))) |
13 | | eldif 3222 |
. . . . . . . . . . . . . . 15
⊢ (⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩ ∈ ( Ins2 Ins2 S ∖ Ins4 ((( Ins4 SI3
Swap ∩ Ins2
Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) ↔ (⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩ ∈ Ins2 Ins2 S ∧ ¬ ⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩ ∈ Ins4 ((( Ins4 SI3 Swap
∩ Ins2 Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c)))) |
14 | | snex 4112 |
. . . . . . . . . . . . . . . . . 18
⊢ {x} ∈
V |
15 | 14 | otelins2 5792 |
. . . . . . . . . . . . . . . . 17
⊢ (⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩ ∈ Ins2 Ins2 S ↔ ⟨{y}, ⟨r, a⟩⟩ ∈ Ins2 S ) |
16 | 2 | otelins2 5792 |
. . . . . . . . . . . . . . . . 17
⊢ (⟨{y}, ⟨r, a⟩⟩ ∈ Ins2 S ↔ ⟨{y}, a⟩ ∈ S
) |
17 | | vex 2863 |
. . . . . . . . . . . . . . . . . 18
⊢ y ∈
V |
18 | 17, 3 | opelssetsn 4761 |
. . . . . . . . . . . . . . . . 17
⊢ (⟨{y}, a⟩ ∈ S ↔ y ∈ a) |
19 | 15, 16, 18 | 3bitri 262 |
. . . . . . . . . . . . . . . 16
⊢ (⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩ ∈ Ins2 Ins2 S ↔ y ∈ a) |
20 | 3 | oqelins4 5795 |
. . . . . . . . . . . . . . . . . 18
⊢ (⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩ ∈ Ins4 ((( Ins4 SI3
Swap ∩ Ins2
Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c)) ↔ ⟨{y}, ⟨{x}, r⟩⟩ ∈ ((( Ins4 SI3
Swap ∩ Ins2
Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) |
21 | | elun 3221 |
. . . . . . . . . . . . . . . . . 18
⊢ (⟨{y}, ⟨{x}, r⟩⟩ ∈ ((( Ins4 SI3
Swap ∩ Ins2
Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c)) ↔ (⟨{y}, ⟨{x}, r⟩⟩ ∈ (( Ins4 SI3
Swap ∩ Ins2
Ins2 S ) “
1c) ∨ ⟨{y}, ⟨{x}, r⟩⟩ ∈ (( Ins4 SI3
I ∩ Ins2 Ins2
S ) “
1c))) |
22 | | elin 3220 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (⟨{p}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ ( Ins4 SI3 Swap
∩ Ins2 Ins2 S ) ↔ (⟨{p}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ Ins4 SI3 Swap
∧ ⟨{p}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ Ins2 Ins2 S )) |
23 | 2 | oqelins4 5795 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (⟨{p}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ Ins4 SI3 Swap
↔ ⟨{p}, ⟨{y}, {x}⟩⟩ ∈ SI3 Swap
) |
24 | | vex 2863 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ p ∈
V |
25 | 24, 17, 9 | otsnelsi3 5806 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (⟨{p}, ⟨{y}, {x}⟩⟩ ∈ SI3 Swap
↔ ⟨p, ⟨y, x⟩⟩ ∈ Swap
) |
26 | | df-br 4641 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (p Swap ⟨y, x⟩ ↔ ⟨p, ⟨y, x⟩⟩ ∈ Swap ) |
27 | 17, 9 | brswap2 4861 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (p Swap ⟨y, x⟩ ↔ p = ⟨x, y⟩) |
28 | 26, 27 | bitr3i 242 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (⟨p, ⟨y, x⟩⟩ ∈ Swap ↔ p =
⟨x,
y⟩) |
29 | 23, 25, 28 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (⟨{p}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ Ins4 SI3 Swap
↔ p = ⟨x, y⟩) |
30 | | snex 4112 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ {y} ∈
V |
31 | 30 | otelins2 5792 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (⟨{p}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ Ins2 Ins2 S ↔ ⟨{p}, ⟨{x}, r⟩⟩ ∈ Ins2 S ) |
32 | 14 | otelins2 5792 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (⟨{p}, ⟨{x}, r⟩⟩ ∈ Ins2 S ↔ ⟨{p}, r⟩ ∈ S
) |
33 | 24, 2 | opelssetsn 4761 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (⟨{p}, r⟩ ∈ S ↔ p ∈ r) |
34 | 31, 32, 33 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (⟨{p}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ Ins2 Ins2 S ↔ p ∈ r) |
35 | 29, 34 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((⟨{p}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ Ins4 SI3 Swap
∧ ⟨{p}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ Ins2 Ins2 S ) ↔ (p = ⟨x, y⟩ ∧ p ∈ r)) |
36 | 22, 35 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (⟨{p}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ ( Ins4 SI3 Swap
∩ Ins2 Ins2 S ) ↔ (p = ⟨x, y⟩ ∧ p ∈ r)) |
37 | 36 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (∃p⟨{p}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ ( Ins4 SI3 Swap
∩ Ins2 Ins2 S ) ↔ ∃p(p = ⟨x, y⟩ ∧ p ∈ r)) |
38 | | elima1c 4948 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (⟨{y}, ⟨{x}, r⟩⟩ ∈ (( Ins4 SI3
Swap ∩ Ins2
Ins2 S ) “
1c) ↔ ∃p⟨{p}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ ( Ins4 SI3
Swap ∩ Ins2
Ins2 S
)) |
39 | | df-br 4641 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (xry ↔ ⟨x, y⟩ ∈ r) |
40 | | df-clel 2349 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (⟨x, y⟩ ∈ r ↔
∃p(p = ⟨x, y⟩ ∧ p ∈ r)) |
41 | 39, 40 | bitri 240 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (xry ↔ ∃p(p = ⟨x, y⟩ ∧ p ∈ r)) |
42 | 37, 38, 41 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . 19
⊢ (⟨{y}, ⟨{x}, r⟩⟩ ∈ (( Ins4 SI3
Swap ∩ Ins2
Ins2 S ) “
1c) ↔ xry) |
43 | | elin 3220 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (⟨{p}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ ( Ins4 SI3 I ∩ Ins2 Ins2 S ) ↔ (⟨{p}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ Ins4 SI3 I ∧ ⟨{p}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ Ins2 Ins2 S )) |
44 | 2 | oqelins4 5795 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (⟨{p}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ Ins4 SI3 I ↔ ⟨{p}, ⟨{y}, {x}⟩⟩ ∈ SI3 I ) |
45 | 24, 17, 9 | otsnelsi3 5806 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (⟨{p}, ⟨{y}, {x}⟩⟩ ∈ SI3 I ↔ ⟨p, ⟨y, x⟩⟩ ∈ I
) |
46 | | df-br 4641 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (p I ⟨y, x⟩ ↔ ⟨p, ⟨y, x⟩⟩ ∈ I
) |
47 | 17, 9 | opex 4589 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ⟨y, x⟩ ∈ V |
48 | 47 | ideq 4871 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (p I ⟨y, x⟩ ↔ p =
⟨y,
x⟩) |
49 | 46, 48 | bitr3i 242 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (⟨p, ⟨y, x⟩⟩ ∈ I ↔
p = ⟨y, x⟩) |
50 | 44, 45, 49 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (⟨{p}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ Ins4 SI3 I ↔ p = ⟨y, x⟩) |
51 | 50, 34 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((⟨{p}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ Ins4 SI3 I ∧ ⟨{p}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ Ins2 Ins2 S ) ↔ (p =
⟨y,
x⟩ ∧ p ∈ r)) |
52 | 43, 51 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (⟨{p}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ ( Ins4 SI3 I ∩ Ins2 Ins2 S ) ↔ (p =
⟨y,
x⟩ ∧ p ∈ r)) |
53 | 52 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (∃p⟨{p}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ ( Ins4 SI3 I ∩ Ins2 Ins2 S ) ↔ ∃p(p = ⟨y, x⟩ ∧ p ∈ r)) |
54 | | elima1c 4948 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (⟨{y}, ⟨{x}, r⟩⟩ ∈ (( Ins4 SI3
I ∩ Ins2 Ins2
S ) “ 1c) ↔ ∃p⟨{p}, ⟨{y}, ⟨{x}, r⟩⟩⟩ ∈ ( Ins4 SI3 I ∩ Ins2 Ins2 S )) |
55 | | df-br 4641 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (yrx ↔ ⟨y, x⟩ ∈ r) |
56 | | df-clel 2349 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (⟨y, x⟩ ∈ r ↔
∃p(p = ⟨y, x⟩ ∧ p ∈ r)) |
57 | 55, 56 | bitri 240 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (yrx ↔ ∃p(p = ⟨y, x⟩ ∧ p ∈ r)) |
58 | 53, 54, 57 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . 19
⊢ (⟨{y}, ⟨{x}, r⟩⟩ ∈ (( Ins4 SI3
I ∩ Ins2 Ins2
S ) “ 1c) ↔ yrx) |
59 | 42, 58 | orbi12i 507 |
. . . . . . . . . . . . . . . . . 18
⊢ ((⟨{y}, ⟨{x}, r⟩⟩ ∈ (( Ins4 SI3
Swap ∩ Ins2
Ins2 S ) “
1c) ∨ ⟨{y}, ⟨{x}, r⟩⟩ ∈ (( Ins4 SI3
I ∩ Ins2 Ins2
S ) “ 1c)) ↔
(xry ∨ yrx)) |
60 | 20, 21, 59 | 3bitri 262 |
. . . . . . . . . . . . . . . . 17
⊢ (⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩ ∈ Ins4 ((( Ins4 SI3
Swap ∩ Ins2
Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c)) ↔ (xry ∨ yrx)) |
61 | 60 | notbii 287 |
. . . . . . . . . . . . . . . 16
⊢ (¬ ⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩ ∈ Ins4 ((( Ins4 SI3
Swap ∩ Ins2
Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c)) ↔ ¬
(xry ∨ yrx)) |
62 | 19, 61 | anbi12i 678 |
. . . . . . . . . . . . . . 15
⊢ ((⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩ ∈ Ins2 Ins2 S ∧ ¬ ⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩ ∈ Ins4 ((( Ins4 SI3 Swap
∩ Ins2 Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) ↔ (y ∈ a ∧ ¬ (xry ∨ yrx))) |
63 | 13, 62 | bitri 240 |
. . . . . . . . . . . . . 14
⊢ (⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩ ∈ ( Ins2 Ins2 S ∖ Ins4 ((( Ins4 SI3
Swap ∩ Ins2
Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) ↔ (y ∈ a ∧ ¬ (xry ∨ yrx))) |
64 | 63 | exbii 1582 |
. . . . . . . . . . . . 13
⊢ (∃y⟨{y}, ⟨{x}, ⟨r, a⟩⟩⟩ ∈ ( Ins2 Ins2 S ∖ Ins4 ((( Ins4 SI3
Swap ∩ Ins2
Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) ↔ ∃y(y ∈ a ∧ ¬ (xry ∨ yrx))) |
65 | 12, 64 | bitri 240 |
. . . . . . . . . . . 12
⊢ (⟨{x}, ⟨r, a⟩⟩ ∈ (( Ins2 Ins2 S ∖ Ins4 ((( Ins4 SI3 Swap
∩ Ins2 Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) “
1c) ↔ ∃y(y ∈ a ∧ ¬ (xry ∨ yrx))) |
66 | | df-rex 2621 |
. . . . . . . . . . . 12
⊢ (∃y ∈ a ¬
(xry ∨ yrx) ↔ ∃y(y ∈ a ∧ ¬ (xry ∨ yrx))) |
67 | | rexnal 2626 |
. . . . . . . . . . . 12
⊢ (∃y ∈ a ¬
(xry ∨ yrx) ↔ ¬
∀y
∈ a
(xry ∨ yrx)) |
68 | 65, 66, 67 | 3bitr2i 264 |
. . . . . . . . . . 11
⊢ (⟨{x}, ⟨r, a⟩⟩ ∈ (( Ins2 Ins2 S ∖ Ins4 ((( Ins4 SI3 Swap
∩ Ins2 Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) “
1c) ↔ ¬ ∀y ∈ a (xry ∨ yrx)) |
69 | 11, 68 | anbi12i 678 |
. . . . . . . . . 10
⊢ ((⟨{x}, ⟨r, a⟩⟩ ∈ Ins2 S ∧ ⟨{x}, ⟨r, a⟩⟩ ∈ (( Ins2 Ins2 S ∖ Ins4 ((( Ins4 SI3
Swap ∩ Ins2
Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) ↔ (x ∈ a ∧ ¬ ∀y ∈ a (xry ∨ yrx))) |
70 | 7, 69 | bitri 240 |
. . . . . . . . 9
⊢ (⟨{x}, ⟨r, a⟩⟩ ∈ ( Ins2 S ∩ (( Ins2 Ins2 S ∖ Ins4 ((( Ins4 SI3 Swap
∩ Ins2 Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) ↔ (x ∈ a ∧ ¬ ∀y ∈ a (xry ∨ yrx))) |
71 | 70 | exbii 1582 |
. . . . . . . 8
⊢ (∃x⟨{x}, ⟨r, a⟩⟩ ∈ ( Ins2 S ∩ (( Ins2 Ins2 S ∖ Ins4 ((( Ins4 SI3 Swap
∩ Ins2 Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) ↔ ∃x(x ∈ a ∧ ¬ ∀y ∈ a (xry ∨ yrx))) |
72 | 6, 71 | bitri 240 |
. . . . . . 7
⊢ (⟨r, a⟩ ∈ (( Ins2 S ∩ (( Ins2 Ins2 S ∖ Ins4 ((( Ins4 SI3
Swap ∩ Ins2
Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c) ↔ ∃x(x ∈ a ∧ ¬ ∀y ∈ a (xry ∨ yrx))) |
73 | | df-rex 2621 |
. . . . . . 7
⊢ (∃x ∈ a ¬ ∀y ∈ a (xry ∨ yrx) ↔ ∃x(x ∈ a ∧ ¬ ∀y ∈ a (xry ∨ yrx))) |
74 | | rexnal 2626 |
. . . . . . 7
⊢ (∃x ∈ a ¬ ∀y ∈ a (xry ∨ yrx) ↔ ¬ ∀x ∈ a ∀y ∈ a (xry ∨ yrx)) |
75 | 72, 73, 74 | 3bitr2i 264 |
. . . . . 6
⊢ (⟨r, a⟩ ∈ (( Ins2 S ∩ (( Ins2 Ins2 S ∖ Ins4 ((( Ins4 SI3
Swap ∩ Ins2
Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c) ↔ ¬ ∀x ∈ a ∀y ∈ a (xry ∨ yrx)) |
76 | 75 | con2bii 322 |
. . . . 5
⊢ (∀x ∈ a ∀y ∈ a (xry ∨ yrx) ↔ ¬ ⟨r, a⟩ ∈ (( Ins2 S ∩ (( Ins2 Ins2 S ∖ Ins4 ((( Ins4 SI3
Swap ∩ Ins2
Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c)) |
77 | 5, 76 | bitr4i 243 |
. . . 4
⊢ (⟨r, a⟩ ∈ ∼ (( Ins2 S ∩ (( Ins2 Ins2 S ∖ Ins4 ((( Ins4 SI3
Swap ∩ Ins2
Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c) ↔ ∀x ∈ a ∀y ∈ a (xry ∨ yrx)) |
78 | 77 | opabbi2i 4867 |
. . 3
⊢ ∼ (( Ins2 S ∩ (( Ins2 Ins2 S ∖ Ins4 ((( Ins4 SI3 Swap
∩ Ins2 Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c) = {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a (xry ∨ yrx)} |
79 | 1, 78 | eqtr4i 2376 |
. 2
⊢ Connex = ∼ (( Ins2
S ∩ (( Ins2
Ins2 S ∖ Ins4 ((( Ins4 SI3
Swap ∩ Ins2
Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c) |
80 | | ssetex 4745 |
. . . . . 6
⊢ S ∈
V |
81 | 80 | ins2ex 5798 |
. . . . 5
⊢ Ins2 S ∈ V |
82 | 81 | ins2ex 5798 |
. . . . . . 7
⊢ Ins2 Ins2 S ∈
V |
83 | | swapex 4743 |
. . . . . . . . . . . . 13
⊢ Swap ∈
V |
84 | 83 | si3ex 5807 |
. . . . . . . . . . . 12
⊢ SI3 Swap
∈ V |
85 | 84 | ins4ex 5800 |
. . . . . . . . . . 11
⊢ Ins4 SI3
Swap ∈
V |
86 | 85, 82 | inex 4106 |
. . . . . . . . . 10
⊢ ( Ins4 SI3
Swap ∩ Ins2
Ins2 S ) ∈ V |
87 | | 1cex 4143 |
. . . . . . . . . 10
⊢
1c ∈
V |
88 | 86, 87 | imaex 4748 |
. . . . . . . . 9
⊢ (( Ins4 SI3
Swap ∩ Ins2
Ins2 S ) “
1c) ∈ V |
89 | | idex 5505 |
. . . . . . . . . . . . 13
⊢ I ∈ V |
90 | 89 | si3ex 5807 |
. . . . . . . . . . . 12
⊢ SI3 I ∈ V |
91 | 90 | ins4ex 5800 |
. . . . . . . . . . 11
⊢ Ins4 SI3
I ∈ V |
92 | 91, 82 | inex 4106 |
. . . . . . . . . 10
⊢ ( Ins4 SI3
I ∩ Ins2 Ins2
S ) ∈
V |
93 | 92, 87 | imaex 4748 |
. . . . . . . . 9
⊢ (( Ins4 SI3
I ∩ Ins2 Ins2
S ) “ 1c) ∈ V |
94 | 88, 93 | unex 4107 |
. . . . . . . 8
⊢ ((( Ins4 SI3
Swap ∩ Ins2
Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c)) ∈ V |
95 | 94 | ins4ex 5800 |
. . . . . . 7
⊢ Ins4 ((( Ins4 SI3 Swap
∩ Ins2 Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c)) ∈ V |
96 | 82, 95 | difex 4108 |
. . . . . 6
⊢ ( Ins2 Ins2 S ∖ Ins4 ((( Ins4 SI3 Swap
∩ Ins2 Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) ∈ V |
97 | 96, 87 | imaex 4748 |
. . . . 5
⊢ (( Ins2 Ins2 S ∖ Ins4 ((( Ins4 SI3 Swap
∩ Ins2 Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) “
1c) ∈ V |
98 | 81, 97 | inex 4106 |
. . . 4
⊢ ( Ins2 S ∩ (( Ins2 Ins2 S ∖ Ins4 ((( Ins4 SI3 Swap
∩ Ins2 Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) ∈ V |
99 | 98, 87 | imaex 4748 |
. . 3
⊢ (( Ins2 S ∩ (( Ins2 Ins2 S ∖ Ins4 ((( Ins4 SI3 Swap
∩ Ins2 Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c) ∈ V |
100 | 99 | complex 4105 |
. 2
⊢ ∼ (( Ins2 S ∩ (( Ins2 Ins2 S ∖ Ins4 ((( Ins4 SI3 Swap
∩ Ins2 Ins2 S ) “
1c) ∪ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c) ∈ V |
101 | 79, 100 | eqeltri 2423 |
1
⊢ Connex ∈
V |