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 rexex 
 |-  ( E. w e. U ~P z C_ U -> E. w ~P z C_ U )
14 ax5e 
 |-  ( E. w ~P z C_ U -> ~P z C_ U )
15 13 14 syl 
 |-  ( E. w e. U ~P z C_ U -> ~P z C_ U )
16 3 8 12 15 4syl 
 |-  ( 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 )
17 inss1 
 |-  ( U i^i g ) C_ U
18 vex 
 |-  g e. _V
19 18 inex2 
 |-  ( U i^i g ) e. _V
20 19 elpw 
 |-  ( ( U i^i g ) e. ~P U <-> ( U i^i g ) C_ U )
21 17 20 mpbir 
 |-  ( U i^i g ) e. ~P U
22 unieq 
 |-  ( f = ( U i^i g ) -> U. f = U. ( U i^i g ) )
23 22 ineq2d 
 |-  ( f = ( U i^i g ) -> ( z i^i U. f ) = ( z i^i U. ( U i^i g ) ) )
24 ineq1 
 |-  ( f = ( U i^i g ) -> ( f i^i ~P ~P w ) = ( ( U i^i g ) i^i ~P ~P w ) )
25 24 unieqd 
 |-  ( f = ( U i^i g ) -> U. ( f i^i ~P ~P w ) = U. ( ( U i^i g ) i^i ~P ~P w ) )
26 23 25 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 ) ) )
27 26 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 ) ) ) )
28 27 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 ) ) ) )
29 28 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 ) ) ) )
30 21 29 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 ) ) )
31 30 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 ) ) )
32 inss2 
 |-  ( U i^i w ) C_ w
33 sstr2 
 |-  ( ~P z C_ ( U i^i w ) -> ( ( U i^i w ) C_ w -> ~P z C_ w ) )
34 32 33 mpi 
 |-  ( ~P z C_ ( U i^i w ) -> ~P z C_ w )
35 an12 
 |-  ( ( v e. U /\ ( i e. v /\ v e. g ) ) <-> ( i e. v /\ ( v e. U /\ v e. g ) ) )
36 elin 
 |-  ( v e. ( U i^i g ) <-> ( v e. U /\ v e. g ) )
37 36 bicomi 
 |-  ( ( v e. U /\ v e. g ) <-> v e. ( U i^i g ) )
38 37 anbi2i 
 |-  ( ( i e. v /\ ( v e. U /\ v e. g ) ) <-> ( i e. v /\ v e. ( U i^i g ) ) )
39 35 38 bitri 
 |-  ( ( v e. U /\ ( i e. v /\ v e. g ) ) <-> ( i e. v /\ v e. ( U i^i g ) ) )
40 39 exbii 
 |-  ( E. v ( v e. U /\ ( i e. v /\ v e. g ) ) <-> E. v ( i e. v /\ v e. ( U i^i g ) ) )
41 df-rex 
 |-  ( E. v e. U ( i e. v /\ v e. g ) <-> E. v ( v e. U /\ ( i e. v /\ v e. g ) ) )
42 eluni 
 |-  ( i e. U. ( U i^i g ) <-> E. v ( i e. v /\ v e. ( U i^i g ) ) )
43 40 41 42 3bitr4i 
 |-  ( E. v e. U ( i e. v /\ v e. g ) <-> i e. U. ( U i^i g ) )
44 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 ) )
45 elin 
 |-  ( i e. ( z i^i U. ( U i^i g ) ) <-> ( i e. z /\ i e. U. ( U i^i g ) ) )
46 45 biimpri 
 |-  ( ( i e. z /\ i e. U. ( U i^i g ) ) -> i e. ( z i^i U. ( U i^i g ) ) )
47 46 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 ) ) )
48 44 47 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 ) )
49 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 ) ) )
50 48 49 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 ) ) )
51 elinel1 
 |-  ( u e. ( ( U i^i g ) i^i ~P ~P w ) -> u e. ( U i^i g ) )
52 51 elin2d 
 |-  ( u e. ( ( U i^i g ) i^i ~P ~P w ) -> u e. g )
53 elinel2 
 |-  ( u e. ( ( U i^i g ) i^i ~P ~P w ) -> u e. ~P ~P w )
54 elpwpw 
 |-  ( u e. ~P ~P w <-> ( u e. _V /\ U. u C_ w ) )
55 54 simprbi 
 |-  ( u e. ~P ~P w -> U. u C_ w )
56 53 55 syl 
 |-  ( u e. ( ( U i^i g ) i^i ~P ~P w ) -> U. u C_ w )
57 52 56 jca 
 |-  ( u e. ( ( U i^i g ) i^i ~P ~P w ) -> ( u e. g /\ U. u C_ w ) )
58 57 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 ) ) )
59 an12 
 |-  ( ( i e. u /\ ( u e. g /\ U. u C_ w ) ) <-> ( u e. g /\ ( i e. u /\ U. u C_ w ) ) )
60 58 59 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 ) ) )
61 60 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 ) ) )
62 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 ) ) )
63 61 62 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 ) )
64 50 63 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 ) )
65 64 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 ) ) )
66 43 65 biimtrid 
 |-  ( ( ( 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 ) ) )
67 66 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 ) ) )
68 34 67 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 ) ) ) )
69 68 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 ) ) ) )
70 31 69 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 ) ) ) )
71 elequ2 
 |-  ( f = g -> ( v e. f <-> v e. g ) )
72 71 anbi2d 
 |-  ( f = g -> ( ( i e. v /\ v e. f ) <-> ( i e. v /\ v e. g ) ) )
73 72 rexbidv 
 |-  ( f = g -> ( E. v e. U ( i e. v /\ v e. f ) <-> E. v e. U ( i e. v /\ v e. g ) ) )
74 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 ) ) )
75 73 74 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 ) ) ) )
76 75 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 ) ) ) )
77 76 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 ) ) ) ) )
78 77 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 ) ) ) ) )
79 78 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 ) ) ) )
80 70 79 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 ) ) ) )
81 16 80 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 ) ) ) ) )
82 nfv 
 |-  F/ f ~P z C_ U
83 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 ) ) )
84 82 83 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 ) ) ) )
85 elpwi 
 |-  ( f e. ~P U -> f C_ U )
86 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 ) ) ) )
87 ssin 
 |-  ( ( ~P z C_ U /\ ~P z C_ w ) <-> ~P z C_ ( U i^i w ) )
88 87 biimpi 
 |-  ( ( ~P z C_ U /\ ~P z C_ w ) -> ~P z C_ ( U i^i w ) )
89 88 ex 
 |-  ( ~P z C_ U -> ( ~P z C_ w -> ~P z C_ ( U i^i w ) ) )
90 89 adantr 
 |-  ( ( ~P z C_ U /\ f C_ U ) -> ( ~P z C_ w -> ~P z C_ ( U i^i w ) ) )
91 simp3 
 |-  ( ( ~P z C_ U /\ f C_ U /\ i e. U. f ) -> i e. U. f )
92 eluni 
 |-  ( i e. U. f <-> E. v ( i e. v /\ v e. f ) )
93 91 92 sylib 
 |-  ( ( ~P z C_ U /\ f C_ U /\ i e. U. f ) -> E. v ( i e. v /\ v e. f ) )
94 simpl2 
 |-  ( ( ( ~P z C_ U /\ f C_ U /\ i e. U. f ) /\ ( i e. v /\ v e. f ) ) -> f C_ U )
95 simprr 
 |-  ( ( ( ~P z C_ U /\ f C_ U /\ i e. U. f ) /\ ( i e. v /\ v e. f ) ) -> v e. f )
96 94 95 sseldd 
 |-  ( ( ( ~P z C_ U /\ f C_ U /\ i e. U. f ) /\ ( i e. v /\ v e. f ) ) -> v e. U )
97 simprl 
 |-  ( ( ( ~P z C_ U /\ f C_ U /\ i e. U. f ) /\ ( i e. v /\ v e. f ) ) -> i e. v )
98 96 97 95 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 ) )
99 98 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 ) ) )
100 99 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 ) ) )
101 93 100 mpd 
 |-  ( ( ~P z C_ U /\ f C_ U /\ i e. U. f ) -> E. v ( v e. U /\ i e. v /\ v e. f ) )
102 df-rex 
 |-  ( E. v e. U ( i e. v /\ v e. f ) <-> E. v ( v e. U /\ ( i e. v /\ v e. f ) ) )
103 3anass 
 |-  ( ( v e. U /\ i e. v /\ v e. f ) <-> ( v e. U /\ ( i e. v /\ v e. f ) ) )
104 103 exbii 
 |-  ( E. v ( v e. U /\ i e. v /\ v e. f ) <-> E. v ( v e. U /\ ( i e. v /\ v e. f ) ) )
105 102 104 bitr4i 
 |-  ( E. v e. U ( i e. v /\ v e. f ) <-> E. v ( v e. U /\ i e. v /\ v e. f ) )
106 101 105 sylibr 
 |-  ( ( ~P z C_ U /\ f C_ U /\ i e. U. f ) -> E. v e. U ( i e. v /\ v e. f ) )
107 106 3expia 
 |-  ( ( ~P z C_ U /\ f C_ U ) -> ( i e. U. f -> E. v e. U ( i e. v /\ v e. f ) ) )
108 elin 
 |-  ( u e. ( f i^i ~P ~P w ) <-> ( u e. f /\ u e. ~P ~P w ) )
109 vex 
 |-  u e. _V
110 109 54 mpbiran 
 |-  ( u e. ~P ~P w <-> U. u C_ w )
111 110 anbi2i 
 |-  ( ( u e. f /\ u e. ~P ~P w ) <-> ( u e. f /\ U. u C_ w ) )
112 108 111 bitri 
 |-  ( u e. ( f i^i ~P ~P w ) <-> ( u e. f /\ U. u C_ w ) )
113 112 anbi2i 
 |-  ( ( i e. u /\ u e. ( f i^i ~P ~P w ) ) <-> ( i e. u /\ ( u e. f /\ U. u C_ w ) ) )
114 an12 
 |-  ( ( u e. f /\ ( i e. u /\ U. u C_ w ) ) <-> ( i e. u /\ ( u e. f /\ U. u C_ w ) ) )
115 113 114 bitr4i 
 |-  ( ( i e. u /\ u e. ( f i^i ~P ~P w ) ) <-> ( u e. f /\ ( i e. u /\ U. u C_ w ) ) )
116 115 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 ) ) )
117 eluni 
 |-  ( i e. U. ( f i^i ~P ~P w ) <-> E. u ( i e. u /\ u e. ( f i^i ~P ~P w ) ) )
118 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 ) ) )
119 116 117 118 3bitr4i 
 |-  ( i e. U. ( f i^i ~P ~P w ) <-> E. u e. f ( i e. u /\ U. u C_ w ) )
120 119 biimpri 
 |-  ( E. u e. f ( i e. u /\ U. u C_ w ) -> i e. U. ( f i^i ~P ~P w ) )
121 120 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 ) ) )
122 107 121 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 ) ) ) )
123 122 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 ) ) ) )
124 elin 
 |-  ( i e. ( z i^i U. f ) <-> ( i e. z /\ i e. U. f ) )
125 124 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 ) ) )
126 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 ) ) ) )
127 125 126 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 ) ) ) )
128 127 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 ) ) ) )
129 df-ss 
 |-  ( ( 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 ) ) )
130 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 ) ) ) )
131 128 129 130 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 ) ) )
132 123 131 imbitrrdi 
 |-  ( ( ~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 ) ) )
133 90 132 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 ) ) ) )
134 133 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 ) ) ) )
135 134 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 ) ) )
136 135 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 ) ) )
137 86 136 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 ) ) )
138 137 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 ) ) )
139 85 138 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 ) ) )
140 84 139 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 ) ) )
141 81 140 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 ) ) ) ) )