Step | Hyp | Ref
| Expression |
1 | | df-ranfn 5772 |
. . 3
⊢ Ran = (x ∈ V ↦ ran
x) |
2 | | elin 3219 |
. . . . . . . . 9
⊢ (〈{w}, 〈{z}, 〈{y}, x〉〉〉 ∈ ( Ins4 SI3 I ∩ Ins2 Ins2 S ) ↔ (〈{w}, 〈{z}, 〈{y}, x〉〉〉 ∈ Ins4 SI3 I ∧ 〈{w}, 〈{z}, 〈{y}, x〉〉〉 ∈ Ins2 Ins2 S )) |
3 | | vex 2862 |
. . . . . . . . . . . 12
⊢ x ∈
V |
4 | 3 | oqelins4 5794 |
. . . . . . . . . . 11
⊢ (〈{w}, 〈{z}, 〈{y}, x〉〉〉 ∈ Ins4 SI3 I ↔ 〈{w}, 〈{z}, {y}〉〉 ∈ SI3 I ) |
5 | | vex 2862 |
. . . . . . . . . . . . 13
⊢ w ∈
V |
6 | | vex 2862 |
. . . . . . . . . . . . 13
⊢ z ∈
V |
7 | | vex 2862 |
. . . . . . . . . . . . 13
⊢ y ∈
V |
8 | 5, 6, 7 | otsnelsi3 5805 |
. . . . . . . . . . . 12
⊢ (〈{w}, 〈{z}, {y}〉〉 ∈ SI3 I ↔ 〈w, 〈z, y〉〉 ∈ I
) |
9 | | df-br 4640 |
. . . . . . . . . . . 12
⊢ (w I 〈z, y〉 ↔ 〈w, 〈z, y〉〉 ∈ I
) |
10 | 6, 7 | opex 4588 |
. . . . . . . . . . . . 13
⊢ 〈z, y〉 ∈ V |
11 | 10 | ideq 4870 |
. . . . . . . . . . . 12
⊢ (w I 〈z, y〉 ↔ w =
〈z,
y〉) |
12 | 8, 9, 11 | 3bitr2i 264 |
. . . . . . . . . . 11
⊢ (〈{w}, 〈{z}, {y}〉〉 ∈ SI3 I ↔ w = 〈z, y〉) |
13 | 4, 12 | bitri 240 |
. . . . . . . . . 10
⊢ (〈{w}, 〈{z}, 〈{y}, x〉〉〉 ∈ Ins4 SI3 I ↔ w = 〈z, y〉) |
14 | | snex 4111 |
. . . . . . . . . . . 12
⊢ {z} ∈
V |
15 | 14 | otelins2 5791 |
. . . . . . . . . . 11
⊢ (〈{w}, 〈{z}, 〈{y}, x〉〉〉 ∈ Ins2 Ins2 S ↔ 〈{w}, 〈{y}, x〉〉 ∈ Ins2 S ) |
16 | | snex 4111 |
. . . . . . . . . . . . 13
⊢ {y} ∈
V |
17 | 16 | otelins2 5791 |
. . . . . . . . . . . 12
⊢ (〈{w}, 〈{y}, x〉〉 ∈ Ins2 S ↔ 〈{w}, x〉 ∈ S
) |
18 | 5, 3 | opelssetsn 4760 |
. . . . . . . . . . . 12
⊢ (〈{w}, x〉 ∈ S ↔ w ∈ x) |
19 | 17, 18 | bitri 240 |
. . . . . . . . . . 11
⊢ (〈{w}, 〈{y}, x〉〉 ∈ Ins2 S ↔ w ∈ x) |
20 | 15, 19 | bitri 240 |
. . . . . . . . . 10
⊢ (〈{w}, 〈{z}, 〈{y}, x〉〉〉 ∈ Ins2 Ins2 S ↔ w ∈ x) |
21 | 13, 20 | anbi12i 678 |
. . . . . . . . 9
⊢ ((〈{w}, 〈{z}, 〈{y}, x〉〉〉 ∈ Ins4 SI3 I ∧ 〈{w}, 〈{z}, 〈{y}, x〉〉〉 ∈ Ins2 Ins2 S ) ↔ (w =
〈z,
y〉 ∧ w ∈ x)) |
22 | 2, 21 | bitri 240 |
. . . . . . . 8
⊢ (〈{w}, 〈{z}, 〈{y}, x〉〉〉 ∈ ( Ins4 SI3 I ∩ Ins2 Ins2 S ) ↔ (w =
〈z,
y〉 ∧ w ∈ x)) |
23 | 22 | exbii 1582 |
. . . . . . 7
⊢ (∃w〈{w}, 〈{z}, 〈{y}, x〉〉〉 ∈ ( Ins4 SI3 I ∩ Ins2 Ins2 S ) ↔ ∃w(w = 〈z, y〉 ∧ w ∈ x)) |
24 | | elima1c 4947 |
. . . . . . 7
⊢ (〈{z}, 〈{y}, x〉〉 ∈ (( Ins4 SI3
I ∩ Ins2 Ins2
S ) “ 1c) ↔ ∃w〈{w}, 〈{z}, 〈{y}, x〉〉〉 ∈ ( Ins4 SI3 I ∩ Ins2 Ins2 S )) |
25 | | df-clel 2349 |
. . . . . . 7
⊢ (〈z, y〉 ∈ x ↔
∃w(w = 〈z, y〉 ∧ w ∈ x)) |
26 | 23, 24, 25 | 3bitr4i 268 |
. . . . . 6
⊢ (〈{z}, 〈{y}, x〉〉 ∈ (( Ins4 SI3
I ∩ Ins2 Ins2
S ) “ 1c) ↔ 〈z, y〉 ∈ x) |
27 | 26 | exbii 1582 |
. . . . 5
⊢ (∃z〈{z}, 〈{y}, x〉〉 ∈ (( Ins4 SI3
I ∩ Ins2 Ins2
S ) “ 1c) ↔ ∃z〈z, y〉 ∈ x) |
28 | | elima1c 4947 |
. . . . 5
⊢ (〈{y}, x〉 ∈ ((( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c) “
1c) ↔ ∃z〈{z}, 〈{y}, x〉〉 ∈ (( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c)) |
29 | | elrn2 4897 |
. . . . 5
⊢ (y ∈ ran x ↔ ∃z〈z, y〉 ∈ x) |
30 | 27, 28, 29 | 3bitr4i 268 |
. . . 4
⊢ (〈{y}, x〉 ∈ ((( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c) “
1c) ↔ y ∈ ran x) |
31 | 30 | releqmpt 5808 |
. . 3
⊢ ((V × V)
∩ ◡ ∼ (( Ins3 S ⊕ Ins2 ((( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c) “
1c)) “ 1c)) = (x ∈ V ↦ ran x) |
32 | 1, 31 | eqtr4i 2376 |
. 2
⊢ Ran = ((V × V) ∩ ◡ ∼ (( Ins3
S ⊕ Ins2 (((
Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c) “
1c)) “ 1c)) |
33 | | vvex 4109 |
. . 3
⊢ V ∈ V |
34 | | idex 5504 |
. . . . . . . 8
⊢ I ∈ V |
35 | 34 | si3ex 5806 |
. . . . . . 7
⊢ SI3 I ∈ V |
36 | 35 | ins4ex 5799 |
. . . . . 6
⊢ Ins4 SI3
I ∈ V |
37 | | ssetex 4744 |
. . . . . . . 8
⊢ S ∈
V |
38 | 37 | ins2ex 5797 |
. . . . . . 7
⊢ Ins2 S ∈ V |
39 | 38 | ins2ex 5797 |
. . . . . 6
⊢ Ins2 Ins2 S ∈
V |
40 | 36, 39 | inex 4105 |
. . . . 5
⊢ ( Ins4 SI3
I ∩ Ins2 Ins2
S ) ∈
V |
41 | | 1cex 4142 |
. . . . 5
⊢
1c ∈
V |
42 | 40, 41 | imaex 4747 |
. . . 4
⊢ (( Ins4 SI3
I ∩ Ins2 Ins2
S ) “ 1c) ∈ V |
43 | 42, 41 | imaex 4747 |
. . 3
⊢ ((( Ins4 SI3
I ∩ Ins2 Ins2
S ) “ 1c) “
1c) ∈ V |
44 | 33, 43 | mptexlem 5810 |
. 2
⊢ ((V × V)
∩ ◡ ∼ (( Ins3 S ⊕ Ins2 ((( Ins4 SI3 I ∩ Ins2 Ins2 S ) “ 1c) “
1c)) “ 1c)) ∈ V |
45 | 32, 44 | eqeltri 2423 |
1
⊢ Ran ∈
V |