Step | Hyp | Ref
| Expression |
1 | | df-trans 5899 |
. . 3
⊢ Trans = {〈r, a〉 ∣ ∀x ∈ a ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz)} |
2 | | vex 2862 |
. . . . . . 7
⊢ r ∈
V |
3 | | vex 2862 |
. . . . . . 7
⊢ a ∈
V |
4 | 2, 3 | opex 4588 |
. . . . . 6
⊢ 〈r, a〉 ∈ V |
5 | 4 | elcompl 3225 |
. . . . 5
⊢ (〈r, a〉 ∈ ∼ (( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c)) “
1c) ↔ ¬ 〈r, a〉 ∈ (( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4
(( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c)) “
1c)) |
6 | | elin 3219 |
. . . . . . . . . 10
⊢ (〈{x}, 〈r, a〉〉 ∈ ( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4
(( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c)) ↔ (〈{x}, 〈r, a〉〉 ∈ Ins2 S ∧ 〈{x}, 〈r, a〉〉 ∈ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c))) |
7 | 2 | otelins2 5791 |
. . . . . . . . . . . 12
⊢ (〈{x}, 〈r, a〉〉 ∈ Ins2 S ↔ 〈{x}, a〉 ∈ S
) |
8 | | vex 2862 |
. . . . . . . . . . . . 13
⊢ x ∈
V |
9 | 8, 3 | opelssetsn 4760 |
. . . . . . . . . . . 12
⊢ (〈{x}, a〉 ∈ S ↔ x ∈ a) |
10 | 7, 9 | bitri 240 |
. . . . . . . . . . 11
⊢ (〈{x}, 〈r, a〉〉 ∈ Ins2 S ↔ x ∈ a) |
11 | | elima1c 4947 |
. . . . . . . . . . . 12
⊢ (〈{x}, 〈r, a〉〉 ∈ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4
(( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c) ↔ ∃y〈{y}, 〈{x}, 〈r, a〉〉〉 ∈ ( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c))) |
12 | | elin 3219 |
. . . . . . . . . . . . . 14
⊢ (〈{y}, 〈{x}, 〈r, a〉〉〉 ∈ ( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) ↔ (〈{y}, 〈{x}, 〈r, a〉〉〉 ∈ Ins2 Ins2 S ∧ 〈{y}, 〈{x}, 〈r, a〉〉〉 ∈ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4
(( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c))) |
13 | | snex 4111 |
. . . . . . . . . . . . . . . . 17
⊢ {x} ∈
V |
14 | 13 | otelins2 5791 |
. . . . . . . . . . . . . . . 16
⊢ (〈{y}, 〈{x}, 〈r, a〉〉〉 ∈ Ins2 Ins2 S ↔ 〈{y}, 〈r, a〉〉 ∈ Ins2 S ) |
15 | 2 | otelins2 5791 |
. . . . . . . . . . . . . . . 16
⊢ (〈{y}, 〈r, a〉〉 ∈ Ins2 S ↔ 〈{y}, a〉 ∈ S
) |
16 | | vex 2862 |
. . . . . . . . . . . . . . . . 17
⊢ y ∈
V |
17 | 16, 3 | opelssetsn 4760 |
. . . . . . . . . . . . . . . 16
⊢ (〈{y}, a〉 ∈ S ↔ y ∈ a) |
18 | 14, 15, 17 | 3bitri 262 |
. . . . . . . . . . . . . . 15
⊢ (〈{y}, 〈{x}, 〈r, a〉〉〉 ∈ Ins2 Ins2 S ↔ y ∈ a) |
19 | | elima1c 4947 |
. . . . . . . . . . . . . . . 16
⊢ (〈{y}, 〈{x}, 〈r, a〉〉〉 ∈ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4
(( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c) ↔ ∃z〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ ( Ins2 Ins2 Ins2 S ∩ (((V × Ins4
(( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)))) |
20 | | elin 3219 |
. . . . . . . . . . . . . . . . . 18
⊢ (〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ ( Ins2 Ins2 Ins2 S ∩ (((V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) ↔ (〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ Ins2 Ins2 Ins2 S ∧ 〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ (((V × Ins4 ((
Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)))) |
21 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ {y} ∈
V |
22 | 21 | otelins2 5791 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ Ins2 Ins2 Ins2 S ↔ 〈{z}, 〈{x}, 〈r, a〉〉〉 ∈ Ins2 Ins2 S ) |
23 | 13 | otelins2 5791 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (〈{z}, 〈{x}, 〈r, a〉〉〉 ∈ Ins2 Ins2 S ↔ 〈{z}, 〈r, a〉〉 ∈ Ins2 S ) |
24 | 2 | otelins2 5791 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (〈{z}, 〈r, a〉〉 ∈ Ins2 S ↔ 〈{z}, a〉 ∈ S
) |
25 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ z ∈
V |
26 | 25, 3 | opelssetsn 4760 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (〈{z}, a〉 ∈ S ↔ z ∈ a) |
27 | 24, 26 | bitri 240 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (〈{z}, 〈r, a〉〉 ∈ Ins2 S ↔ z ∈ a) |
28 | 22, 23, 27 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . 19
⊢ (〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ Ins2 Ins2 Ins2 S ↔ z ∈ a) |
29 | | eldif 3221 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ (((V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ↔ (〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ ((V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∧ ¬ 〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) |
30 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ ((V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ↔ (〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ (V × Ins4 ((
Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∧ 〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c))) |
31 | | snex 4111 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ {z} ∈
V |
32 | | opelxp 4811 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ (V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ↔ ({z} ∈ V ∧ 〈{y}, 〈{x}, 〈r, a〉〉〉 ∈ Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) |
33 | 31, 32 | mpbiran 884 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ (V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ↔ 〈{y}, 〈{x}, 〈r, a〉〉〉 ∈ Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) |
34 | 3 | oqelins4 5794 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (〈{y}, 〈{x}, 〈r, a〉〉〉 ∈ Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) ↔ 〈{y}, 〈{x}, r〉〉 ∈ (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) |
35 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (〈{z}, 〈{y}, 〈{x}, r〉〉〉 ∈ ( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) ↔ (〈{z}, 〈{y}, 〈{x}, r〉〉〉 ∈ Ins4 SI3 (2nd ⊗
1st ) ∧ 〈{z}, 〈{y}, 〈{x}, r〉〉〉 ∈ Ins2 Ins2 S )) |
36 | 2 | oqelins4 5794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (〈{z}, 〈{y}, 〈{x}, r〉〉〉 ∈ Ins4 SI3 (2nd ⊗
1st ) ↔ 〈{z}, 〈{y}, {x}〉〉 ∈ SI3 (2nd ⊗
1st )) |
37 | 25, 16, 8 | otsnelsi3 5805 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (〈{z}, 〈{y}, {x}〉〉 ∈ SI3 (2nd ⊗
1st ) ↔ 〈z, 〈y, x〉〉 ∈ (2nd ⊗ 1st
)) |
38 | | oteltxp 5782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (〈z, 〈y, x〉〉 ∈
(2nd ⊗ 1st ) ↔ (〈z, y〉 ∈ 2nd ∧
〈z,
x〉 ∈ 1st )) |
39 | | ancom 437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((〈z, y〉 ∈ 2nd ∧
〈z,
x〉 ∈ 1st ) ↔ (〈z, x〉 ∈ 1st ∧
〈z,
y〉 ∈ 2nd )) |
40 | | df-br 4640 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (z1st x ↔ 〈z, x〉 ∈
1st ) |
41 | | df-br 4640 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (z2nd y ↔ 〈z, y〉 ∈
2nd ) |
42 | 40, 41 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((z1st x ∧ z2nd y) ↔ (〈z, x〉 ∈ 1st ∧
〈z,
y〉 ∈ 2nd )) |
43 | 39, 42 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((〈z, y〉 ∈ 2nd ∧
〈z,
x〉 ∈ 1st ) ↔ (z1st x ∧ z2nd y)) |
44 | 8, 16 | op1st2nd 5790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((z1st x ∧ z2nd y) ↔ z =
〈x,
y〉) |
45 | 38, 43, 44 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (〈z, 〈y, x〉〉 ∈
(2nd ⊗ 1st ) ↔ z = 〈x, y〉) |
46 | 36, 37, 45 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (〈{z}, 〈{y}, 〈{x}, r〉〉〉 ∈ Ins4 SI3 (2nd ⊗
1st ) ↔ z = 〈x, y〉) |
47 | 21 | otelins2 5791 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (〈{z}, 〈{y}, 〈{x}, r〉〉〉 ∈ Ins2 Ins2 S ↔ 〈{z}, 〈{x}, r〉〉 ∈ Ins2 S ) |
48 | 13 | otelins2 5791 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (〈{z}, 〈{x}, r〉〉 ∈ Ins2 S ↔ 〈{z}, r〉 ∈ S
) |
49 | 25, 2 | opelssetsn 4760 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (〈{z}, r〉 ∈ S ↔ z ∈ r) |
50 | 47, 48, 49 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (〈{z}, 〈{y}, 〈{x}, r〉〉〉 ∈ Ins2 Ins2 S ↔ z ∈ r) |
51 | 46, 50 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((〈{z}, 〈{y}, 〈{x}, r〉〉〉 ∈ Ins4 SI3 (2nd ⊗
1st ) ∧ 〈{z}, 〈{y}, 〈{x}, r〉〉〉 ∈ Ins2 Ins2 S ) ↔ (z = 〈x, y〉 ∧ z ∈ r)) |
52 | 35, 51 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (〈{z}, 〈{y}, 〈{x}, r〉〉〉 ∈ ( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) ↔ (z = 〈x, y〉 ∧ z ∈ r)) |
53 | 52 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (∃z〈{z}, 〈{y}, 〈{x}, r〉〉〉 ∈ ( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) ↔ ∃z(z = 〈x, y〉 ∧ z ∈ r)) |
54 | | elima1c 4947 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (〈{y}, 〈{x}, r〉〉 ∈ (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) ↔ ∃z〈{z}, 〈{y}, 〈{x}, r〉〉〉 ∈ ( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S )) |
55 | | df-br 4640 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (xry ↔ 〈x, y〉 ∈ r) |
56 | | df-clel 2349 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (〈x, y〉 ∈ r ↔
∃z(z = 〈x, y〉 ∧ z ∈ r)) |
57 | 55, 56 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (xry ↔ ∃z(z = 〈x, y〉 ∧ z ∈ r)) |
58 | 53, 54, 57 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (〈{y}, 〈{x}, r〉〉 ∈ (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) ↔ xry) |
59 | 33, 34, 58 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ (V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ↔ xry) |
60 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (〈{q}, 〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉〉 ∈ ( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) ↔ (〈{q}, 〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉〉 ∈ Ins4 SI3 (2nd ⊗
1st ) ∧ 〈{q}, 〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉〉 ∈ Ins2 Ins2 Ins2 Ins3 S )) |
61 | 13, 4 | opex 4588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 〈{x}, 〈r, a〉〉 ∈
V |
62 | 61 | oqelins4 5794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (〈{q}, 〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉〉 ∈ Ins4 SI3 (2nd ⊗
1st ) ↔ 〈{q}, 〈{z}, {y}〉〉 ∈ SI3 (2nd ⊗
1st )) |
63 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ q ∈
V |
64 | 63, 25, 16 | otsnelsi3 5805 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (〈{q}, 〈{z}, {y}〉〉 ∈ SI3 (2nd ⊗
1st ) ↔ 〈q, 〈z, y〉〉 ∈ (2nd ⊗ 1st
)) |
65 | | oteltxp 5782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (〈q, 〈z, y〉〉 ∈
(2nd ⊗ 1st ) ↔ (〈q, z〉 ∈ 2nd ∧
〈q,
y〉 ∈ 1st )) |
66 | | ancom 437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((〈q, z〉 ∈ 2nd ∧
〈q,
y〉 ∈ 1st ) ↔ (〈q, y〉 ∈ 1st ∧
〈q,
z〉 ∈ 2nd )) |
67 | | df-br 4640 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (q1st y ↔ 〈q, y〉 ∈
1st ) |
68 | | df-br 4640 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (q2nd z ↔ 〈q, z〉 ∈
2nd ) |
69 | 67, 68 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((q1st y ∧ q2nd z) ↔ (〈q, y〉 ∈ 1st ∧
〈q,
z〉 ∈ 2nd )) |
70 | 66, 69 | bitr4i 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((〈q, z〉 ∈ 2nd ∧
〈q,
y〉 ∈ 1st ) ↔ (q1st y ∧ q2nd z)) |
71 | 16, 25 | op1st2nd 5790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((q1st y ∧ q2nd z) ↔ q =
〈y,
z〉) |
72 | 65, 70, 71 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (〈q, 〈z, y〉〉 ∈
(2nd ⊗ 1st ) ↔ q = 〈y, z〉) |
73 | 62, 64, 72 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (〈{q}, 〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉〉 ∈ Ins4 SI3 (2nd ⊗
1st ) ↔ q = 〈y, z〉) |
74 | 31 | otelins2 5791 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (〈{q}, 〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉〉 ∈ Ins2 Ins2 Ins2 Ins3 S ↔ 〈{q}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ Ins2 Ins2 Ins3 S ) |
75 | 21 | otelins2 5791 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (〈{q}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ Ins2 Ins2 Ins3 S ↔ 〈{q}, 〈{x}, 〈r, a〉〉〉 ∈ Ins2 Ins3 S ) |
76 | 13 | otelins2 5791 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (〈{q}, 〈{x}, 〈r, a〉〉〉 ∈ Ins2 Ins3 S ↔ 〈{q}, 〈r, a〉〉 ∈ Ins3 S ) |
77 | 3 | otelins3 5792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (〈{q}, 〈r, a〉〉 ∈ Ins3 S ↔ 〈{q}, r〉 ∈ S
) |
78 | 63, 2 | opelssetsn 4760 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (〈{q}, r〉 ∈ S ↔ q ∈ r) |
79 | 76, 77, 78 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (〈{q}, 〈{x}, 〈r, a〉〉〉 ∈ Ins2 Ins3 S ↔ q ∈ r) |
80 | 74, 75, 79 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (〈{q}, 〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉〉 ∈ Ins2 Ins2 Ins2 Ins3 S ↔ q ∈ r) |
81 | 73, 80 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((〈{q}, 〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉〉 ∈ Ins4 SI3 (2nd ⊗
1st ) ∧ 〈{q}, 〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉〉 ∈ Ins2 Ins2 Ins2 Ins3 S ) ↔ (q = 〈y, z〉 ∧ q ∈ r)) |
82 | 60, 81 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (〈{q}, 〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉〉 ∈ ( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) ↔ (q = 〈y, z〉 ∧ q ∈ r)) |
83 | 82 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (∃q〈{q}, 〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉〉 ∈ ( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) ↔ ∃q(q = 〈y, z〉 ∧ q ∈ r)) |
84 | | elima1c 4947 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c) ↔ ∃q〈{q}, 〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉〉 ∈ ( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S )) |
85 | | df-br 4640 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (yrz ↔ 〈y, z〉 ∈ r) |
86 | | df-clel 2349 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (〈y, z〉 ∈ r ↔
∃q(q = 〈y, z〉 ∧ q ∈ r)) |
87 | 85, 86 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (yrz ↔ ∃q(q = 〈y, z〉 ∧ q ∈ r)) |
88 | 83, 84, 87 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c) ↔ yrz) |
89 | 59, 88 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ (V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∧ 〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c)) ↔ (xry ∧ yrz)) |
90 | 30, 89 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ ((V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ↔ (xry ∧ yrz)) |
91 | 21 | otelins2 5791 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) ↔ 〈{z}, 〈{x}, 〈r, a〉〉〉 ∈ Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) |
92 | 3 | oqelins4 5794 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (〈{z}, 〈{x}, 〈r, a〉〉〉 ∈ Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) ↔ 〈{z}, 〈{x}, r〉〉 ∈ (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) |
93 | | elin 3219 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (〈{y}, 〈{z}, 〈{x}, r〉〉〉 ∈ ( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) ↔ (〈{y}, 〈{z}, 〈{x}, r〉〉〉 ∈ Ins4 SI3 (2nd ⊗
1st ) ∧ 〈{y}, 〈{z}, 〈{x}, r〉〉〉 ∈ Ins2 Ins2 S )) |
94 | 2 | oqelins4 5794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (〈{y}, 〈{z}, 〈{x}, r〉〉〉 ∈ Ins4 SI3 (2nd ⊗
1st ) ↔ 〈{y}, 〈{z}, {x}〉〉 ∈ SI3 (2nd ⊗
1st )) |
95 | 16, 25, 8 | otsnelsi3 5805 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (〈{y}, 〈{z}, {x}〉〉 ∈ SI3 (2nd ⊗
1st ) ↔ 〈y, 〈z, x〉〉 ∈ (2nd ⊗ 1st
)) |
96 | | ancom 437 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((〈y, z〉 ∈ 2nd ∧
〈y,
x〉 ∈ 1st ) ↔ (〈y, x〉 ∈ 1st ∧
〈y,
z〉 ∈ 2nd )) |
97 | | oteltxp 5782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (〈y, 〈z, x〉〉 ∈
(2nd ⊗ 1st ) ↔ (〈y, z〉 ∈ 2nd ∧
〈y,
x〉 ∈ 1st )) |
98 | | df-br 4640 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (y1st x ↔ 〈y, x〉 ∈
1st ) |
99 | | df-br 4640 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (y2nd z ↔ 〈y, z〉 ∈
2nd ) |
100 | 98, 99 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((y1st x ∧ y2nd z) ↔ (〈y, x〉 ∈ 1st ∧
〈y,
z〉 ∈ 2nd )) |
101 | 96, 97, 100 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (〈y, 〈z, x〉〉 ∈
(2nd ⊗ 1st ) ↔ (y1st x ∧ y2nd z)) |
102 | 8, 25 | op1st2nd 5790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((y1st x ∧ y2nd z) ↔ y =
〈x,
z〉) |
103 | 95, 101, 102 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (〈{y}, 〈{z}, {x}〉〉 ∈ SI3 (2nd ⊗
1st ) ↔ y = 〈x, z〉) |
104 | 94, 103 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (〈{y}, 〈{z}, 〈{x}, r〉〉〉 ∈ Ins4 SI3 (2nd ⊗
1st ) ↔ y = 〈x, z〉) |
105 | 31 | otelins2 5791 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (〈{y}, 〈{z}, 〈{x}, r〉〉〉 ∈ Ins2 Ins2 S ↔ 〈{y}, 〈{x}, r〉〉 ∈ Ins2 S ) |
106 | 13 | otelins2 5791 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (〈{y}, 〈{x}, r〉〉 ∈ Ins2 S ↔ 〈{y}, r〉 ∈ S
) |
107 | 16, 2 | opelssetsn 4760 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (〈{y}, r〉 ∈ S ↔ y ∈ r) |
108 | 105, 106,
107 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (〈{y}, 〈{z}, 〈{x}, r〉〉〉 ∈ Ins2 Ins2 S ↔ y ∈ r) |
109 | 104, 108 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((〈{y}, 〈{z}, 〈{x}, r〉〉〉 ∈ Ins4 SI3 (2nd ⊗
1st ) ∧ 〈{y}, 〈{z}, 〈{x}, r〉〉〉 ∈ Ins2 Ins2 S ) ↔ (y = 〈x, z〉 ∧ y ∈ r)) |
110 | 93, 109 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (〈{y}, 〈{z}, 〈{x}, r〉〉〉 ∈ ( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) ↔ (y = 〈x, z〉 ∧ y ∈ r)) |
111 | 110 | exbii 1582 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (∃y〈{y}, 〈{z}, 〈{x}, r〉〉〉 ∈ ( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) ↔ ∃y(y = 〈x, z〉 ∧ y ∈ r)) |
112 | | elima1c 4947 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (〈{z}, 〈{x}, r〉〉 ∈ (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) ↔ ∃y〈{y}, 〈{z}, 〈{x}, r〉〉〉 ∈ ( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S )) |
113 | | df-br 4640 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (xrz ↔ 〈x, z〉 ∈ r) |
114 | | df-clel 2349 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (〈x, z〉 ∈ r ↔
∃y(y = 〈x, z〉 ∧ y ∈ r)) |
115 | 113, 114 | bitri 240 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (xrz ↔ ∃y(y = 〈x, z〉 ∧ y ∈ r)) |
116 | 111, 112,
115 | 3bitr4i 268 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (〈{z}, 〈{x}, r〉〉 ∈ (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) ↔ xrz) |
117 | 91, 92, 116 | 3bitri 262 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) ↔ xrz) |
118 | 117 | notbii 287 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬ 〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) ↔ ¬ xrz) |
119 | 90, 118 | anbi12i 678 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ ((V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∧ ¬ 〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ↔ ((xry ∧ yrz) ∧ ¬ xrz)) |
120 | 29, 119 | bitri 240 |
. . . . . . . . . . . . . . . . . . 19
⊢ (〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ (((V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ↔ ((xry ∧ yrz) ∧ ¬ xrz)) |
121 | 28, 120 | anbi12i 678 |
. . . . . . . . . . . . . . . . . 18
⊢ ((〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ Ins2 Ins2 Ins2 S ∧ 〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ (((V × Ins4 ((
Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) ↔ (z ∈ a ∧ ((xry ∧ yrz) ∧ ¬ xrz))) |
122 | 20, 121 | bitri 240 |
. . . . . . . . . . . . . . . . 17
⊢ (〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ ( Ins2 Ins2 Ins2 S ∩ (((V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) ↔ (z ∈ a ∧ ((xry ∧ yrz) ∧ ¬ xrz))) |
123 | 122 | exbii 1582 |
. . . . . . . . . . . . . . . 16
⊢ (∃z〈{z}, 〈{y}, 〈{x}, 〈r, a〉〉〉〉 ∈ ( Ins2 Ins2 Ins2 S ∩ (((V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) ↔ ∃z(z ∈ a ∧ ((xry ∧ yrz) ∧ ¬ xrz))) |
124 | | df-rex 2620 |
. . . . . . . . . . . . . . . . 17
⊢ (∃z ∈ a ((xry ∧ yrz) ∧ ¬ xrz) ↔ ∃z(z ∈ a ∧ ((xry ∧ yrz) ∧ ¬ xrz))) |
125 | | rexanali 2660 |
. . . . . . . . . . . . . . . . 17
⊢ (∃z ∈ a ((xry ∧ yrz) ∧ ¬ xrz) ↔ ¬ ∀z ∈ a ((xry ∧ yrz) → xrz)) |
126 | 124, 125 | bitr3i 242 |
. . . . . . . . . . . . . . . 16
⊢ (∃z(z ∈ a ∧ ((xry ∧ yrz) ∧ ¬ xrz)) ↔ ¬ ∀z ∈ a ((xry ∧ yrz) → xrz)) |
127 | 19, 123, 126 | 3bitri 262 |
. . . . . . . . . . . . . . 15
⊢ (〈{y}, 〈{x}, 〈r, a〉〉〉 ∈ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4
(( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c) ↔ ¬ ∀z ∈ a ((xry ∧ yrz) → xrz)) |
128 | 18, 127 | anbi12i 678 |
. . . . . . . . . . . . . 14
⊢ ((〈{y}, 〈{x}, 〈r, a〉〉〉 ∈ Ins2 Ins2 S ∧ 〈{y}, 〈{x}, 〈r, a〉〉〉 ∈ (( Ins2 Ins2 Ins2 S ∩ (((V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) ↔ (y ∈ a ∧ ¬ ∀z ∈ a ((xry ∧ yrz) → xrz))) |
129 | 12, 128 | bitri 240 |
. . . . . . . . . . . . 13
⊢ (〈{y}, 〈{x}, 〈r, a〉〉〉 ∈ ( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) ↔ (y ∈ a ∧ ¬ ∀z ∈ a ((xry ∧ yrz) → xrz))) |
130 | 129 | exbii 1582 |
. . . . . . . . . . . 12
⊢ (∃y〈{y}, 〈{x}, 〈r, a〉〉〉 ∈ ( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) ↔ ∃y(y ∈ a ∧ ¬ ∀z ∈ a ((xry ∧ yrz) → xrz))) |
131 | | df-rex 2620 |
. . . . . . . . . . . . 13
⊢ (∃y ∈ a ¬ ∀z ∈ a ((xry ∧ yrz) → xrz) ↔ ∃y(y ∈ a ∧ ¬ ∀z ∈ a ((xry ∧ yrz) → xrz))) |
132 | | rexnal 2625 |
. . . . . . . . . . . . 13
⊢ (∃y ∈ a ¬ ∀z ∈ a ((xry ∧ yrz) → xrz) ↔ ¬ ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz)) |
133 | 131, 132 | bitr3i 242 |
. . . . . . . . . . . 12
⊢ (∃y(y ∈ a ∧ ¬ ∀z ∈ a ((xry ∧ yrz) → xrz)) ↔ ¬ ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz)) |
134 | 11, 130, 133 | 3bitri 262 |
. . . . . . . . . . 11
⊢ (〈{x}, 〈r, a〉〉 ∈ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4
(( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c) ↔ ¬ ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz)) |
135 | 10, 134 | anbi12i 678 |
. . . . . . . . . 10
⊢ ((〈{x}, 〈r, a〉〉 ∈ Ins2 S ∧ 〈{x}, 〈r, a〉〉 ∈ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c)) ↔ (x ∈ a ∧ ¬ ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz))) |
136 | 6, 135 | bitri 240 |
. . . . . . . . 9
⊢ (〈{x}, 〈r, a〉〉 ∈ ( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4
(( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c)) ↔ (x ∈ a ∧ ¬ ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz))) |
137 | 136 | exbii 1582 |
. . . . . . . 8
⊢ (∃x〈{x}, 〈r, a〉〉 ∈ ( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4
(( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c)) ↔ ∃x(x ∈ a ∧ ¬ ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz))) |
138 | | elima1c 4947 |
. . . . . . . 8
⊢ (〈r, a〉 ∈ (( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c)) “
1c) ↔ ∃x〈{x}, 〈r, a〉〉 ∈ ( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c))) |
139 | | df-rex 2620 |
. . . . . . . 8
⊢ (∃x ∈ a ¬ ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz) ↔ ∃x(x ∈ a ∧ ¬ ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz))) |
140 | 137, 138,
139 | 3bitr4i 268 |
. . . . . . 7
⊢ (〈r, a〉 ∈ (( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c)) “
1c) ↔ ∃x ∈ a ¬ ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz)) |
141 | | rexnal 2625 |
. . . . . . 7
⊢ (∃x ∈ a ¬ ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz) ↔ ¬ ∀x ∈ a ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz)) |
142 | 140, 141 | bitri 240 |
. . . . . 6
⊢ (〈r, a〉 ∈ (( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c)) “
1c) ↔ ¬ ∀x ∈ a ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz)) |
143 | 142 | con2bii 322 |
. . . . 5
⊢ (∀x ∈ a ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz) ↔ ¬ 〈r, a〉 ∈ (( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c)) “
1c)) |
144 | 5, 143 | bitr4i 243 |
. . . 4
⊢ (〈r, a〉 ∈ ∼ (( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c)) “
1c) ↔ ∀x ∈ a ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) →
xrz)) |
145 | 144 | opabbi2i 4866 |
. . 3
⊢ ∼ (( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4
(( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c)) “
1c) = {〈r, a〉 ∣ ∀x ∈ a ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz)} |
146 | 1, 145 | eqtr4i 2376 |
. 2
⊢ Trans = ∼ (( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c)) “
1c) |
147 | | ssetex 4744 |
. . . . . 6
⊢ S ∈
V |
148 | 147 | ins2ex 5797 |
. . . . 5
⊢ Ins2 S ∈ V |
149 | 148 | ins2ex 5797 |
. . . . . . 7
⊢ Ins2 Ins2 S ∈
V |
150 | 149 | ins2ex 5797 |
. . . . . . . . 9
⊢ Ins2 Ins2 Ins2 S ∈ V |
151 | | vvex 4109 |
. . . . . . . . . . . 12
⊢ V ∈ V |
152 | | 2ndex 5112 |
. . . . . . . . . . . . . . . . . 18
⊢ 2nd
∈ V |
153 | | 1stex 4739 |
. . . . . . . . . . . . . . . . . 18
⊢ 1st
∈ V |
154 | 152, 153 | txpex 5785 |
. . . . . . . . . . . . . . . . 17
⊢ (2nd
⊗ 1st ) ∈
V |
155 | 154 | si3ex 5806 |
. . . . . . . . . . . . . . . 16
⊢ SI3 (2nd ⊗
1st ) ∈ V |
156 | 155 | ins4ex 5799 |
. . . . . . . . . . . . . . 15
⊢ Ins4 SI3
(2nd ⊗ 1st ) ∈
V |
157 | 156, 149 | inex 4105 |
. . . . . . . . . . . . . 14
⊢ ( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) ∈
V |
158 | | 1cex 4142 |
. . . . . . . . . . . . . 14
⊢
1c ∈
V |
159 | 157, 158 | imaex 4747 |
. . . . . . . . . . . . 13
⊢ (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) ∈ V |
160 | 159 | ins4ex 5799 |
. . . . . . . . . . . 12
⊢ Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c) ∈ V |
161 | 151, 160 | xpex 5115 |
. . . . . . . . . . 11
⊢ (V × Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∈ V |
162 | 147 | ins3ex 5798 |
. . . . . . . . . . . . . . . 16
⊢ Ins3 S ∈ V |
163 | 162 | ins2ex 5797 |
. . . . . . . . . . . . . . 15
⊢ Ins2 Ins3 S ∈
V |
164 | 163 | ins2ex 5797 |
. . . . . . . . . . . . . 14
⊢ Ins2 Ins2 Ins3 S ∈ V |
165 | 164 | ins2ex 5797 |
. . . . . . . . . . . . 13
⊢ Ins2 Ins2 Ins2 Ins3 S ∈
V |
166 | 156, 165 | inex 4105 |
. . . . . . . . . . . 12
⊢ ( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) ∈
V |
167 | 166, 158 | imaex 4747 |
. . . . . . . . . . 11
⊢ (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “ 1c) ∈ V |
168 | 161, 167 | inex 4105 |
. . . . . . . . . 10
⊢ ((V × Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∈ V |
169 | 160 | ins2ex 5797 |
. . . . . . . . . 10
⊢ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c) ∈ V |
170 | 168, 169 | difex 4107 |
. . . . . . . . 9
⊢ (((V × Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c)) ∈ V |
171 | 150, 170 | inex 4105 |
. . . . . . . 8
⊢ ( Ins2 Ins2 Ins2 S ∩ (((V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) ∈ V |
172 | 171, 158 | imaex 4747 |
. . . . . . 7
⊢ (( Ins2 Ins2 Ins2 S ∩ (((V ×
Ins4 (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c) ∈ V |
173 | 149, 172 | inex 4105 |
. . . . . 6
⊢ ( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4
(( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) ∈ V |
174 | 173, 158 | imaex 4747 |
. . . . 5
⊢ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4
(( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c) ∈ V |
175 | 148, 174 | inex 4105 |
. . . 4
⊢ ( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4
(( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c)) ∈ V |
176 | 175, 158 | imaex 4747 |
. . 3
⊢ (( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4
(( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c)) “
1c) ∈ V |
177 | 176 | complex 4104 |
. 2
⊢ ∼ (( Ins2 S ∩ (( Ins2 Ins2 S ∩ (( Ins2 Ins2 Ins2 S ∩ (((V × Ins4
(( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 S ) “
1c)) ∩ (( Ins4 SI3 (2nd ⊗
1st ) ∩ Ins2 Ins2 Ins2 Ins3 S ) “
1c)) ∖ Ins2 Ins4 (( Ins4 SI3
(2nd ⊗ 1st ) ∩ Ins2 Ins2 S ) “ 1c))) “
1c)) “ 1c)) “
1c) ∈ V |
178 | 146, 177 | eqeltri 2423 |
1
⊢ Trans ∈
V |