New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  funsex GIF version

Theorem funsex 5828
 Description: The class of all functions forms a set. (Contributed by SF, 18-Feb-2015.)
Assertion
Ref Expression
funsex Funs V

Proof of Theorem funsex
Dummy variables x f y z p q are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-funs 5760 . . 3 Funs = {f Fun f}
2 elima1c 4947 . . . . . . . 8 (f ( ∼ ( ∼ (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) “ 1c) “ 1c) ↔ x{x}, f ∼ ( ∼ (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) “ 1c))
3 snex 4111 . . . . . . . . . . . 12 {x} V
4 vex 2862 . . . . . . . . . . . 12 f V
53, 4opex 4588 . . . . . . . . . . 11 {x}, f V
65elcompl 3225 . . . . . . . . . 10 ({x}, f ∼ ( ∼ (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) “ 1c) ↔ ¬ {x}, f ( ∼ (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) “ 1c))
7 elima1c 4947 . . . . . . . . . . . 12 ({x}, f ( ∼ (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) “ 1c) ↔ z{z}, {x}, f ∼ (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c))
8 elima1c 4947 . . . . . . . . . . . . . . . 16 ({z}, {x}, f (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) ↔ y{y}, {z}, {x}, f ( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ))
9 eldif 3221 . . . . . . . . . . . . . . . . . 18 ({y}, {z}, {x}, f ( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) ↔ ({y}, {z}, {x}, f Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) ¬ {y}, {z}, {x}, f Ins3 I ))
10 snex 4111 . . . . . . . . . . . . . . . . . . . . 21 {z} V
1110otelins2 5791 . . . . . . . . . . . . . . . . . . . 20 ({y}, {z}, {x}, f Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) ↔ {y}, {x}, f (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ))
12 vex 2862 . . . . . . . . . . . . . . . . . . . . . . 23 x V
13 vex 2862 . . . . . . . . . . . . . . . . . . . . . . 23 y V
1412, 13opex 4588 . . . . . . . . . . . . . . . . . . . . . 22 x, y V
1514, 4opelssetsn 4760 . . . . . . . . . . . . . . . . . . . . 21 ({x, y}, f S x, y f)
16 df-br 4640 . . . . . . . . . . . . . . . . . . . . . . . 24 (p( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ){y}, {x}, fp, {y}, {x}, f ( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ))
17 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . 25 (p, {y}, {x}, f ( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) ↔ (p, {y}, {x}, f Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) p, {y}, {x}, f Ins2 Ins2 2nd ))
184oqelins4 5794 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (p, {y}, {x}, f Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ↔ p, {y}, {x} ((1stSI3 (2nd ⊗ 1st )) “ 1c))
19 elima1c 4947 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (p, {y}, {x} ((1stSI3 (2nd ⊗ 1st )) “ 1c) ↔ q{q}, p, {y}, {x} (1stSI3 (2nd ⊗ 1st )))
20 oteltxp 5782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ({q}, p, {y}, {x} (1stSI3 (2nd ⊗ 1st )) ↔ ({q}, p 1st {q}, {y}, {x} SI3 (2nd ⊗ 1st )))
21 opelcnv 4893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ({q}, p 1stp, {q} 1st )
22 df-br 4640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (p1st {q} ↔ p, {q} 1st )
2321, 22bitr4i 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ({q}, p 1stp1st {q})
24 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 q V
2524, 13, 12otsnelsi3 5805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ({q}, {y}, {x} SI3 (2nd ⊗ 1st ) ↔ q, y, x (2nd ⊗ 1st ))
26 oteltxp 5782 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (q, y, x (2nd ⊗ 1st ) ↔ (q, y 2nd q, x 1st ))
27 df-br 4640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (q1st xq, x 1st )
28 df-br 4640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (q2nd yq, y 2nd )
2927, 28anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((q1st x q2nd y) ↔ (q, x 1st q, y 2nd ))
30 ancom 437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((q, x 1st q, y 2nd ) ↔ (q, y 2nd q, x 1st ))
3129, 30bitr2i 241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((q, y 2nd q, x 1st ) ↔ (q1st x q2nd y))
3212, 13op1st2nd 5790 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((q1st x q2nd y) ↔ q = x, y)
3326, 31, 323bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (q, y, x (2nd ⊗ 1st ) ↔ q = x, y)
3425, 33bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ({q}, {y}, {x} SI3 (2nd ⊗ 1st ) ↔ q = x, y)
3523, 34anbi12ci 679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (({q}, p 1st {q}, {y}, {x} SI3 (2nd ⊗ 1st )) ↔ (q = x, y p1st {q}))
3620, 35bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ({q}, p, {y}, {x} (1stSI3 (2nd ⊗ 1st )) ↔ (q = x, y p1st {q}))
3736exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (q{q}, p, {y}, {x} (1stSI3 (2nd ⊗ 1st )) ↔ q(q = x, y p1st {q}))
38 sneq 3744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (q = x, y → {q} = {x, y})
3938breq2d 4651 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (q = x, y → (p1st {q} ↔ p1st {x, y}))
4014, 39ceqsexv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (q(q = x, y p1st {q}) ↔ p1st {x, y})
4119, 37, 403bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (p, {y}, {x} ((1stSI3 (2nd ⊗ 1st )) “ 1c) ↔ p1st {x, y})
4218, 41bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (p, {y}, {x}, f Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ↔ p1st {x, y})
433otelins2 5791 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (p, {x}, f Ins2 2ndp, f 2nd )
44 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 {y} V
4544otelins2 5791 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (p, {y}, {x}, f Ins2 Ins2 2ndp, {x}, f Ins2 2nd )
46 df-br 4640 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (p2nd fp, f 2nd )
4743, 45, 463bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (p, {y}, {x}, f Ins2 Ins2 2ndp2nd f)
4842, 47anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((p, {y}, {x}, f Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) p, {y}, {x}, f Ins2 Ins2 2nd ) ↔ (p1st {x, y} p2nd f))
4917, 48bitri 240 . . . . . . . . . . . . . . . . . . . . . . . 24 (p, {y}, {x}, f ( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) ↔ (p1st {x, y} p2nd f))
50 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . 25 {x, y} V
5150, 4op1st2nd 5790 . . . . . . . . . . . . . . . . . . . . . . . 24 ((p1st {x, y} p2nd f) ↔ p = {x, y}, f)
5216, 49, 513bitri 262 . . . . . . . . . . . . . . . . . . . . . . 23 (p( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ){y}, {x}, fp = {x, y}, f)
5352rexbii 2639 . . . . . . . . . . . . . . . . . . . . . 22 (p S p( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ){y}, {x}, fp S p = {x, y}, f)
54 elima 4754 . . . . . . . . . . . . . . . . . . . . . 22 ({y}, {x}, f (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) ↔ p S p( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ){y}, {x}, f)
55 risset 2661 . . . . . . . . . . . . . . . . . . . . . 22 ({x, y}, f S p S p = {x, y}, f)
5653, 54, 553bitr4i 268 . . . . . . . . . . . . . . . . . . . . 21 ({y}, {x}, f (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) ↔ {x, y}, f S )
57 df-br 4640 . . . . . . . . . . . . . . . . . . . . 21 (xfyx, y f)
5815, 56, 573bitr4i 268 . . . . . . . . . . . . . . . . . . . 20 ({y}, {x}, f (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) ↔ xfy)
5911, 58bitri 240 . . . . . . . . . . . . . . . . . . 19 ({y}, {z}, {x}, f Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) ↔ xfy)
605otelins3 5792 . . . . . . . . . . . . . . . . . . . . 21 ({y}, {z}, {x}, f Ins3 I ↔ {y}, {z} I )
6110ideq 4870 . . . . . . . . . . . . . . . . . . . . . 22 ({y} I {z} ↔ {y} = {z})
62 df-br 4640 . . . . . . . . . . . . . . . . . . . . . 22 ({y} I {z} ↔ {y}, {z} I )
6313sneqb 3876 . . . . . . . . . . . . . . . . . . . . . 22 ({y} = {z} ↔ y = z)
6461, 62, 633bitr3i 266 . . . . . . . . . . . . . . . . . . . . 21 ({y}, {z} I ↔ y = z)
6560, 64bitri 240 . . . . . . . . . . . . . . . . . . . 20 ({y}, {z}, {x}, f Ins3 I ↔ y = z)
6665notbii 287 . . . . . . . . . . . . . . . . . . 19 {y}, {z}, {x}, f Ins3 I ↔ ¬ y = z)
6759, 66anbi12i 678 . . . . . . . . . . . . . . . . . 18 (({y}, {z}, {x}, f Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) ¬ {y}, {z}, {x}, f Ins3 I ) ↔ (xfy ¬ y = z))
689, 67bitri 240 . . . . . . . . . . . . . . . . 17 ({y}, {z}, {x}, f ( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) ↔ (xfy ¬ y = z))
6968exbii 1582 . . . . . . . . . . . . . . . 16 (y{y}, {z}, {x}, f ( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) ↔ y(xfy ¬ y = z))
708, 69bitri 240 . . . . . . . . . . . . . . 15 ({z}, {x}, f (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) ↔ y(xfy ¬ y = z))
7170notbii 287 . . . . . . . . . . . . . 14 {z}, {x}, f (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) ↔ ¬ y(xfy ¬ y = z))
7210, 5opex 4588 . . . . . . . . . . . . . . 15 {z}, {x}, f V
7372elcompl 3225 . . . . . . . . . . . . . 14 ({z}, {x}, f ∼ (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) ↔ ¬ {z}, {x}, f (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c))
74 exanali 1585 . . . . . . . . . . . . . . 15 (y(xfy ¬ y = z) ↔ ¬ y(xfyy = z))
7574con2bii 322 . . . . . . . . . . . . . 14 (y(xfyy = z) ↔ ¬ y(xfy ¬ y = z))
7671, 73, 753bitr4i 268 . . . . . . . . . . . . 13 ({z}, {x}, f ∼ (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) ↔ y(xfyy = z))
7776exbii 1582 . . . . . . . . . . . 12 (z{z}, {x}, f ∼ (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) ↔ zy(xfyy = z))
787, 77bitri 240 . . . . . . . . . . 11 ({x}, f ( ∼ (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) “ 1c) ↔ zy(xfyy = z))
7978notbii 287 . . . . . . . . . 10 {x}, f ( ∼ (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) “ 1c) ↔ ¬ zy(xfyy = z))
806, 79bitri 240 . . . . . . . . 9 ({x}, f ∼ ( ∼ (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) “ 1c) ↔ ¬ zy(xfyy = z))
8180exbii 1582 . . . . . . . 8 (x{x}, f ∼ ( ∼ (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) “ 1c) ↔ x ¬ zy(xfyy = z))
822, 81bitri 240 . . . . . . 7 (f ( ∼ ( ∼ (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) “ 1c) “ 1c) ↔ x ¬ zy(xfyy = z))
8382notbii 287 . . . . . 6 f ( ∼ ( ∼ (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) “ 1c) “ 1c) ↔ ¬ x ¬ zy(xfyy = z))
844elcompl 3225 . . . . . 6 (f ∼ ( ∼ ( ∼ (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) “ 1c) “ 1c) ↔ ¬ f ( ∼ ( ∼ (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) “ 1c) “ 1c))
85 alex 1572 . . . . . 6 (xzy(xfyy = z) ↔ ¬ x ¬ zy(xfyy = z))
8683, 84, 853bitr4i 268 . . . . 5 (f ∼ ( ∼ ( ∼ (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) “ 1c) “ 1c) ↔ xzy(xfyy = z))
87 dffun3 5120 . . . . 5 (Fun fxzy(xfyy = z))
8886, 87bitr4i 243 . . . 4 (f ∼ ( ∼ ( ∼ (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) “ 1c) “ 1c) ↔ Fun f)
8988abbi2i 2464 . . 3 ∼ ( ∼ ( ∼ (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) “ 1c) “ 1c) = {f Fun f}
901, 89eqtr4i 2376 . 2 Funs = ∼ ( ∼ ( ∼ (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) “ 1c) “ 1c)
91 1stex 4739 . . . . . . . . . . . . . . . 16 1st V
9291cnvex 5102 . . . . . . . . . . . . . . 15 1st V
93 2ndex 5112 . . . . . . . . . . . . . . . . 17 2nd V
9493, 91txpex 5785 . . . . . . . . . . . . . . . 16 (2nd ⊗ 1st ) V
9594si3ex 5806 . . . . . . . . . . . . . . 15 SI3 (2nd ⊗ 1st ) V
9692, 95txpex 5785 . . . . . . . . . . . . . 14 (1stSI3 (2nd ⊗ 1st )) V
97 1cex 4142 . . . . . . . . . . . . . 14 1c V
9896, 97imaex 4747 . . . . . . . . . . . . 13 ((1stSI3 (2nd ⊗ 1st )) “ 1c) V
9998ins4ex 5799 . . . . . . . . . . . 12 Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) V
10093ins2ex 5797 . . . . . . . . . . . . 13 Ins2 2nd V
101100ins2ex 5797 . . . . . . . . . . . 12 Ins2 Ins2 2nd V
10299, 101inex 4105 . . . . . . . . . . 11 ( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) V
103 ssetex 4744 . . . . . . . . . . 11 S V
104102, 103imaex 4747 . . . . . . . . . 10 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) V
105104ins2ex 5797 . . . . . . . . 9 Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) V
106 idex 5504 . . . . . . . . . 10 I V
107106ins3ex 5798 . . . . . . . . 9 Ins3 I V
108105, 107difex 4107 . . . . . . . 8 ( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) V
109108, 97imaex 4747 . . . . . . 7 (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) V
110109complex 4104 . . . . . 6 ∼ (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) V
111110, 97imaex 4747 . . . . 5 ( ∼ (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) “ 1c) V
112111complex 4104 . . . 4 ∼ ( ∼ (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) “ 1c) V
113112, 97imaex 4747 . . 3 ( ∼ ( ∼ (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) “ 1c) “ 1c) V
114113complex 4104 . 2 ∼ ( ∼ ( ∼ (( Ins2 (( Ins4 ((1stSI3 (2nd ⊗ 1st )) “ 1c) ∩ Ins2 Ins2 2nd ) “ S ) Ins3 I ) “ 1c) “ 1c) “ 1c) V
11590, 114eqeltri 2423 1 Funs V
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 358  ∀wal 1540  ∃wex 1541   = wceq 1642   ∈ wcel 1710  {cab 2339  ∃wrex 2615  Vcvv 2859   ∼ ccompl 3205   ∖ cdif 3206   ∩ cin 3208  {csn 3737  1cc1c 4134  ⟨cop 4561   class class class wbr 4639  1st c1st 4717   S csset 4719   “ cima 4722   I cid 4763  ◡ccnv 4771  Fun wfun 4775  2nd c2nd 4783   ⊗ ctxp 5735   Ins2 cins2 5749   Ins3 cins3 5751   Ins4 cins4 5755   SI3 csi3 5757   Funs cfuns 5759 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-reu 2621  df-rmo 2622  df-rab 2623  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-pss 3261  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-iota 4339  df-0c 4377  df-addc 4378  df-nnc 4379  df-fin 4380  df-lefin 4440  df-ltfin 4441  df-ncfin 4442  df-tfin 4443  df-evenfin 4444  df-oddfin 4445  df-sfin 4446  df-spfin 4447  df-phi 4565  df-op 4566  df-proj1 4567  df-proj2 4568  df-opab 4623  df-br 4640  df-1st 4723  df-swap 4724  df-sset 4725  df-co 4726  df-ima 4727  df-si 4728  df-id 4767  df-cnv 4785  df-fun 4789  df-2nd 4797  df-txp 5736  df-ins2 5750  df-ins3 5752  df-ins4 5756  df-si3 5758  df-funs 5760 This theorem is referenced by:  fnsex  5832  mapexi  6003  pmex  6005  fnpm  6008
 Copyright terms: Public domain W3C validator