Metamath Proof Explorer

Theorem ismnushort

Description: Express the predicate on U and z in ismnu in a shorter form while avoiding complicated definitions. (Contributed by Rohan Ridenour, 10-Oct-2024)

Ref Expression
Assertion ismnushort 
|- ( A. f e. ~P U E. w e. U ( ~P z C_ ( U i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) <-> ( ~P z C_ U /\ A. f E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( ~P z C_ ( U i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) -> ~P z C_ ( U i^i w ) )
2 1 reximi 
 |-  ( E. w e. U ( ~P z C_ ( U i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) -> E. w e. U ~P z C_ ( U i^i w ) )
3 2 ralimi 
 |-  ( A. f e. ~P U E. w e. U ( ~P z C_ ( U i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) -> A. f e. ~P U E. w e. U ~P z C_ ( U i^i w ) )
4 0elpw 
 |-  (/) e. ~P U
5 4 a1i 
 |-  ( T. -> (/) e. ~P U )
6 biidd 
 |-  ( ( T. /\ f = (/) ) -> ( E. w e. U ~P z C_ ( U i^i w ) <-> E. w e. U ~P z C_ ( U i^i w ) ) )
7 5 6 rspcdv 
 |-  ( T. -> ( A. f e. ~P U E. w e. U ~P z C_ ( U i^i w ) -> E. w e. U ~P z C_ ( U i^i w ) ) )
8 7 mptru 
 |-  ( A. f e. ~P U E. w e. U ~P z C_ ( U i^i w ) -> E. w e. U ~P z C_ ( U i^i w ) )
9 inss1 
 |-  ( U i^i w ) C_ U
10 sstr2 
 |-  ( ~P z C_ ( U i^i w ) -> ( ( U i^i w ) C_ U -> ~P z C_ U ) )
11 9 10 mpi 
 |-  ( ~P z C_ ( U i^i w ) -> ~P z C_ U )
12 11 reximi 
 |-  ( E. w e. U ~P z C_ ( U i^i w ) -> E. w e. U ~P z C_ U )
13 8 12 syl 
 |-  ( A. f e. ~P U E. w e. U ~P z C_ ( U i^i w ) -> E. w e. U ~P z C_ U )
14 rexex 
 |-  ( E. w e. U ~P z C_ U -> E. w ~P z C_ U )
15 ax5e 
 |-  ( E. w ~P z C_ U -> ~P z C_ U )
16 14 15 syl 
 |-  ( E. w e. U ~P z C_ U -> ~P z C_ U )
17 3 13 16 3syl 
 |-  ( A. f e. ~P U E. w e. U ( ~P z C_ ( U i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) -> ~P z C_ U )
18 inss1 
 |-  ( U i^i g ) C_ U
19 vex 
 |-  g e. _V
20 19 inex2 
 |-  ( U i^i g ) e. _V
21 20 elpw 
 |-  ( ( U i^i g ) e. ~P U <-> ( U i^i g ) C_ U )
22 18 21 mpbir 
 |-  ( U i^i g ) e. ~P U
23 unieq 
 |-  ( f = ( U i^i g ) -> U. f = U. ( U i^i g ) )
24 23 ineq2d 
 |-  ( f = ( U i^i g ) -> ( z i^i U. f ) = ( z i^i U. ( U i^i g ) ) )
25 ineq1 
 |-  ( f = ( U i^i g ) -> ( f i^i ~P ~P w ) = ( ( U i^i g ) i^i ~P ~P w ) )
26 25 unieqd 
 |-  ( f = ( U i^i g ) -> U. ( f i^i ~P ~P w ) = U. ( ( U i^i g ) i^i ~P ~P w ) )
27 24 26 sseq12d 
 |-  ( f = ( U i^i g ) -> ( ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) <-> ( z i^i U. ( U i^i g ) ) C_ U. ( ( U i^i g ) i^i ~P ~P w ) ) )
28 27 anbi2d 
 |-  ( f = ( U i^i g ) -> ( ( ~P z C_ ( U i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) <-> ( ~P z C_ ( U i^i w ) /\ ( z i^i U. ( U i^i g ) ) C_ U. ( ( U i^i g ) i^i ~P ~P w ) ) ) )
29 28 rexbidv 
 |-  ( f = ( U i^i g ) -> ( E. w e. U ( ~P z C_ ( U i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) <-> E. w e. U ( ~P z C_ ( U i^i w ) /\ ( z i^i U. ( U i^i g ) ) C_ U. ( ( U i^i g ) i^i ~P ~P w ) ) ) )
30 29 rspcv 
 |-  ( ( U i^i g ) e. ~P U -> ( A. f e. ~P U E. w e. U ( ~P z C_ ( U i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) -> E. w e. U ( ~P z C_ ( U i^i w ) /\ ( z i^i U. ( U i^i g ) ) C_ U. ( ( U i^i g ) i^i ~P ~P w ) ) ) )
31 22 30 ax-mp 
 |-  ( A. f e. ~P U E. w e. U ( ~P z C_ ( U i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) -> E. w e. U ( ~P z C_ ( U i^i w ) /\ ( z i^i U. ( U i^i g ) ) C_ U. ( ( U i^i g ) i^i ~P ~P w ) ) )
32 31 alrimiv 
 |-  ( A. f e. ~P U E. w e. U ( ~P z C_ ( U i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) -> A. g E. w e. U ( ~P z C_ ( U i^i w ) /\ ( z i^i U. ( U i^i g ) ) C_ U. ( ( U i^i g ) i^i ~P ~P w ) ) )
33 inss2 
 |-  ( U i^i w ) C_ w
34 sstr2 
 |-  ( ~P z C_ ( U i^i w ) -> ( ( U i^i w ) C_ w -> ~P z C_ w ) )
35 33 34 mpi 
 |-  ( ~P z C_ ( U i^i w ) -> ~P z C_ w )
36 an12 
 |-  ( ( v e. U /\ ( i e. v /\ v e. g ) ) <-> ( i e. v /\ ( v e. U /\ v e. g ) ) )
37 elin 
 |-  ( v e. ( U i^i g ) <-> ( v e. U /\ v e. g ) )
38 37 bicomi 
 |-  ( ( v e. U /\ v e. g ) <-> v e. ( U i^i g ) )
39 38 anbi2i 
 |-  ( ( i e. v /\ ( v e. U /\ v e. g ) ) <-> ( i e. v /\ v e. ( U i^i g ) ) )
40 36 39 bitri 
 |-  ( ( v e. U /\ ( i e. v /\ v e. g ) ) <-> ( i e. v /\ v e. ( U i^i g ) ) )
41 40 exbii 
 |-  ( E. v ( v e. U /\ ( i e. v /\ v e. g ) ) <-> E. v ( i e. v /\ v e. ( U i^i g ) ) )
42 df-rex 
 |-  ( E. v e. U ( i e. v /\ v e. g ) <-> E. v ( v e. U /\ ( i e. v /\ v e. g ) ) )
43 eluni 
 |-  ( i e. U. ( U i^i g ) <-> E. v ( i e. v /\ v e. ( U i^i g ) ) )
44 41 42 43 3bitr4i 
 |-  ( E. v e. U ( i e. v /\ v e. g ) <-> i e. U. ( U i^i g ) )
45 simp1 
 |-  ( ( ( z i^i U. ( U i^i g ) ) C_ U. ( ( U i^i g ) i^i ~P ~P w ) /\ i e. z /\ i e. U. ( U i^i g ) ) -> ( z i^i U. ( U i^i g ) ) C_ U. ( ( U i^i g ) i^i ~P ~P w ) )
46 elin 
 |-  ( i e. ( z i^i U. ( U i^i g ) ) <-> ( i e. z /\ i e. U. ( U i^i g ) ) )
47 46 biimpri 
 |-  ( ( i e. z /\ i e. U. ( U i^i g ) ) -> i e. ( z i^i U. ( U i^i g ) ) )
48 47 3adant1 
 |-  ( ( ( z i^i U. ( U i^i g ) ) C_ U. ( ( U i^i g ) i^i ~P ~P w ) /\ i e. z /\ i e. U. ( U i^i g ) ) -> i e. ( z i^i U. ( U i^i g ) ) )
49 45 48 sseldd 
 |-  ( ( ( z i^i U. ( U i^i g ) ) C_ U. ( ( U i^i g ) i^i ~P ~P w ) /\ i e. z /\ i e. U. ( U i^i g ) ) -> i e. U. ( ( U i^i g ) i^i ~P ~P w ) )
50 eluni 
 |-  ( i e. U. ( ( U i^i g ) i^i ~P ~P w ) <-> E. u ( i e. u /\ u e. ( ( U i^i g ) i^i ~P ~P w ) ) )
51 49 50 sylib 
 |-  ( ( ( z i^i U. ( U i^i g ) ) C_ U. ( ( U i^i g ) i^i ~P ~P w ) /\ i e. z /\ i e. U. ( U i^i g ) ) -> E. u ( i e. u /\ u e. ( ( U i^i g ) i^i ~P ~P w ) ) )
52 elinel1 
 |-  ( u e. ( ( U i^i g ) i^i ~P ~P w ) -> u e. ( U i^i g ) )
53 52 elin2d 
 |-  ( u e. ( ( U i^i g ) i^i ~P ~P w ) -> u e. g )
54 elinel2 
 |-  ( u e. ( ( U i^i g ) i^i ~P ~P w ) -> u e. ~P ~P w )
55 elpwpw 
 |-  ( u e. ~P ~P w <-> ( u e. _V /\ U. u C_ w ) )
56 55 simprbi 
 |-  ( u e. ~P ~P w -> U. u C_ w )
57 54 56 syl 
 |-  ( u e. ( ( U i^i g ) i^i ~P ~P w ) -> U. u C_ w )
58 53 57 jca 
 |-  ( u e. ( ( U i^i g ) i^i ~P ~P w ) -> ( u e. g /\ U. u C_ w ) )
59 58 anim2i 
 |-  ( ( i e. u /\ u e. ( ( U i^i g ) i^i ~P ~P w ) ) -> ( i e. u /\ ( u e. g /\ U. u C_ w ) ) )
60 an12 
 |-  ( ( i e. u /\ ( u e. g /\ U. u C_ w ) ) <-> ( u e. g /\ ( i e. u /\ U. u C_ w ) ) )
61 59 60 sylib 
 |-  ( ( i e. u /\ u e. ( ( U i^i g ) i^i ~P ~P w ) ) -> ( u e. g /\ ( i e. u /\ U. u C_ w ) ) )
62 61 eximi 
 |-  ( E. u ( i e. u /\ u e. ( ( U i^i g ) i^i ~P ~P w ) ) -> E. u ( u e. g /\ ( i e. u /\ U. u C_ w ) ) )
63 df-rex 
 |-  ( E. u e. g ( i e. u /\ U. u C_ w ) <-> E. u ( u e. g /\ ( i e. u /\ U. u C_ w ) ) )
64 62 63 sylibr 
 |-  ( E. u ( i e. u /\ u e. ( ( U i^i g ) i^i ~P ~P w ) ) -> E. u e. g ( i e. u /\ U. u C_ w ) )
65 51 64 syl 
 |-  ( ( ( z i^i U. ( U i^i g ) ) C_ U. ( ( U i^i g ) i^i ~P ~P w ) /\ i e. z /\ i e. U. ( U i^i g ) ) -> E. u e. g ( i e. u /\ U. u C_ w ) )
66 65 3expia 
 |-  ( ( ( z i^i U. ( U i^i g ) ) C_ U. ( ( U i^i g ) i^i ~P ~P w ) /\ i e. z ) -> ( i e. U. ( U i^i g ) -> E. u e. g ( i e. u /\ U. u C_ w ) ) )
67 44 66 syl5bi 
 |-  ( ( ( z i^i U. ( U i^i g ) ) C_ U. ( ( U i^i g ) i^i ~P ~P w ) /\ i e. z ) -> ( E. v e. U ( i e. v /\ v e. g ) -> E. u e. g ( i e. u /\ U. u C_ w ) ) )
68 67 ralrimiva 
 |-  ( ( z i^i U. ( U i^i g ) ) C_ U. ( ( U i^i g ) i^i ~P ~P w ) -> A. i e. z ( E. v e. U ( i e. v /\ v e. g ) -> E. u e. g ( i e. u /\ U. u C_ w ) ) )
69 35 68 anim12i 
 |-  ( ( ~P z C_ ( U i^i w ) /\ ( z i^i U. ( U i^i g ) ) C_ U. ( ( U i^i g ) i^i ~P ~P w ) ) -> ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. g ) -> E. u e. g ( i e. u /\ U. u C_ w ) ) ) )
70 69 reximi 
 |-  ( E. w e. U ( ~P z C_ ( U i^i w ) /\ ( z i^i U. ( U i^i g ) ) C_ U. ( ( U i^i g ) i^i ~P ~P w ) ) -> E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. g ) -> E. u e. g ( i e. u /\ U. u C_ w ) ) ) )
71 32 70 sylg 
 |-  ( A. f e. ~P U E. w e. U ( ~P z C_ ( U i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) -> A. g E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. g ) -> E. u e. g ( i e. u /\ U. u C_ w ) ) ) )
72 elequ2 
 |-  ( f = g -> ( v e. f <-> v e. g ) )
73 72 anbi2d 
 |-  ( f = g -> ( ( i e. v /\ v e. f ) <-> ( i e. v /\ v e. g ) ) )
74 73 rexbidv 
 |-  ( f = g -> ( E. v e. U ( i e. v /\ v e. f ) <-> E. v e. U ( i e. v /\ v e. g ) ) )
75 rexeq 
 |-  ( f = g -> ( E. u e. f ( i e. u /\ U. u C_ w ) <-> E. u e. g ( i e. u /\ U. u C_ w ) ) )
76 74 75 imbi12d 
 |-  ( f = g -> ( ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) <-> ( E. v e. U ( i e. v /\ v e. g ) -> E. u e. g ( i e. u /\ U. u C_ w ) ) ) )
77 76 ralbidv 
 |-  ( f = g -> ( A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) <-> A. i e. z ( E. v e. U ( i e. v /\ v e. g ) -> E. u e. g ( i e. u /\ U. u C_ w ) ) ) )
78 77 anbi2d 
 |-  ( f = g -> ( ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) <-> ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. g ) -> E. u e. g ( i e. u /\ U. u C_ w ) ) ) ) )
79 78 rexbidv 
 |-  ( f = g -> ( E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) <-> E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. g ) -> E. u e. g ( i e. u /\ U. u C_ w ) ) ) ) )
80 79 cbvalvw 
 |-  ( A. f E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) <-> A. g E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. g ) -> E. u e. g ( i e. u /\ U. u C_ w ) ) ) )
81 71 80 sylibr 
 |-  ( A. f e. ~P U E. w e. U ( ~P z C_ ( U i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) -> A. f E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) )
82 17 81 jca 
 |-  ( A. f e. ~P U E. w e. U ( ~P z C_ ( U i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) -> ( ~P z C_ U /\ A. f E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) )
83 nfv 
 |-  F/ f ~P z C_ U
84 nfa1 
 |-  F/ f A. f E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) )
85 83 84 nfan 
 |-  F/ f ( ~P z C_ U /\ A. f E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) )
86 elpwi 
 |-  ( f e. ~P U -> f C_ U )
87 sp 
 |-  ( A. f E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) -> E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) )
88 ssin 
 |-  ( ( ~P z C_ U /\ ~P z C_ w ) <-> ~P z C_ ( U i^i w ) )
89 88 biimpi 
 |-  ( ( ~P z C_ U /\ ~P z C_ w ) -> ~P z C_ ( U i^i w ) )
90 89 ex 
 |-  ( ~P z C_ U -> ( ~P z C_ w -> ~P z C_ ( U i^i w ) ) )
91 90 adantr 
 |-  ( ( ~P z C_ U /\ f C_ U ) -> ( ~P z C_ w -> ~P z C_ ( U i^i w ) ) )
92 simp3 
 |-  ( ( ~P z C_ U /\ f C_ U /\ i e. U. f ) -> i e. U. f )
93 eluni 
 |-  ( i e. U. f <-> E. v ( i e. v /\ v e. f ) )
94 92 93 sylib 
 |-  ( ( ~P z C_ U /\ f C_ U /\ i e. U. f ) -> E. v ( i e. v /\ v e. f ) )
95 simpl2 
 |-  ( ( ( ~P z C_ U /\ f C_ U /\ i e. U. f ) /\ ( i e. v /\ v e. f ) ) -> f C_ U )
96 simprr 
 |-  ( ( ( ~P z C_ U /\ f C_ U /\ i e. U. f ) /\ ( i e. v /\ v e. f ) ) -> v e. f )
97 95 96 sseldd 
 |-  ( ( ( ~P z C_ U /\ f C_ U /\ i e. U. f ) /\ ( i e. v /\ v e. f ) ) -> v e. U )
98 simprl 
 |-  ( ( ( ~P z C_ U /\ f C_ U /\ i e. U. f ) /\ ( i e. v /\ v e. f ) ) -> i e. v )
99 97 98 96 3jca 
 |-  ( ( ( ~P z C_ U /\ f C_ U /\ i e. U. f ) /\ ( i e. v /\ v e. f ) ) -> ( v e. U /\ i e. v /\ v e. f ) )
100 99 ex 
 |-  ( ( ~P z C_ U /\ f C_ U /\ i e. U. f ) -> ( ( i e. v /\ v e. f ) -> ( v e. U /\ i e. v /\ v e. f ) ) )
101 100 eximdv 
 |-  ( ( ~P z C_ U /\ f C_ U /\ i e. U. f ) -> ( E. v ( i e. v /\ v e. f ) -> E. v ( v e. U /\ i e. v /\ v e. f ) ) )
102 94 101 mpd 
 |-  ( ( ~P z C_ U /\ f C_ U /\ i e. U. f ) -> E. v ( v e. U /\ i e. v /\ v e. f ) )
103 df-rex 
 |-  ( E. v e. U ( i e. v /\ v e. f ) <-> E. v ( v e. U /\ ( i e. v /\ v e. f ) ) )
104 3anass 
 |-  ( ( v e. U /\ i e. v /\ v e. f ) <-> ( v e. U /\ ( i e. v /\ v e. f ) ) )
105 104 exbii 
 |-  ( E. v ( v e. U /\ i e. v /\ v e. f ) <-> E. v ( v e. U /\ ( i e. v /\ v e. f ) ) )
106 103 105 bitr4i 
 |-  ( E. v e. U ( i e. v /\ v e. f ) <-> E. v ( v e. U /\ i e. v /\ v e. f ) )
107 102 106 sylibr 
 |-  ( ( ~P z C_ U /\ f C_ U /\ i e. U. f ) -> E. v e. U ( i e. v /\ v e. f ) )
108 107 3expia 
 |-  ( ( ~P z C_ U /\ f C_ U ) -> ( i e. U. f -> E. v e. U ( i e. v /\ v e. f ) ) )
109 elin 
 |-  ( u e. ( f i^i ~P ~P w ) <-> ( u e. f /\ u e. ~P ~P w ) )
110 vex 
 |-  u e. _V
111 110 55 mpbiran 
 |-  ( u e. ~P ~P w <-> U. u C_ w )
112 111 anbi2i 
 |-  ( ( u e. f /\ u e. ~P ~P w ) <-> ( u e. f /\ U. u C_ w ) )
113 109 112 bitri 
 |-  ( u e. ( f i^i ~P ~P w ) <-> ( u e. f /\ U. u C_ w ) )
114 113 anbi2i 
 |-  ( ( i e. u /\ u e. ( f i^i ~P ~P w ) ) <-> ( i e. u /\ ( u e. f /\ U. u C_ w ) ) )
115 an12 
 |-  ( ( u e. f /\ ( i e. u /\ U. u C_ w ) ) <-> ( i e. u /\ ( u e. f /\ U. u C_ w ) ) )
116 114 115 bitr4i 
 |-  ( ( i e. u /\ u e. ( f i^i ~P ~P w ) ) <-> ( u e. f /\ ( i e. u /\ U. u C_ w ) ) )
117 116 exbii 
 |-  ( E. u ( i e. u /\ u e. ( f i^i ~P ~P w ) ) <-> E. u ( u e. f /\ ( i e. u /\ U. u C_ w ) ) )
118 eluni 
 |-  ( i e. U. ( f i^i ~P ~P w ) <-> E. u ( i e. u /\ u e. ( f i^i ~P ~P w ) ) )
119 df-rex 
 |-  ( E. u e. f ( i e. u /\ U. u C_ w ) <-> E. u ( u e. f /\ ( i e. u /\ U. u C_ w ) ) )
120 117 118 119 3bitr4i 
 |-  ( i e. U. ( f i^i ~P ~P w ) <-> E. u e. f ( i e. u /\ U. u C_ w ) )
121 120 biimpri 
 |-  ( E. u e. f ( i e. u /\ U. u C_ w ) -> i e. U. ( f i^i ~P ~P w ) )
122 121 a1i 
 |-  ( ( ~P z C_ U /\ f C_ U ) -> ( E. u e. f ( i e. u /\ U. u C_ w ) -> i e. U. ( f i^i ~P ~P w ) ) )
123 108 122 imim12d 
 |-  ( ( ~P z C_ U /\ f C_ U ) -> ( ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) -> ( i e. U. f -> i e. U. ( f i^i ~P ~P w ) ) ) )
124 123 ralimdv 
 |-  ( ( ~P z C_ U /\ f C_ U ) -> ( A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) -> A. i e. z ( i e. U. f -> i e. U. ( f i^i ~P ~P w ) ) ) )
125 elin 
 |-  ( i e. ( z i^i U. f ) <-> ( i e. z /\ i e. U. f ) )
126 125 imbi1i 
 |-  ( ( i e. ( z i^i U. f ) -> i e. U. ( f i^i ~P ~P w ) ) <-> ( ( i e. z /\ i e. U. f ) -> i e. U. ( f i^i ~P ~P w ) ) )
127 impexp 
 |-  ( ( ( i e. z /\ i e. U. f ) -> i e. U. ( f i^i ~P ~P w ) ) <-> ( i e. z -> ( i e. U. f -> i e. U. ( f i^i ~P ~P w ) ) ) )
128 126 127 bitri 
 |-  ( ( i e. ( z i^i U. f ) -> i e. U. ( f i^i ~P ~P w ) ) <-> ( i e. z -> ( i e. U. f -> i e. U. ( f i^i ~P ~P w ) ) ) )
129 128 albii 
 |-  ( A. i ( i e. ( z i^i U. f ) -> i e. U. ( f i^i ~P ~P w ) ) <-> A. i ( i e. z -> ( i e. U. f -> i e. U. ( f i^i ~P ~P w ) ) ) )
130 dfss2 
 |-  ( ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) <-> A. i ( i e. ( z i^i U. f ) -> i e. U. ( f i^i ~P ~P w ) ) )
131 df-ral 
 |-  ( A. i e. z ( i e. U. f -> i e. U. ( f i^i ~P ~P w ) ) <-> A. i ( i e. z -> ( i e. U. f -> i e. U. ( f i^i ~P ~P w ) ) ) )
132 129 130 131 3bitr4i 
 |-  ( ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) <-> A. i e. z ( i e. U. f -> i e. U. ( f i^i ~P ~P w ) ) )
133 124 132 syl6ibr 
 |-  ( ( ~P z C_ U /\ f C_ U ) -> ( A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) -> ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) )
134 91 133 anim12d 
 |-  ( ( ~P z C_ U /\ f C_ U ) -> ( ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) -> ( ~P z C_ ( U i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) ) )
135 134 reximdv 
 |-  ( ( ~P z C_ U /\ f C_ U ) -> ( E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) -> E. w e. U ( ~P z C_ ( U i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) ) )
136 135 3impia 
 |-  ( ( ~P z C_ U /\ f C_ U /\ E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) -> E. w e. U ( ~P z C_ ( U i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) )
137 136 3com23 
 |-  ( ( ~P z C_ U /\ E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) /\ f C_ U ) -> E. w e. U ( ~P z C_ ( U i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) )
138 87 137 syl3an2 
 |-  ( ( ~P z C_ U /\ A. f E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) /\ f C_ U ) -> E. w e. U ( ~P z C_ ( U i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) )
139 138 3expa 
 |-  ( ( ( ~P z C_ U /\ A. f E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) /\ f C_ U ) -> E. w e. U ( ~P z C_ ( U i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) )
140 86 139 sylan2 
 |-  ( ( ( ~P z C_ U /\ A. f E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) /\ f e. ~P U ) -> E. w e. U ( ~P z C_ ( U i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) )
141 85 140 ralrimia 
 |-  ( ( ~P z C_ U /\ A. f E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) -> A. f e. ~P U E. w e. U ( ~P z C_ ( U i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) )
142 82 141 impbii 
 |-  ( A. f e. ~P U E. w e. U ( ~P z C_ ( U i^i w ) /\ ( z i^i U. f ) C_ U. ( f i^i ~P ~P w ) ) <-> ( ~P z C_ U /\ A. f E. w e. U ( ~P z C_ w /\ A. i e. z ( E. v e. U ( i e. v /\ v e. f ) -> E. u e. f ( i e. u /\ U. u C_ w ) ) ) ) )