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

Theorem foundex 5914
Description: The class of all founded relationships is a set. (Contributed by SF, 19-Feb-2015.)
Assertion
Ref Expression
foundex Fr V

Proof of Theorem foundex
Dummy variables a r t x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-found 5905 . . 3 Fr = {r, a x((x a x) → z x y x (yrzy = z))}
2 vex 2862 . . . . . . 7 r V
3 vex 2862 . . . . . . 7 a V
42, 3opex 4588 . . . . . 6 r, a V
54elcompl 3225 . . . . 5 (r, a ∼ ran ( ∼ (( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) “ 1c) ⊗ ( S ∩ ( ∼ {} × V))) ↔ ¬ r, a ran ( ∼ (( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) “ 1c) ⊗ ( S ∩ ( ∼ {} × V))))
6 elrn2 4897 . . . . . . 7 (r, a ran ( ∼ (( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) “ 1c) ⊗ ( S ∩ ( ∼ {} × V))) ↔ xx, r, a ( ∼ (( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) “ 1c) ⊗ ( S ∩ ( ∼ {} × V))))
7 oteltxp 5782 . . . . . . . . 9 (x, r, a ( ∼ (( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) “ 1c) ⊗ ( S ∩ ( ∼ {} × V))) ↔ (x, r ∼ (( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) “ 1c) x, a ( S ∩ ( ∼ {} × V))))
8 vex 2862 . . . . . . . . . . . . 13 x V
98, 2opex 4588 . . . . . . . . . . . 12 x, r V
109elcompl 3225 . . . . . . . . . . 11 (x, r ∼ (( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) “ 1c) ↔ ¬ x, r (( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) “ 1c))
11 elin 3219 . . . . . . . . . . . . . . 15 ({z}, x, r ( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) ↔ ({z}, x, r Ins3 S {z}, x, r ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)))
122otelins3 5792 . . . . . . . . . . . . . . . . 17 ({z}, x, r Ins3 S {z}, x S )
13 vex 2862 . . . . . . . . . . . . . . . . . 18 z V
1413, 8opelssetsn 4760 . . . . . . . . . . . . . . . . 17 ({z}, x S z x)
1512, 14bitri 240 . . . . . . . . . . . . . . . 16 ({z}, x, r Ins3 S z x)
16 snex 4111 . . . . . . . . . . . . . . . . . . 19 {z} V
1716, 9opex 4588 . . . . . . . . . . . . . . . . . 18 {z}, x, r V
1817elcompl 3225 . . . . . . . . . . . . . . . . 17 ({z}, x, r ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c) ↔ ¬ {z}, x, r (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c))
19 elin 3219 . . . . . . . . . . . . . . . . . . . . . 22 ({y}, {z}, x, r ( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) ↔ ({y}, {z}, x, r Ins2 Ins3 S {y}, {z}, x, r ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )))
2016otelins2 5791 . . . . . . . . . . . . . . . . . . . . . . . 24 ({y}, {z}, x, r Ins2 Ins3 S {y}, x, r Ins3 S )
212otelins3 5792 . . . . . . . . . . . . . . . . . . . . . . . 24 ({y}, x, r Ins3 S {y}, x S )
22 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . 25 y V
2322, 8opelssetsn 4760 . . . . . . . . . . . . . . . . . . . . . . . 24 ({y}, x S y x)
2420, 21, 233bitri 262 . . . . . . . . . . . . . . . . . . . . . . 23 ({y}, {z}, x, r Ins2 Ins3 S y x)
25 eldif 3221 . . . . . . . . . . . . . . . . . . . . . . . 24 ({y}, {z}, x, r ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I ) ↔ ({y}, {z}, x, r (( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) ¬ {y}, {z}, x, r Ins3 I ))
26 elin 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ({t}, {y}, {z}, x, r ( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) ↔ ({t}, {y}, {z}, x, r Ins4 SI3 I {t}, {y}, {z}, x, r Ins2 Ins2 Ins2 S ))
279oqelins4 5794 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ({t}, {y}, {z}, x, r Ins4 SI3 I ↔ {t}, {y}, {z} SI3 I )
28 vex 2862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 t V
2928, 22, 13otsnelsi3 5805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ({t}, {y}, {z} SI3 I ↔ t, y, z I )
30 df-br 4640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (t I y, zt, y, z I )
3122, 13opex 4588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 y, z V
3231ideq 4870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (t I y, zt = y, z)
3330, 32bitr3i 242 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (t, y, z I ↔ t = y, z)
3427, 29, 333bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ({t}, {y}, {z}, x, r Ins4 SI3 I ↔ t = y, z)
35 snex 4111 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 {y} V
3635otelins2 5791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ({t}, {y}, {z}, x, r Ins2 Ins2 Ins2 S {t}, {z}, x, r Ins2 Ins2 S )
3716otelins2 5791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ({t}, {z}, x, r Ins2 Ins2 S {t}, x, r Ins2 S )
388otelins2 5791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ({t}, x, r Ins2 S {t}, r S )
3928, 2opelssetsn 4760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ({t}, r S t r)
4038, 39bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ({t}, x, r Ins2 S t r)
4136, 37, 403bitri 262 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ({t}, {y}, {z}, x, r Ins2 Ins2 Ins2 S t r)
4234, 41anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (({t}, {y}, {z}, x, r Ins4 SI3 I {t}, {y}, {z}, x, r Ins2 Ins2 Ins2 S ) ↔ (t = y, z t r))
4326, 42bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({t}, {y}, {z}, x, r ( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) ↔ (t = y, z t r))
4443exbii 1582 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (t{t}, {y}, {z}, x, r ( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) ↔ t(t = y, z t r))
45 elima1c 4947 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({y}, {z}, x, r (( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) ↔ t{t}, {y}, {z}, x, r ( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ))
46 df-br 4640 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (yrzy, z r)
47 df-clel 2349 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (y, z rt(t = y, z t r))
4846, 47bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (yrzt(t = y, z t r))
4944, 45, 483bitr4i 268 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({y}, {z}, x, r (( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) ↔ yrz)
509otelins3 5792 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({y}, {z}, x, r Ins3 I ↔ {y}, {z} I )
51 df-br 4640 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ({y} I {z} ↔ {y}, {z} I )
5216ideq 4870 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ({y} I {z} ↔ {y} = {z})
5322sneqb 3876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ({y} = {z} ↔ y = z)
5452, 53bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ({y} I {z} ↔ y = z)
5551, 54bitr3i 242 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ({y}, {z} I ↔ y = z)
5650, 55bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({y}, {z}, x, r Ins3 I ↔ y = z)
5756notbii 287 . . . . . . . . . . . . . . . . . . . . . . . . 25 {y}, {z}, x, r Ins3 I ↔ ¬ y = z)
5849, 57anbi12i 678 . . . . . . . . . . . . . . . . . . . . . . . 24 (({y}, {z}, x, r (( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) ¬ {y}, {z}, x, r Ins3 I ) ↔ (yrz ¬ y = z))
5925, 58bitri 240 . . . . . . . . . . . . . . . . . . . . . . 23 ({y}, {z}, x, r ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I ) ↔ (yrz ¬ y = z))
6024, 59anbi12i 678 . . . . . . . . . . . . . . . . . . . . . 22 (({y}, {z}, x, r Ins2 Ins3 S {y}, {z}, x, r ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) ↔ (y x (yrz ¬ y = z)))
6119, 60bitri 240 . . . . . . . . . . . . . . . . . . . . 21 ({y}, {z}, x, r ( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) ↔ (y x (yrz ¬ y = z)))
6261exbii 1582 . . . . . . . . . . . . . . . . . . . 20 (y{y}, {z}, x, r ( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) ↔ y(y x (yrz ¬ y = z)))
63 elima1c 4947 . . . . . . . . . . . . . . . . . . . 20 ({z}, x, r (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c) ↔ y{y}, {z}, x, r ( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )))
64 df-rex 2620 . . . . . . . . . . . . . . . . . . . 20 (y x (yrz ¬ y = z) ↔ y(y x (yrz ¬ y = z)))
6562, 63, 643bitr4i 268 . . . . . . . . . . . . . . . . . . 19 ({z}, x, r (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c) ↔ y x (yrz ¬ y = z))
66 rexanali 2660 . . . . . . . . . . . . . . . . . . 19 (y x (yrz ¬ y = z) ↔ ¬ y x (yrzy = z))
6765, 66bitri 240 . . . . . . . . . . . . . . . . . 18 ({z}, x, r (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c) ↔ ¬ y x (yrzy = z))
6867con2bii 322 . . . . . . . . . . . . . . . . 17 (y x (yrzy = z) ↔ ¬ {z}, x, r (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c))
6918, 68bitr4i 243 . . . . . . . . . . . . . . . 16 ({z}, x, r ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c) ↔ y x (yrzy = z))
7015, 69anbi12i 678 . . . . . . . . . . . . . . 15 (({z}, x, r Ins3 S {z}, x, r ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) ↔ (z x y x (yrzy = z)))
7111, 70bitri 240 . . . . . . . . . . . . . 14 ({z}, x, r ( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) ↔ (z x y x (yrzy = z)))
7271exbii 1582 . . . . . . . . . . . . 13 (z{z}, x, r ( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) ↔ z(z x y x (yrzy = z)))
73 elima1c 4947 . . . . . . . . . . . . 13 (x, r (( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) “ 1c) ↔ z{z}, x, r ( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)))
74 df-rex 2620 . . . . . . . . . . . . 13 (z x y x (yrzy = z) ↔ z(z x y x (yrzy = z)))
7572, 73, 743bitr4i 268 . . . . . . . . . . . 12 (x, r (( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) “ 1c) ↔ z x y x (yrzy = z))
7675notbii 287 . . . . . . . . . . 11 x, r (( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) “ 1c) ↔ ¬ z x y x (yrzy = z))
7710, 76bitri 240 . . . . . . . . . 10 (x, r ∼ (( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) “ 1c) ↔ ¬ z x y x (yrzy = z))
78 elin 3219 . . . . . . . . . . 11 (x, a ( S ∩ ( ∼ {} × V)) ↔ (x, a S x, a ( ∼ {} × V)))
79 df-br 4640 . . . . . . . . . . . . 13 (x S ax, a S )
808, 3brsset 4758 . . . . . . . . . . . . 13 (x S ax a)
8179, 80bitr3i 242 . . . . . . . . . . . 12 (x, a S x a)
82 opelxp 4811 . . . . . . . . . . . . . 14 (x, a ( ∼ {} × V) ↔ (x ∼ {} a V))
833, 82mpbiran2 885 . . . . . . . . . . . . 13 (x, a ( ∼ {} × V) ↔ x ∼ {})
848elcompl 3225 . . . . . . . . . . . . 13 (x ∼ {} ↔ ¬ x {})
85 elsn 3748 . . . . . . . . . . . . . 14 (x {} ↔ x = )
8685necon3bbii 2547 . . . . . . . . . . . . 13 x {} ↔ x)
8783, 84, 863bitri 262 . . . . . . . . . . . 12 (x, a ( ∼ {} × V) ↔ x)
8881, 87anbi12i 678 . . . . . . . . . . 11 ((x, a S x, a ( ∼ {} × V)) ↔ (x a x))
8978, 88bitri 240 . . . . . . . . . 10 (x, a ( S ∩ ( ∼ {} × V)) ↔ (x a x))
9077, 89anbi12ci 679 . . . . . . . . 9 ((x, r ∼ (( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) “ 1c) x, a ( S ∩ ( ∼ {} × V))) ↔ ((x a x) ¬ z x y x (yrzy = z)))
917, 90bitri 240 . . . . . . . 8 (x, r, a ( ∼ (( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) “ 1c) ⊗ ( S ∩ ( ∼ {} × V))) ↔ ((x a x) ¬ z x y x (yrzy = z)))
9291exbii 1582 . . . . . . 7 (xx, r, a ( ∼ (( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) “ 1c) ⊗ ( S ∩ ( ∼ {} × V))) ↔ x((x a x) ¬ z x y x (yrzy = z)))
93 exanali 1585 . . . . . . 7 (x((x a x) ¬ z x y x (yrzy = z)) ↔ ¬ x((x a x) → z x y x (yrzy = z)))
946, 92, 933bitri 262 . . . . . 6 (r, a ran ( ∼ (( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) “ 1c) ⊗ ( S ∩ ( ∼ {} × V))) ↔ ¬ x((x a x) → z x y x (yrzy = z)))
9594con2bii 322 . . . . 5 (x((x a x) → z x y x (yrzy = z)) ↔ ¬ r, a ran ( ∼ (( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) “ 1c) ⊗ ( S ∩ ( ∼ {} × V))))
965, 95bitr4i 243 . . . 4 (r, a ∼ ran ( ∼ (( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) “ 1c) ⊗ ( S ∩ ( ∼ {} × V))) ↔ x((x a x) → z x y x (yrzy = z)))
9796opabbi2i 4866 . . 3 ∼ ran ( ∼ (( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) “ 1c) ⊗ ( S ∩ ( ∼ {} × V))) = {r, a x((x a x) → z x y x (yrzy = z))}
981, 97eqtr4i 2376 . 2 Fr = ∼ ran ( ∼ (( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) “ 1c) ⊗ ( S ∩ ( ∼ {} × V)))
99 ssetex 4744 . . . . . . . . 9 S V
10099ins3ex 5798 . . . . . . . 8 Ins3 S V
101100ins2ex 5797 . . . . . . . . . . 11 Ins2 Ins3 S V
102 idex 5504 . . . . . . . . . . . . . . . 16 I V
103102si3ex 5806 . . . . . . . . . . . . . . 15 SI3 I V
104103ins4ex 5799 . . . . . . . . . . . . . 14 Ins4 SI3 I V
10599ins2ex 5797 . . . . . . . . . . . . . . . 16 Ins2 S V
106105ins2ex 5797 . . . . . . . . . . . . . . 15 Ins2 Ins2 S V
107106ins2ex 5797 . . . . . . . . . . . . . 14 Ins2 Ins2 Ins2 S V
108104, 107inex 4105 . . . . . . . . . . . . 13 ( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) V
109 1cex 4142 . . . . . . . . . . . . 13 1c V
110108, 109imaex 4747 . . . . . . . . . . . 12 (( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) V
111102ins3ex 5798 . . . . . . . . . . . 12 Ins3 I V
112110, 111difex 4107 . . . . . . . . . . 11 ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I ) V
113101, 112inex 4105 . . . . . . . . . 10 ( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) V
114113, 109imaex 4747 . . . . . . . . 9 (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c) V
115114complex 4104 . . . . . . . 8 ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c) V
116100, 115inex 4105 . . . . . . 7 ( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) V
117116, 109imaex 4747 . . . . . 6 (( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) “ 1c) V
118117complex 4104 . . . . 5 ∼ (( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) “ 1c) V
119 snex 4111 . . . . . . . 8 {} V
120119complex 4104 . . . . . . 7 ∼ {} V
121 vvex 4109 . . . . . . 7 V V
122120, 121xpex 5115 . . . . . 6 ( ∼ {} × V) V
12399, 122inex 4105 . . . . 5 ( S ∩ ( ∼ {} × V)) V
124118, 123txpex 5785 . . . 4 ( ∼ (( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) “ 1c) ⊗ ( S ∩ ( ∼ {} × V))) V
125124rnex 5107 . . 3 ran ( ∼ (( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) “ 1c) ⊗ ( S ∩ ( ∼ {} × V))) V
126125complex 4104 . 2 ∼ ran ( ∼ (( Ins3 S ∩ ∼ (( Ins2 Ins3 S ∩ ((( Ins4 SI3 I ∩ Ins2 Ins2 Ins2 S ) “ 1c) Ins3 I )) “ 1c)) “ 1c) ⊗ ( S ∩ ( ∼ {} × V))) V
12798, 126eqeltri 2423 1 Fr V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   wa 358  wal 1540  wex 1541   = wceq 1642   wcel 1710  wne 2516  wral 2614  wrex 2615  Vcvv 2859  ccompl 3205   cdif 3206  cin 3208   wss 3257  c0 3550  {csn 3737  1cc1c 4134  cop 4561  {copab 4622   class class class wbr 4639   S csset 4719  cima 4722   I cid 4763   × cxp 4770  ran crn 4773  ctxp 5735   Ins2 cins2 5749   Ins3 cins3 5751   Ins4 cins4 5755   SI3 csi3 5757   Fr cfound 5894
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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-xp 4784  df-cnv 4785  df-rn 4786  df-2nd 4797  df-txp 5736  df-ins2 5750  df-ins3 5752  df-ins4 5756  df-si3 5758  df-found 5905
This theorem is referenced by:  weex  5919
  Copyright terms: Public domain W3C validator